From c546d9df978994e097eb0681da307d4b953bd4df Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 5 Sep 2018 13:07:41 -0700 Subject: [PATCH 1/2] creport example --- test/creport2.ivy | 26 +++++++++++++++++--------- 1 file changed, 17 insertions(+), 9 deletions(-) diff --git a/test/creport2.ivy b/test/creport2.ivy index c1690dc..efc1812 100644 --- a/test/creport2.ivy +++ b/test/creport2.ivy @@ -109,13 +109,18 @@ module mysegment(domain,range,none) = { property X < offset(W) -> value(W,X,none) property shift.r(offset(W),X,Y) & Y < elems(W).end -> value(W,X,elems(W).value(Y)) - property shift.r(offset(W),X,Y) & Y >= elems(W).end -> value(W,X,none) +# property shift.r(offset(W),X,Y) & Y >= elems(W).end -> value(W,X,none) property value(W, I, V1) & value(W, I, V2) -> V1 = V2 property value(W, I, V) -> 0 <= I + # definition value(w:this,x:domain,v:range) = + # (exists Y. shift.r(offset(w),x,Y) & + # (v = elems(w).value(Y) if Y < elems(w).end else none)) + # | x < offset(w) & v = none + definition value(w:this,x:domain,v:range) = - (exists Y. shift.r(offset(w),x,Y) & - (v = elems(w).value(Y) if Y < elems(w).end else none)) + (exists Y. shift.r(offset(w),x,Y) & Y < elems(w).end & v = elems(w).value(Y)) + | (exists Y. shift.r(offset(w),Y,elems(w).end) & Y <= x & v = none) | x < offset(w) & v = none definition begin(W,I) = (I = offset(W)) @@ -141,11 +146,12 @@ module mysegment(domain,range,none) = { if j < bound { while j < bound invariant i <= j & j <= bound - invariant shift.r(w.offset,bound,w.elems.end) - invariant j <= X & X < bound & shift.r(w.offset,X,Y) -> value(w,X,w.elems.value(Y)) - invariant X < j & shift.r(i,X,Y) -> value(w,X,w.elems.value(Y)) - invariant w.offset <= j - invariant shift.r(i,j,X) -> X < w.elems.end + invariant shift.r(offset(old w),bound,old w.elems.end) + invariant j <= X & X < bound & shift.r(offset(old w),X,Y) -> value(old w,X,w.elems.value(Y)) + invariant X < j & shift.r(i,X,Y) -> value(old w,X,w.elems.value(Y)) + invariant w.offset <= j & w.offset = offset(old w) + invariant w.elems.end = elems(old w).end +# invariant shift.r(i,j,X) -> X < w.elems.end { w.elems := w.elems.set(shift.f(i,j),w.elems.value(shift.f(w.offset,j))); j := j.next; @@ -154,9 +160,11 @@ module mysegment(domain,range,none) = { w.offset := i } else { + assume false; w.elems := arr.empty; w.offset := i; - } + }; + bound := shift.b(offset(w),w.elems.end) # just for a witness } From 20299eedd5aaa44f510a992560d56e9bac0914c0 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Wed, 5 Sep 2018 15:55:24 -0700 Subject: [PATCH 2/2] creport2.ivy --- test/creport2.ivy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test/creport2.ivy b/test/creport2.ivy index efc1812..99b8c8e 100644 --- a/test/creport2.ivy +++ b/test/creport2.ivy @@ -119,8 +119,8 @@ module mysegment(domain,range,none) = { # | x < offset(w) & v = none definition value(w:this,x:domain,v:range) = - (exists Y. shift.r(offset(w),x,Y) & Y < elems(w).end & v = elems(w).value(Y)) - | (exists Y. shift.r(offset(w),Y,elems(w).end) & Y <= x & v = none) + (exists Y. shift.r(offset(w),x,Y) & + (v = elems(w).value(Y) if Y < elems(w).end else none)) | x < offset(w) & v = none definition begin(W,I) = (I = offset(W))