diff options
Diffstat (limited to 'Test')
24 files changed, 1276 insertions, 46 deletions
diff --git a/Test/VerifyThis2015/Problem2.dfy b/Test/VerifyThis2015/Problem2.dfy index 84fa924d..1c7deffd 100644 --- a/Test/VerifyThis2015/Problem2.dfy +++ b/Test/VerifyThis2015/Problem2.dfy @@ -2,7 +2,7 @@ // RUN: %diff "%s.expect" "%t"
// Rustan Leino
-// 13 April 2015
+// 13 April 2015, and many subsequent enhancements and revisions
// VerifyThis 2015
// Problem 2 -- Parallel GCD
@@ -109,7 +109,6 @@ method ParallelGcd_WithoutTermination(A: int, B: int) returns (gcd: int) method ParallelGcd(A: int, B: int) returns (gcd: int)
requires A > 0 && B > 0
ensures gcd == Gcd(A, B)
- decreases *
{
var a, b := A, B;
var pc0, pc1 := 0, 0; // program counter for the two processes
@@ -127,12 +126,13 @@ method ParallelGcd(A: int, B: int) returns (gcd: int) invariant pc0 == 2 ==> b <= b0 && (b0 <= a0 ==> b0 == b)
invariant pc1 == 2 ==> a <= a1 && (a1 <= b1 ==> a1 == a)
invariant (pc0 == 3 ==> a == b) && (pc1 == 3 ==> a == b)
- invariant 0 <= budget0 && 0 <= budget1 && 1 <= budget0 + budget1
+ invariant 0 <= budget0 && 0 <= budget1 && (pc0 == 3 || pc1 == 3 || 1 <= budget0 + budget1)
// With the budgets, the program is guaranteed to terminate, as is proved by the following termination
- // metric (which is a lexicographic triple):
- decreases *, a + b,
-// if a == b then 0 else if a < b then budget0 else budget1,
- (if a0 < b0 then budget0 else 0) + (if b1 < a1 then budget1 else 0),
+ // metric (which is a lexicographic tuple):
+ decreases a + b,
+ FinalStretch(pc0, pc1, a0, b0, b) + FinalStretch(pc1, pc0, b1, a1, a),
+ (if pc0 == 2 && a0 < b0 && !(a < b) then 1 else 0) + (if pc1 == 2 && b1 < a1 && !(b < a) then 1 else 0),
+ (if a < b then budget0 else 0) + (if b < a then budget1 else 0),
8 - pc0 - pc1
{
if {
@@ -166,15 +166,26 @@ method ParallelGcd(A: int, B: int) returns (gcd: int) gcd := a;
}
+function FinalStretch(pcThis: int, pcThat: int, a0: int, b0: int, b: int): int
+{
+ if pcThat != 3 then 10 // we're not yet in the final stretch
+ else if pcThis == 3 then 0
+ else if pcThis == 2 && a0 == b0 then 1
+ else if pcThis == 1 && a0 == b then 2
+ else if pcThis == 0 then 3
+ else if pcThis == 2 && a0 < b0 then 4
+ else 5
+}
+
method BudgetUpdate(inThis: int, inThat: int, pcThat: int) returns (outThis: int, outThat: int)
requires pcThat == 3 || 0 < inThis
- ensures pcThat == 3 ==> outThis == inThis && outThat == inThat
- ensures pcThat != 3 ==> outThis == inThis - 1 && outThat > 0
+ ensures outThis == if 0 < inThis then inThis - 1 else inThis
+ ensures if pcThat == 3 then outThat == inThat else outThat > 0
{
+ outThis := if 0 < inThis then inThis - 1 else inThis;
if pcThat == 3 {
- outThis, outThat := inThis, inThat;
+ outThat := inThat;
} else {
- outThis := inThis - 1;
outThat :| outThat > 0;
}
}
@@ -295,11 +306,7 @@ lemma Symmetry(a: int, b: int) assert DividesBoth(k, a, b) && forall m :: DividesBoth(m, a, b) ==> m <= k;
assert DividesBoth(l, b, a) && forall m :: DividesBoth(m, b, a) ==> m <= l;
assert DividesBoth(l, a, b);
- forall m | DividesBoth(m, b, a)
- ensures m <= l && DividesBoth(m, a, b)
- {
- }
- assert forall m :: DividesBoth(m, a, b) ==> m <= l;
+ assert forall m :: DividesBoth(m, b, a) ==> m <= l && DividesBoth(m, a, b);
assert k == l;
}
diff --git a/Test/VerifyThis2015/Problem2.dfy.expect b/Test/VerifyThis2015/Problem2.dfy.expect index ad540132..f5e3b3dc 100644 --- a/Test/VerifyThis2015/Problem2.dfy.expect +++ b/Test/VerifyThis2015/Problem2.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 35 verified, 0 errors
+Dafny program verifier finished with 36 verified, 0 errors
diff --git a/Test/VerifyThis2015/Problem3.dfy b/Test/VerifyThis2015/Problem3.dfy index fb95637d..4205035d 100644 --- a/Test/VerifyThis2015/Problem3.dfy +++ b/Test/VerifyThis2015/Problem3.dfy @@ -123,3 +123,23 @@ class DoublyLinkedList { Nodes := Nodes[..k] + [x] + Nodes[k..];
}
}
+
+// --------------------------------------------------------
+// If it were not required to build a data structure (like the class above) that supports the
+// Remove and PutBack operations, the operations can easily be verified to compose into the
+// identity transformation. The following method shows that the two operations, under a suitable
+// precondition, have no net effect on any .L or .R field.
+
+method Alt(x: Node)
+ requires x != null && x.L != null && x.R != null
+ requires x.L.R == x && x.R.L == x // links are mirrored
+ modifies x, x.L, x.R
+ ensures forall y: Node :: y != null ==> y.L == old(y.L) && y.R == old(y.R)
+{
+ // remove
+ x.R.L := x.L;
+ x.L.R := x.R;
+ // put back
+ x.R.L := x;
+ x.L.R := x;
+}
diff --git a/Test/VerifyThis2015/Problem3.dfy.expect b/Test/VerifyThis2015/Problem3.dfy.expect index 9559b9a6..4035605c 100644 --- a/Test/VerifyThis2015/Problem3.dfy.expect +++ b/Test/VerifyThis2015/Problem3.dfy.expect @@ -1,5 +1,5 @@ -Dafny program verifier finished with 13 verified, 0 errors
+Dafny program verifier finished with 15 verified, 0 errors
Program compiled successfully
Running...
diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy index 99b263a5..d1b04b1d 100644 --- a/Test/dafny0/Coinductive.dfy +++ b/Test/dafny0/Coinductive.dfy @@ -129,7 +129,7 @@ module CoPredicateResolutionErrors { }
ghost method Lemma(n: int)
- ensures Even(Doubles(n));
+ ensures Even(Doubles(n))
{
}
@@ -184,3 +184,106 @@ module UnfruitfulCoLemmaConclusions { {
}
}
+
+// --------------- Inductive Predicates --------------------------
+
+module InductivePredicateResolutionErrors {
+
+ datatype List<T> = Nil | Cons(head: T, tail: List)
+ codatatype IList<T> = INil | ICons(head: T, tail: IList)
+
+ inductive predicate Pos(s: List<int>)
+ {
+ s.Cons? && 0 < s.head && Pos(s.tail) && Even(s)
+ }
+
+ inductive predicate Even(s: List<int>)
+ {
+ s.Cons? && s.head % 2 == 0 && Even(s.tail)
+ && (s.head == 17 ==> Pos(s))
+ && (Pos(s) ==> s.head == 17) // error: cannot make recursive inductive-predicate call in negative position
+ && !Even(s) // error: cannot make recursive inductive-predicate call in negative position
+ && (Even(s) <==> Even(s)) // error (x2): recursive inductive-predicate calls allowed only in positive positions
+ }
+
+ inductive predicate LetSuchThat(s: List<int>)
+ {
+ if s != Nil then true else
+ var h :| h == s.head;
+ h < 0 && LetSuchThat(s.tail) // this is fine for an inductive predicate
+ }
+ copredicate CoLetSuchThat(s: IList<int>)
+ {
+ if s != INil then true else
+ var h :| h == s.head;
+ h < 0 && CoLetSuchThat(s.tail) // error: recursive call to copredicate in body of let-such-that
+ }
+
+ inductive predicate NegatedLetSuchThat(s: List<int>)
+ {
+ if s != Nil then true else
+ !var h :| h == s.head;
+ h < 0 && !NegatedLetSuchThat(s.tail) // error: recursive call to inductive predicate in body of let-such-that
+ }
+ copredicate NegatedCoLetSuchThat(s: IList<int>)
+ {
+ if s != INil then true else
+ !var h :| h == s.head;
+ h < 0 && !NegatedCoLetSuchThat(s.tail) // this is fine for a coinductive predicate
+ }
+
+ inductive predicate CP(i: int)
+ {
+ CP(i) &&
+ !CP(i) && // error: not in a positive position
+ (exists j :: CP(j)) &&
+ (forall k :: 0 <= k < i*i ==> CP(k)) &&
+ (forall k :: 0 <= k ==> CP(k)) && // error: unbounded range
+ (forall k :: k < i*i ==> CP(k)) && // error: unbounded range
+ (forall l :: CP(l)) // error: unbounded range
+ }
+
+ inductive predicate CQ(i: int, j: int)
+ {
+ forall i :: i == 6 ==> if j % 2 == 0 then CQ(i, i) else CQ(j, j)
+ }
+
+ inductive predicate CR(i: int, j: int)
+ {
+ i == if CR(i, j) then 6 else j // error: not allowed to call CR recursively here
+ }
+
+ inductive predicate CS(i: int, j: int)
+ {
+ forall i ::
+ i <= (if CS(i, j) then 6 else j) && // error: not allowed to call CS recursively here
+ (if CS(i, j) then 6 else j) <= i // error: not allowed to call CS recursively here
+ }
+
+ inductive predicate Another(s: List<int>)
+ {
+ !Even(s) // here, negation is fine
+ }
+
+ inductive predicate IndStmtExpr_Good(s: List<int>)
+ {
+ s.head > 0 && (MyLemma(s.head); IndStmtExpr_Good(s.tail))
+ }
+
+ lemma MyLemma(x: int)
+ {
+ }
+
+ inductive predicate IndStmtExpr_Bad(s: List<int>)
+ {
+ s.Cons? && s.head > 0 &&
+ (MyRecursiveLemma(s.head); // error: cannot call method recursively from inductive predicate
+ IndStmtExpr_Bad(s.tail))
+ }
+
+ lemma MyRecursiveLemma(x: int)
+ {
+ var p := IndStmtExpr_Bad(Cons(x, Nil));
+ }
+}
+
diff --git a/Test/dafny0/Coinductive.dfy.expect b/Test/dafny0/Coinductive.dfy.expect index 26fec211..4821a0e3 100644 --- a/Test/dafny0/Coinductive.dfy.expect +++ b/Test/dafny0/Coinductive.dfy.expect @@ -14,4 +14,18 @@ Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(148,21): Error: a recursive call from a copredicate can go only to other copredicates
-16 resolution/type errors detected in Coinductive.dfy
+Coinductive.dfy(204,8): Error: an inductive predicate can be called recursively only in positive positions
+Coinductive.dfy(205,8): Error: an inductive predicate can be called recursively only in positive positions
+Coinductive.dfy(206,8): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
+Coinductive.dfy(206,21): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
+Coinductive.dfy(219,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(226,16): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
+Coinductive.dfy(238,5): Error: an inductive predicate can be called recursively only in positive positions
+Coinductive.dfy(241,28): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
+Coinductive.dfy(242,29): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
+Coinductive.dfy(243,17): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
+Coinductive.dfy(253,12): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
+Coinductive.dfy(259,15): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
+Coinductive.dfy(260,10): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier
+Coinductive.dfy(280,21): Error: a recursive call from an inductive predicate can go only to other inductive predicates
+30 resolution/type errors detected in Coinductive.dfy
diff --git a/Test/dafny0/InductivePredicates.dfy b/Test/dafny0/InductivePredicates.dfy new file mode 100644 index 00000000..424118e7 --- /dev/null +++ b/Test/dafny0/InductivePredicates.dfy @@ -0,0 +1,175 @@ +// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype natinf = N(n: nat) | Inf
+
+inductive predicate Even(x: natinf)
+{
+ (x.N? && x.n == 0) ||
+ (x.N? && 2 <= x.n && Even(N(x.n - 2)))
+}
+
+lemma M(x: natinf)
+ requires Even(x)
+ ensures x.N? && x.n % 2 == 0
+{
+ var k: nat :| Even#[k](x);
+ M'(k, x);
+}
+
+// yay! my first proof involving an inductive predicate :)
+lemma M'(k: nat, x: natinf)
+ requires Even#[k](x)
+ ensures x.N? && x.n % 2 == 0
+{
+ if 0 < k {
+ if {
+ case x.N? && x.n == 0 =>
+ // trivial
+ case x.N? && 2 <= x.n && Even#[k-1](N(x.n - 2)) =>
+ M'(k-1, N(x.n - 2));
+ }
+ }
+}
+
+// Here is the same proof as in M / M', but packaged into a single "inductive lemma":
+inductive lemma IL(x: natinf)
+ requires Even(x)
+ ensures x.N? && x.n % 2 == 0
+{
+ if {
+ case x.N? && x.n == 0 =>
+ // trivial
+ case x.N? && 2 <= x.n && Even#[_k-1](N(x.n - 2)) =>
+ IL(N(x.n - 2));
+ }
+}
+
+inductive lemma IL_EvenBetter(x: natinf)
+ requires Even(x)
+ ensures x.N? && x.n % 2 == 0
+{
+ if {
+ case x.N? && x.n == 0 =>
+ // trivial
+ case x.N? && 2 <= x.n && Even(N(x.n - 2)) =>
+ IL_EvenBetter(N(x.n - 2));
+ }
+}
+
+inductive lemma IL_Bad(x: natinf)
+ requires Even(x)
+ ensures x.N? && x.n % 2 == 0
+{
+ assert false; // error: one shouldn't be able to prove just anything
+}
+
+lemma InfNotEven()
+ ensures !Even(Inf)
+{
+}
+
+lemma Test()
+{
+ assert !Even(N(1)); // Dafny can prove this
+ assert !Even(N(5));
+ assert !Even(N(17)); // error: this holds, but Dafny can't prove it directly (but see lemma below)
+}
+
+lemma SeventeenIsNotEven()
+ ensures !Even(N(17))
+{
+ assert Even(N(17))
+ == Even(N(15))
+ == Even(N(13))
+ == Even(N(11))
+ == Even(N(9))
+ == Even(N(7))
+ == Even(N(5))
+ == Even(N(3))
+ == Even(N(1))
+ == false;
+}
+
+lemma OneMore(x: natinf) returns (y: natinf)
+ requires Even(x)
+ ensures Even(y)
+{
+ y := N(x.n + 2);
+}
+
+// ----------------------- Here's another version of Even, using the S function
+
+module Alt {
+ datatype natinf = N(n: nat) | Inf
+
+ function S(x: natinf): natinf
+ {
+ match x
+ case N(n) => N(n+1)
+ case Inf => Inf
+ }
+
+ inductive predicate Even(x: natinf)
+ {
+ (x.N? && x.n == 0) ||
+ exists y :: x == S(S(y)) && Even(y)
+ }
+
+ inductive lemma MyLemma_NotSoNice(x: natinf)
+ requires Even(x)
+ ensures x.N? && x.n % 2 == 0
+ {
+ if {
+ case x.N? && x.n == 0 =>
+ // trivial
+ case exists y :: x == S(S(y)) && Even#[_k-1](y) =>
+ var y :| x == S(S(y)) && Even#[_k-1](y);
+ MyLemma_NotSoNice(y);
+ assert x.n == y.n + 2;
+ }
+ }
+
+ inductive lemma MyLemma_NiceButNotFast(x: natinf)
+ requires Even(x)
+ ensures x.N? && x.n % 2 == 0
+ {
+ if {
+ case x.N? && x.n == 0 =>
+ // trivial
+ case exists y :: x == S(S(y)) && Even(y) =>
+ var y :| x == S(S(y)) && Even(y);
+ MyLemma_NiceButNotFast(y);
+ assert x.n == y.n + 2;
+ }
+ }
+
+ lemma InfNotEven()
+ ensures !Even(Inf)
+ {
+ if Even(Inf) {
+ InfNotEven_Aux();
+ }
+ }
+
+ inductive lemma InfNotEven_Aux()
+ requires Even(Inf)
+ ensures false
+ {
+ var x := Inf;
+ if {
+ case x.N? && x.n == 0 =>
+ assert false; // this case is absurd
+ case exists y :: x == S(S(y)) && Even(y) =>
+ var y :| x == S(S(y)) && Even(y);
+ assert y == Inf;
+ InfNotEven_Aux();
+ }
+ }
+
+ lemma NextEven(x: natinf)
+ requires Even(x)
+ ensures Even(S(S(x)))
+ {
+ }
+}
diff --git a/Test/dafny0/InductivePredicates.dfy.expect b/Test/dafny0/InductivePredicates.dfy.expect new file mode 100644 index 00000000..b09b7903 --- /dev/null +++ b/Test/dafny0/InductivePredicates.dfy.expect @@ -0,0 +1,9 @@ +InductivePredicates.dfy(64,10): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Then
+InductivePredicates.dfy(76,11): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+
+Dafny program verifier finished with 29 verified, 2 errors
diff --git a/Test/dafny0/NestedMatch.dfy b/Test/dafny0/NestedMatch.dfy new file mode 100644 index 00000000..e6e7c489 --- /dev/null +++ b/Test/dafny0/NestedMatch.dfy @@ -0,0 +1,59 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype Nat = Zero | Suc(Nat)
+
+predicate Even(n: Nat)
+{
+ match n
+ case Zero => true
+ case Suc(Zero) => false
+ case Suc(Suc(p)) => Even(p)
+}
+
+
+method checkEven(n: Nat) {
+ assert Even(Zero) == true;
+ assert Even(Suc(Zero)) == false;
+ assert Even(Suc(Suc(n))) == Even(n);
+}
+
+datatype List<T> = Nil | Cons(T, List<T>)
+
+function last<T>(xs: List<T>): T
+ requires xs != Nil
+{
+ match xs
+ case Cons(y, Nil) => y
+ case Cons(y, Cons(z, zs)) => last(Cons(z, zs))
+}
+
+method checkLast(y: T) {
+ assert last(Cons(y, Nil)) == y;
+ assert last(Cons(y, Cons(y, Nil))) == last(Cons(y, Nil));
+}
+
+
+function minus(x: Nat, y: Nat): Nat
+{
+ match (x, y)
+ case (Zero, _) => Zero
+ case (Suc(_), Zero) => x
+ case (Suc(a), Suc(b)) => minus(a, b)
+}
+
+method checkMinus(x:Nat, y: Nat) {
+ assert minus(Suc(x), Suc(y)) == minus(x,y);
+}
+
+
+// nested match statement
+method Last<T>(xs: List<T>) returns (x: T)
+ requires xs != Nil
+{
+
+ match xs {
+ case Cons(y, Nil) => x:= y;
+ case Cons(y, Cons(z, zs)) => x:=Last(Cons(z, zs));
+ }
+}
diff --git a/Test/dafny0/NestedMatch.dfy.expect b/Test/dafny0/NestedMatch.dfy.expect new file mode 100644 index 00000000..f3a9c95f --- /dev/null +++ b/Test/dafny0/NestedMatch.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 11 verified, 0 errors
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index f0138c6c..761cffa0 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1342,3 +1342,10 @@ module GhostLet { x := ghost var a :| 0 <= a; 10; // fine
}
}
+
+// ------------------- tuple equality support -------------------
+
+module TupleEqualitySupport {
+ datatype GoodRecord = GoodRecord(set<(int,int)>)
+ datatype BadRecord = BadRecord(set<(int, int->bool)>) // error: this tuple type does not support equality
+}
diff --git a/Test/dafny0/snapshots/runtest.snapshot.expect b/Test/dafny0/snapshots/runtest.snapshot.expect index 8ad86f3b..f1050f62 100644 --- a/Test/dafny0/snapshots/runtest.snapshot.expect +++ b/Test/dafny0/snapshots/runtest.snapshot.expect @@ -6,12 +6,17 @@ Processing command (at Snapshots0.v0.dfy(4,10)) assert Lit(false); >>> DoNothingToAssert
Dafny program verifier finished with 3 verified, 0 errors
+Processing implementation CheckWellformed$$_module.__default.bar (at Snapshots0.v1.dfy(7,8)):
+ >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight)
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();
Processing call to procedure IntraModuleCall$$_module.__default.bar in implementation Impl$$_module.__default.foo (at Snapshots0.v1.dfy(3,6)):
- >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##1(call0old#AT#$Heap, $Heap) } ##extracted_function##1(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))
- >>> added after: a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
+ >>> added axiom: (forall call0old#AT#$Heap: Heap, $Heap: Heap :: {:weight 30} { ##extracted_function##2(call0old#AT#$Heap, $Heap) } ##extracted_function##2(call0old#AT#$Heap, $Heap) == (true && Lit(false) && (forall<alpha> $o: ref, $f: Field alpha :: { read($Heap, $o, $f) } $o != null && read(call0old#AT#$Heap, $o, alloc) ==> read($Heap, $o, $f) == read(call0old#AT#$Heap, $o, $f)) && $HeapSucc(call0old#AT#$Heap, $Heap)))
+ >>> added after: a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();
+ >>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots0.v1.dfy(3,6)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
>>> MarkAsFullyVerified
-Processing command (at <unknown location>) a##post##0 := a##post##0 && ##extracted_function##1(call0old#AT#$Heap, $Heap);
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2(call0old#AT#$Heap, $Heap);
>>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots0.v1.dfy(4,10)) assert Lit(false);
>>> MarkAsPartiallyVerified
@@ -31,7 +36,7 @@ Processing command (at Snapshots1.v0.dfy(12,3)) assert true; Dafny program verifier finished with 4 verified, 0 errors
Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots1.v1.dfy(3,4)):
- >>> added after: a##post##0 := a##post##0 && false;
+ >>> added after: a##cached##0 := a##cached##0 && false;
Processing command (at Snapshots1.v1.dfy(12,3)) assert true;
>>> MarkAsFullyVerified
Processing command (at Snapshots1.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
@@ -62,7 +67,11 @@ Processing command (at Snapshots2.v0.dfy(18,3)) assert true; Dafny program verifier finished with 6 verified, 0 errors
Processing call to procedure IntraModuleCall$$_module.__default.N in implementation Impl$$_module.__default.M (at Snapshots2.v1.dfy(3,4)):
- >>> added after: a##post##0 := a##post##0 && false;
+ >>> added after: a##cached##0 := a##cached##0 && false;
+Processing implementation CheckWellformed$$_module.__default.P (at Snapshots2.v1.dfy(10,11)):
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
+Processing implementation CheckWellformed$$_module.__default.Q (at Snapshots2.v1.dfy(13,11)):
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && false;
Processing command (at Snapshots2.v1.dfy(18,3)) assert true;
>>> MarkAsFullyVerified
Processing command (at Snapshots2.v1.dfy(3,4)) assert (forall<alpha> $o: ref, $f: Field alpha :: false ==> $_Frame[$o, $f]);
@@ -73,11 +82,11 @@ Snapshots2.v1.dfy(4,10): Error: assertion violation Execution trace:
(0,0): anon0
Processing command (at Snapshots2.v1.dfy(11,11)) assert true;
- >>> MarkAsFullyVerified
+ >>> DoNothingToAssert
Processing command (at Snapshots2.v1.dfy(11,15)) assert _module.__default.P($LS($LS($LZ)), $Heap) <==> _module.__default.Q($LS($LS($LZ)), $Heap);
>>> DoNothingToAssert
Processing command (at Snapshots2.v1.dfy(14,11)) assert true;
- >>> MarkAsFullyVerified
+ >>> DoNothingToAssert
Processing command (at Snapshots2.v1.dfy(14,15)) assert _module.__default.Q($LS($LS($LZ)), $Heap) <==> Lit(_module.__default.R($Heap));
>>> DoNothingToAssert
@@ -171,8 +180,28 @@ Processing command (at Snapshots7.v0.dfy(19,14)) assert Lit(false); >>> DoNothingToAssert
Dafny program verifier finished with 4 verified, 0 errors
+Processing implementation CheckWellformed$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)):
+ >>> added axiom: ##extracted_function##1() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight)
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##1();
+Processing implementation Impl$$_0_M0.C.Foo (at Snapshots7.v1.dfy(5,12)):
+ >>> added axiom: ##extracted_function##2() == (0 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false))
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##2();
+Processing implementation CheckWellformed$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)):
+ >>> added axiom: ##extracted_function##3() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight)
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##3();
+Processing implementation Impl$$_1_M1.C.Foo (at Snapshots7.v1.dfy[M1](5,12)):
+ >>> added axiom: ##extracted_function##4() == (1 == $ModuleContextHeight && 0 == $FunctionContextHeight && Lit(false))
+ >>> added after assuming the current precondition: a##cached##0 := a##cached##0 && ##extracted_function##4();
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##1();
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##2();
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##3();
+ >>> AssumeNegationOfAssumptionVariable
+Processing command (at <unknown location>) a##cached##0 := a##cached##0 && ##extracted_function##4();
+ >>> AssumeNegationOfAssumptionVariable
Processing command (at Snapshots7.v1.dfy(19,14)) assert Lit(false);
- >>> DoNothingToAssert
+ >>> MarkAsPartiallyVerified
Snapshots7.v1.dfy(19,14): Error: assertion violation
Execution trace:
(0,0): anon0
diff --git a/Test/dafny4/Bug79.dfy b/Test/dafny4/Bug79.dfy new file mode 100644 index 00000000..49f2421b --- /dev/null +++ b/Test/dafny4/Bug79.dfy @@ -0,0 +1,10 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function foo(s:int) : (int, int)
+
+function bar(s:int) : bool
+{
+ var (x, rest) := foo(s);
+ x > 0
+}
\ No newline at end of file diff --git a/Test/dafny4/Bug79.dfy.expect b/Test/dafny4/Bug79.dfy.expect new file mode 100644 index 00000000..069e7767 --- /dev/null +++ b/Test/dafny4/Bug79.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/dafny4/Bug81.dfy b/Test/dafny4/Bug81.dfy new file mode 100644 index 00000000..1992d666 --- /dev/null +++ b/Test/dafny4/Bug81.dfy @@ -0,0 +1,9 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function {:opaque} RefineSeqToSeq<T,U>(s:seq<T>, refine_func:T->U) : seq<U>
+ reads refine_func.reads;
+{
+ if |s| == 0 then []
+ else RefineSeqToSeq(s[1..], refine_func)
+}
diff --git a/Test/dafny4/Bug81.dfy.expect b/Test/dafny4/Bug81.dfy.expect new file mode 100644 index 00000000..069e7767 --- /dev/null +++ b/Test/dafny4/Bug81.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/dafny4/Juggernaut.dfy b/Test/dafny4/Juggernaut.dfy new file mode 100644 index 00000000..783f725b --- /dev/null +++ b/Test/dafny4/Juggernaut.dfy @@ -0,0 +1,20 @@ +// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Jug()
+{
+ var x, y, z;
+ while x > 0 && y > 0 && z > 0
+ decreases x < y, z
+ {
+ if y > x {
+ y := z;
+ x := *;
+ z := x - 1;
+ } else {
+ z := z - 1;
+ x := *;
+ y := x - 1;
+ }
+ }
+}
diff --git a/Test/dafny4/Juggernaut.dfy.expect b/Test/dafny4/Juggernaut.dfy.expect new file mode 100644 index 00000000..069e7767 --- /dev/null +++ b/Test/dafny4/Juggernaut.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 2 verified, 0 errors
diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy b/Test/dafny4/NipkowKlein-chapter3.dfy new file mode 100644 index 00000000..6572359a --- /dev/null +++ b/Test/dafny4/NipkowKlein-chapter3.dfy @@ -0,0 +1,282 @@ +// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file is a Dafny encoding of chapter 3 from "Concrete Semantics: With Isabelle/HOL" by
+// Tobias Nipkow and Gerwin Klein.
+
+// ----- lists -----
+
+datatype List<T> = Nil | Cons(head: T, tail: List<T>)
+
+function append(xs: List, ys: List): List
+{
+ match xs
+ case Nil => ys
+ case Cons(x, tail) => Cons(x, append(tail, ys))
+}
+
+// ----- arithmetic expressions -----
+
+type vname = string // variable names
+datatype aexp = N(n: int) | V(x: vname) | Plus(0: aexp, 1: aexp) // arithmetic expressions
+
+type val = int
+type state = vname -> val
+// In Dafny, functions can in general read the heap (which is not interesting to these examples--in fact, for
+// the examples in this file, the fact that functions can read the state is just a distraction, so you can
+// just ignore all the lines "reads s.reads" if you prefer) and may have preconditions (that is, the function
+// may have some domain that is not specific than what its type says).
+// The following predicate holds for a given s if s can be applied to any vname
+predicate Total(s: state)
+ reads s.reads // this says that Total(s) can read anything that s can (on any input)
+{
+ // the following line is the conjunction, over all x, of the precondition of the call s(x)
+ forall x :: s.requires(x)
+}
+
+function aval(a: aexp, s: state): val
+ reads s.reads
+ requires Total(s)
+{
+ match a
+ case N(n) => n
+ case V(x) => s(x)
+ case Plus(a0, a1) => aval(a0, s) + aval(a1, s)
+}
+
+lemma Example0()
+{
+ var y := aval(Plus(N(3), V("x")), x => 0);
+ // The following line confirms that y is 3. If you don't know what y is, you can use the
+ // verification debugger to figure it out, like this: Put any value in the assert (for example,
+ // "assert y == 0;". If you're lucky and picked the right value, the verifier will prove the
+ // assertion for you. If the verifier says it's unable to prove it, then click on the error
+ // (in the Dafny IDE), which brings up the verification debugger. There, inspect the value
+ // of y. This is probably the right value, but due to incompleteness in the verifier, it
+ // could happen that the value you see is some value that verifier wasn't able to properly
+ // exclude. Therefore, it's best to now take the value you see in the verification debugger,
+ // say K, and put that into the assert ("assert y == K;"), to have the verifier confirm that
+ // K really is the answer.
+ assert y == 3;
+}
+
+// ----- constant folding -----
+
+function asimp_const(a: aexp): aexp
+{
+ match a
+ case N(n) => a
+ case V(x) => a
+ case Plus(a0, a1) =>
+ var as0, as1 := asimp_const(a0), asimp_const(a1);
+ if as0.N? && as1.N? then
+ N(as0.n + as1.n)
+ else
+ Plus(as0, as1)
+}
+
+lemma AsimpConst(a: aexp, s: state)
+ requires Total(s)
+ ensures aval(asimp_const(a), s) == aval(a, s)
+{
+ // by induction
+ forall a' | a' < a {
+ AsimpConst(a', s); // this invokes the induction hypothesis for every a' that is structurally smaller than a
+ }
+/* Here is an alternative proof. In the first two cases, the proof is trivial. The Plus case uses two invocations
+ of the induction hypothesis.
+ match a
+ case N(n) =>
+ case V(x) =>
+ case Plus(a0, a1) =>
+ AsimpConst(a0, s);
+ AsimpConst(a1, s);
+*/
+}
+
+// more constant folding
+
+function plus(a0: aexp, a1: aexp): aexp
+{
+ if a0.N? && a1.N? then
+ N(a0.n + a1.n)
+ else if a0.N? then
+ if a0.n == 0 then a1 else Plus(a0, a1)
+ else if a1.N? then
+ if a1.n == 0 then a0 else Plus(a0, a1)
+ else
+ Plus(a0, a1)
+}
+
+lemma AvalPlus(a0: aexp, a1: aexp, s: state)
+ requires Total(s)
+ ensures aval(plus(a0, a1), s) == aval(a0, s) + aval(a1, s)
+{
+ // this proof is done automatically
+}
+
+function asimp(a: aexp): aexp
+{
+ match a
+ case N(n) => a
+ case V(x) => a
+ case Plus(a0, a1) => plus(asimp(a0), asimp(a1))
+}
+
+lemma AsimpCorrect(a: aexp, s: state)
+ requires Total(s)
+ ensures aval(asimp(a), s) == aval(a, s)
+{
+ // call the induction hypothesis on every value a' that is structurally smaller than a
+ forall a' | a' < a { AsimpCorrect(a', s); }
+}
+
+// ----- boolean expressions -----
+
+datatype bexp = Bc(v: bool) | Not(op: bexp) | And(0: bexp, 1: bexp) | Less(a0: aexp, a1: aexp)
+
+function bval(b: bexp, s: state): bool
+ reads s.reads
+ requires Total(s)
+{
+ match b
+ case Bc(v) => v
+ case Not(b) => !bval(b, s)
+ case And(b0, b1) => bval(b0, s) && bval(b1, s)
+ case Less(a0, a1) => aval(a0, s) < aval(a1, s)
+}
+
+// constant folding for booleans
+
+function not(b: bexp): bexp
+{
+ match b
+ case Bc(b0) => Bc(!b0)
+ case Not(b0) => b0 // this case is not in the Nipkow and Klein book, but it seems a nice one to include
+ case And(_, _) => Not(b)
+ case Less(_, _) => Not(b)
+}
+
+function and(b0: bexp, b1: bexp): bexp
+{
+ if b0.Bc? then
+ if b0.v then b1 else b0
+ else if b1.Bc? then
+ if b1.v then b0 else b1
+ else
+ And(b0, b1)
+}
+
+function less(a0: aexp, a1: aexp): bexp
+{
+ if a0.N? && a1.N? then
+ Bc(a0.n < a1.n)
+ else
+ Less(a0, a1)
+}
+
+function bsimp(b: bexp): bexp
+{
+ match b
+ case Bc(v) => b
+ case Not(b0) => not(bsimp(b0))
+ case And(b0, b1) => and(bsimp(b0), bsimp(b1))
+ case Less(a0, a1) => less(asimp(a0), asimp(a1))
+}
+
+lemma BsimpCorrect(b: bexp, s: state)
+ requires Total(s)
+ ensures bval(bsimp(b), s) == bval(b, s)
+{
+/* Here is one proof, which uses the induction hypothesis any anything smaller than b and also invokes
+ the lemma AsimpCorrect on anything smaller than b.
+ forall b' | b' < b { BsimpCorrect(b', s); }
+ forall a' | a' < b { AsimpCorrect(a', s); }
+*/
+ // Here is another proof, which makes explicit the uses of the induction hypothesis and the other lemma.
+ match b
+ case Bc(v) =>
+ case Not(b0) =>
+ BsimpCorrect(b0, s);
+ case And(b0, b1) =>
+ BsimpCorrect(b0, s); BsimpCorrect(b1, s);
+ case Less(a0, a1) =>
+ AsimpCorrect(a0, s); AsimpCorrect(a1, s);
+}
+
+// ----- stack machine -----
+
+datatype instr = LOADI(val) | LOAD(vname) | ADD
+
+type stack = List<val>
+
+function exec1(i: instr, s: state, stk: stack): stack
+ reads s.reads
+ requires Total(s)
+{
+ match i
+ case LOADI(n) => Cons(n, stk)
+ case LOAD(x) => Cons(s(x), stk)
+ case ADD =>
+ if stk.Cons? && stk.tail.Cons? then
+ var Cons(a1, Cons(a0, tail)) := stk;
+ Cons(a0 + a1, tail)
+ else // stack underflow
+ Nil // an alternative would be to return Cons(n, Nil) for an arbitrary value n--that is what Nipkow and Klein do
+}
+
+function exec(ii: List<instr>, s: state, stk: stack): stack
+ reads s.reads
+ requires Total(s)
+{
+ match ii
+ case Nil => stk
+ case Cons(i, rest) => exec(rest, s, exec1(i, s, stk))
+}
+
+// ----- compilation -----
+
+function comp(a: aexp): List<instr>
+{
+ match a
+ case N(n) => Cons(LOADI(n), Nil)
+ case V(x) => Cons(LOAD(x), Nil)
+ case Plus(a0, a1) => append(append(comp(a0), comp(a1)), Cons(ADD, Nil))
+}
+
+lemma CorrectCompilation(a: aexp, s: state, stk: stack)
+ requires Total(s)
+ ensures exec(comp(a), s, stk) == Cons(aval(a, s), stk)
+{
+ match a
+ case N(n) =>
+ case V(x) =>
+ case Plus(a0, a1) =>
+ // This proof spells out the proof as a series of equality-preserving steps. Each
+ // expression in the calculation is terminated by a semi-colon. In some cases, a hint
+ // for the step is needed. Such hints are given in curly braces.
+ calc {
+ exec(comp(a), s, stk);
+ // definition of comp on Plus
+ exec(append(append(comp(a0), comp(a1)), Cons(ADD, Nil)), s, stk);
+ { ExecAppend(append(comp(a0), comp(a1)), Cons(ADD, Nil), s, stk); }
+ exec(Cons(ADD, Nil), s, exec(append(comp(a0), comp(a1)), s, stk));
+ { ExecAppend(comp(a0), comp(a1), s, stk); }
+ exec(Cons(ADD, Nil), s, exec(comp(a1), s, exec(comp(a0), s, stk)));
+ { CorrectCompilation(a0, s, stk); }
+ exec(Cons(ADD, Nil), s, exec(comp(a1), s, Cons(aval(a0, s), stk)));
+ { CorrectCompilation(a1, s, Cons(aval(a0, s), stk)); }
+ exec(Cons(ADD, Nil), s, Cons(aval(a1, s), Cons(aval(a0, s), stk)));
+ // definition of comp on ADD
+ Cons(aval(a1, s) + aval(a0, s), stk);
+ // definition of aval on Plus
+ Cons(aval(a, s), stk);
+ }
+}
+
+lemma ExecAppend(ii0: List<instr>, ii1: List<instr>, s: state, stk: stack)
+ requires Total(s)
+ ensures exec(append(ii0, ii1), s, stk) == exec(ii1, s, exec(ii0, s, stk))
+{
+ // the proof (which is by induction) is done automatically
+}
diff --git a/Test/dafny4/NipkowKlein-chapter3.dfy.expect b/Test/dafny4/NipkowKlein-chapter3.dfy.expect new file mode 100644 index 00000000..ab18d98e --- /dev/null +++ b/Test/dafny4/NipkowKlein-chapter3.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 28 verified, 0 errors
diff --git a/Test/dafny4/NipkowKlein-chapter7.dfy b/Test/dafny4/NipkowKlein-chapter7.dfy new file mode 100644 index 00000000..33be9dd6 --- /dev/null +++ b/Test/dafny4/NipkowKlein-chapter7.dfy @@ -0,0 +1,468 @@ +// RUN: %dafny /compile:0 /rprint:"%t.rprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// This file is a Dafny encoding of chapter 7 from "Concrete Semantics: With Isabelle/HOL" by
+// Tobias Nipkow and Gerwin Klein.
+
+// ----- first, some definitions from chapter 3 -----
+
+datatype List<T> = Nil | Cons(head: T, tail: List<T>)
+type vname = string // variable names
+
+type val = int
+type state = imap<vname, val>
+predicate Total(s: state)
+{
+ forall x :: x in s
+}
+
+datatype aexp = N(n: int) | V(x: vname) | Plus(0: aexp, 1: aexp) // arithmetic expressions
+function aval(a: aexp, s: state): val
+ requires Total(s)
+{
+ match a
+ case N(n) => n
+ case V(x) => s[x]
+ case Plus(a0, a1) => aval(a0,s ) + aval(a1, s)
+}
+
+datatype bexp = Bc(v: bool) | Not(op: bexp) | And(0: bexp, 1: bexp) | Less(a0: aexp, a1: aexp)
+function bval(b: bexp, s: state): bool
+ requires Total(s)
+{
+ match b
+ case Bc(v) => v
+ case Not(b) => !bval(b, s)
+ case And(b0, b1) => bval(b0, s) && bval(b1, s)
+ case Less(a0, a1) => aval(a0, s) < aval(a1, s)
+}
+
+// ----- IMP commands -----
+
+datatype com = SKIP | Assign(vname, aexp) | Seq(com, com) | If(bexp, com, com) | While(bexp, com)
+
+// ----- Big-step semantics -----
+
+inductive predicate big_step(c: com, s: state, t: state)
+ requires Total(s)
+{
+ match c
+ case SKIP =>
+ s == t
+ case Assign(x, a) =>
+ t == s[x := aval(a, s)]
+ case Seq(c0, c1) =>
+ exists s' ::
+ Total(s') &&
+ big_step(c0, s, s') &&
+ big_step(c1, s', t)
+ case If(b, thn, els) =>
+ big_step(if bval(b, s) then thn else els, s, t)
+ case While(b, body) =>
+ (!bval(b, s) && s == t) ||
+ (bval(b, s) && exists s' ::
+ Total(s') &&
+ big_step(body, s, s') &&
+ big_step(While(b, body), s', t))
+}
+
+lemma Example1(s: state, t: state)
+ requires Total(s)
+ requires t == s["x" := 5]["y" := 5]
+ ensures big_step(Seq(Assign("x", N(5)), Assign("y", V("x"))), s, t)
+{
+ var s' := s["x" := 5];
+ calc <== {
+ big_step(Seq(Assign("x", N(5)), Assign("y", V("x"))), s, t);
+ // 5 is suffiiently high
+ big_step#[5](Seq(Assign("x", N(5)), Assign("y", V("x"))), s, t);
+ big_step#[4](Assign("x", N(5)), s, s') && big_step#[4](Assign("y", V("x")), s', t);
+ // the rest is done automatically
+ true;
+ }
+}
+
+lemma SemiAssociativity(c0: com, c1: com, c2: com, s: state, t: state)
+ requires Total(s)
+ ensures big_step(Seq(Seq(c0, c1), c2), s, t) == big_step(Seq(c0, Seq(c1, c2)), s, t)
+{
+ calc {
+ big_step(Seq(Seq(c0, c1), c2), s, t);
+ // def. big_step
+ exists s'' :: Total(s'') && big_step(Seq(c0, c1), s, s'') && big_step(c2, s'', t);
+ // def. big_step
+ exists s'' :: Total(s'') && (exists s' :: Total(s') && big_step(c0, s, s') && big_step(c1, s', s'')) && big_step(c2, s'', t);
+ // logic
+ exists s', s'' :: Total(s') && Total(s'') && big_step(c0, s, s') && big_step(c1, s', s'') && big_step(c2, s'', t);
+ // logic
+ exists s' :: Total(s') && big_step(c0, s, s') && exists s'' :: Total(s'') && big_step(c1, s', s'') && big_step(c2, s'', t);
+ // def. big_step
+ exists s' :: Total(s') && big_step(c0, s, s') && big_step(Seq(c1, c2), s', t);
+ // def. big_step
+ big_step(Seq(c0, Seq(c1, c2)), s, t);
+ }
+}
+
+predicate equiv_c(c: com, c': com)
+{
+ forall s,t :: Total(s) ==> big_step(c, s, t) == big_step(c', s, t)
+}
+
+lemma lemma_7_3(b: bexp, c: com)
+ ensures equiv_c(While(b, c), If(b, Seq(c, While(b, c)), SKIP))
+{
+}
+
+lemma lemma_7_4(b: bexp, c: com)
+ ensures equiv_c(If(b, c, c), c)
+{
+}
+
+lemma lemma_7_5(b: bexp, c: com, c': com)
+ requires equiv_c(c, c')
+ ensures equiv_c(While(b, c), While(b, c'))
+{
+ forall s,t | Total(s)
+ ensures big_step(While(b, c), s, t) == big_step(While(b, c'), s, t)
+ {
+ if big_step(While(b, c), s, t) {
+ lemma_7_6(b, c, c', s, t);
+ }
+ if big_step(While(b, c'), s, t) {
+ lemma_7_6(b, c', c, s, t);
+ }
+ }
+}
+
+inductive lemma lemma_7_6(b: bexp, c: com, c': com, s: state, t: state)
+ requires Total(s) && big_step(While(b, c), s, t) && equiv_c(c, c')
+ ensures big_step(While(b, c'), s, t)
+{
+ if !bval(b, s) {
+ // trivial
+ } else {
+ var s' :| Total(s') && big_step#[_k-1](c, s, s') && big_step#[_k-1](While(b, c), s', t);
+ lemma_7_6(b, c, c', s', t); // induction hypothesis
+ }
+}
+
+// equiv_c is an equivalence relation
+lemma equiv_c_reflexive(c: com, c': com)
+ ensures c == c' ==> equiv_c(c, c')
+{
+}
+lemma equiv_c_symmetric(c: com, c': com)
+ ensures equiv_c(c, c') ==> equiv_c(c', c)
+{
+}
+lemma equiv_c_transitive(c: com, c': com, c'': com)
+ ensures equiv_c(c, c') && equiv_c(c', c'') ==> equiv_c(c, c'')
+{
+}
+
+inductive lemma IMP_is_deterministic(c: com, s: state, t: state, t': state)
+ requires Total(s) && big_step(c, s, t) && big_step(c, s, t')
+ ensures t == t'
+{
+ match c
+ case SKIP =>
+ // trivial
+ case Assign(x, a) =>
+ // trivial
+ case Seq(c0, c1) =>
+ var s' :| Total(s') && big_step#[_k-1](c0, s, s') && big_step#[_k-1](c1, s', t);
+ var s'' :| Total(s'') && big_step#[_k-1](c0, s, s'') && big_step#[_k-1](c1, s'', t');
+ IMP_is_deterministic(c0, s, s', s'');
+ IMP_is_deterministic(c1, s', t, t');
+ case If(b, thn, els) =>
+ IMP_is_deterministic(if bval(b, s) then thn else els, s, t, t');
+ case While(b, body) =>
+ if !bval(b, s) {
+ // trivial
+ } else {
+ var s' :| Total(s') && big_step#[_k-1](body, s, s') && big_step#[_k-1](While(b, body), s', t);
+ var s'' :| Total(s'') && big_step#[_k-1](body, s, s'') && big_step#[_k-1](While(b, body), s'', t');
+ IMP_is_deterministic(body, s, s', s'');
+ IMP_is_deterministic(While(b, body), s', t, t');
+ }
+}
+
+// ----- Small-step semantics -----
+
+inductive predicate small_step(c: com, s: state, c': com, s': state)
+ requires Total(s)
+{
+ match c
+ case SKIP => false
+ case Assign(x, a) =>
+ c' == SKIP && s' == s[x := aval(a, s)]
+ case Seq(c0, c1) =>
+ (c0 == SKIP && c' == c1 && s' == s) ||
+ exists c0' :: c' == Seq(c0', c1) && small_step(c0, s, c0', s')
+ case If(b, thn, els) =>
+ c' == (if bval(b, s) then thn else els) && s' == s
+ case While(b, body) =>
+ c' == If(b, Seq(body, While(b, body)), SKIP) && s' == s
+}
+
+inductive lemma SmallStep_is_deterministic(cs: (com, state), cs': (com, state), cs'': (com, state))
+ requires Total(cs.1)
+ requires small_step(cs.0, cs.1, cs'.0, cs'.1)
+ requires small_step(cs.0, cs.1, cs''.0, cs''.1)
+ ensures cs' == cs''
+{
+ match cs.0
+ case Assign(x, a) =>
+ case Seq(c0, c1) =>
+ if c0 == SKIP {
+ } else {
+ var c0' :| cs'.0 == Seq(c0', c1) && small_step#[_k-1](c0, cs.1, c0', cs'.1);
+ var c0'' :| cs''.0 == Seq(c0'', c1) && small_step#[_k-1](c0, cs.1, c0'', cs''.1);
+ SmallStep_is_deterministic((c0, cs.1), (c0', cs'.1), (c0'', cs''.1));
+ }
+ case If(b, thn, els) =>
+ case While(b, body) =>
+}
+
+inductive lemma small_step_ends_in_Total_state(c: com, s: state, c': com, s': state)
+ requires Total(s) && small_step(c, s, c', s')
+ ensures Total(s')
+{
+ match c
+ case Assign(x, a) =>
+ case Seq(c0, c1) =>
+ if c0 != SKIP {
+ var c0' :| c' == Seq(c0', c1) && small_step(c0, s, c0', s');
+ small_step_ends_in_Total_state(c0, s, c0', s');
+ }
+ case If(b, thn, els) =>
+ case While(b, body) =>
+}
+
+inductive predicate small_step_star(c: com, s: state, c': com, s': state)
+ requires Total(s)
+{
+ (c == c' && s == s') ||
+ exists c'', s'' ::
+ small_step(c, s, c'', s'') &&
+ (small_step_ends_in_Total_state(c, s, c'', s''); small_step_star(c'', s'', c', s'))
+}
+
+inductive lemma small_step_star_ends_in_Total_state(c: com, s: state, c': com, s': state)
+ requires Total(s) && small_step_star(c, s, c', s')
+ ensures Total(s')
+{
+ if c == c' && s == s' {
+ } else {
+ var c'', s'' :| small_step(c, s, c'', s'') &&
+ (small_step_ends_in_Total_state(c, s, c'', s''); small_step_star#[_k-1](c'', s'', c', s'));
+ small_step_star_ends_in_Total_state(c'', s'', c', s');
+ }
+}
+
+lemma star_transitive(c0: com, s0: state, c1: com, s1: state, c2: com, s2: state)
+ requires Total(s0) && Total(s1)
+ requires small_step_star(c0, s0, c1, s1) && small_step_star(c1, s1, c2, s2)
+ ensures small_step_star(c0, s0, c2, s2)
+{
+ star_transitive_aux(c0, s0, c1, s1, c2, s2);
+}
+inductive lemma star_transitive_aux(c0: com, s0: state, c1: com, s1: state, c2: com, s2: state)
+ requires Total(s0) && Total(s1)
+ requires small_step_star(c0, s0, c1, s1)
+ ensures small_step_star(c1, s1, c2, s2) ==> small_step_star(c0, s0, c2, s2)
+{
+ if c0 == c1 && s0 == s1 {
+ } else {
+ var c', s' :|
+ small_step(c0, s0, c', s') &&
+ (small_step_ends_in_Total_state(c0, s0, c', s'); small_step_star#[_k-1](c', s', c1, s1));
+ star_transitive_aux(c', s', c1, s1, c2, s2);
+ }
+}
+
+// The big-step semantics can be simulated by some number of small steps
+inductive lemma BigStep_implies_SmallStepStar(c: com, s: state, t: state)
+ requires Total(s) && big_step(c, s, t)
+ ensures small_step_star(c, s, SKIP, t)
+{
+ match c
+ case SKIP =>
+ // trivial
+ case Assign(x, a) =>
+ assert t == s[x := aval(a, s)];
+ assert small_step(c, s, SKIP, t);
+ assert small_step_star(SKIP, t, SKIP, t);
+ case Seq(c0, c1) =>
+ var s' :| Total(s') && big_step#[_k-1](c0, s, s') && big_step#[_k-1](c1, s', t);
+ calc <== {
+ small_step_star(c, s, SKIP, t);
+ { star_transitive(Seq(c0, c1), s, Seq(SKIP, c1), s', SKIP, t); }
+ small_step_star(Seq(c0, c1), s, Seq(SKIP, c1), s') && small_step_star(Seq(SKIP, c1), s', SKIP, t);
+ { lemma_7_13(c0, s, SKIP, s', c1); }
+ small_step_star(c0, s, SKIP, s') && small_step_star(Seq(SKIP, c1), s', SKIP, t);
+ { BigStep_implies_SmallStepStar(c0, s, s'); }
+ small_step_star(Seq(SKIP, c1), s', SKIP, t);
+ { assert small_step(Seq(SKIP, c1), s', c1, s'); }
+ small_step_star(c1, s', SKIP, t);
+ { BigStep_implies_SmallStepStar(c1, s', t); }
+ true;
+ }
+ case If(b, thn, els) =>
+ BigStep_implies_SmallStepStar(if bval(b, s) then thn else els, s, t);
+ case While(b, body) =>
+ if !bval(b, s) && s == t {
+ calc <== {
+ small_step_star(c, s, SKIP, t);
+ { assert small_step(c, s, If(b, Seq(body, While(b, body)), SKIP), s); }
+ small_step_star(If(b, Seq(body, While(b, body)), SKIP), s, SKIP, t);
+ { assert small_step(If(b, Seq(body, While(b, body)), SKIP), s, SKIP, s); }
+ small_step_star(SKIP, s, SKIP, t);
+ true;
+ }
+ } else {
+ var s' :| Total(s') && big_step#[_k-1](body, s, s') && big_step#[_k-1](While(b, body), s', t);
+ calc <== {
+ small_step_star(c, s, SKIP, t);
+ { assert small_step(c, s, If(b, Seq(body, While(b, body)), SKIP), s); }
+ small_step_star(If(b, Seq(body, While(b, body)), SKIP), s, SKIP, t);
+ { assert small_step(If(b, Seq(body, While(b, body)), SKIP), s, Seq(body, While(b, body)), s); }
+ small_step_star(Seq(body, While(b, body)), s, SKIP, t);
+ { star_transitive(Seq(body, While(b, body)), s, Seq(SKIP, While(b, body)), s', SKIP, t); }
+ small_step_star(Seq(body, While(b, body)), s, Seq(SKIP, While(b, body)), s') && small_step_star(Seq(SKIP, While(b, body)), s', SKIP, t);
+ { lemma_7_13(body, s, SKIP, s', While(b, body)); }
+ small_step_star(body, s, SKIP, s') && small_step_star(Seq(SKIP, While(b, body)), s', SKIP, t);
+ { BigStep_implies_SmallStepStar(body, s, s'); }
+ small_step_star(Seq(SKIP, While(b, body)), s', SKIP, t);
+ { assert small_step(Seq(SKIP, While(b, body)), s', While(b, body), s'); }
+ small_step_star(While(b, body), s', SKIP, t);
+ { BigStep_implies_SmallStepStar(While(b, body), s', t); }
+ true;
+ }
+ }
+}
+
+inductive lemma lemma_7_13(c0: com, s0: state, c: com, t: state, c1: com)
+ requires Total(s0) && small_step_star(c0, s0, c, t)
+ ensures small_step_star(Seq(c0, c1), s0, Seq(c, c1), t)
+{
+ if c0 == c && s0 == t {
+ } else {
+ var c', s' :| small_step(c0, s0, c', s') && (small_step_ends_in_Total_state(c0, s0, c', s'); small_step_star#[_k-1](c', s', c, t));
+ lemma_7_13(c', s', c, t, c1);
+ }
+}
+
+inductive lemma SmallStepStar_implies_BigStep(c: com, s: state, t: state)
+ requires Total(s) && small_step_star(c, s, SKIP, t)
+ ensures big_step(c, s, t)
+{
+ if c == SKIP && s == t {
+ } else {
+ var c', s' :| small_step(c, s, c', s') && (small_step_ends_in_Total_state(c, s, c', s'); small_step_star#[_k-1](c', s', SKIP, t));
+ SmallStepStar_implies_BigStep(c', s', t);
+ SmallStep_plus_BigStep(c, s, c', s', t);
+ }
+}
+
+inductive lemma SmallStep_plus_BigStep(c: com, s: state, c': com, s': state, t: state)
+ requires Total(s) && Total(s') && small_step(c, s, c', s')
+ ensures big_step(c', s', t) ==> big_step(c, s, t)
+{
+ match c
+ case Assign(x, a) =>
+ case Seq(c0, c1) =>
+ if c0 == SKIP && c' == c1 && s' == s {
+ } else {
+ var c0' :| c' == Seq(c0', c1) && small_step(c0, s, c0', s');
+ if big_step(c', s', t) {
+ var k: nat :| big_step#[k](Seq(c0', c1), s', t);
+ var s'' :| Total(s'') && big_step(c0', s', s'') && big_step(c1, s'', t);
+ SmallStep_plus_BigStep(c0, s, c0', s', s'');
+ }
+ }
+ case If(b, thn, els) =>
+ case While(b, body) =>
+ assert c' == If(b, Seq(body, While(b, body)), SKIP) && s' == s;
+ if big_step(c', s', t) {
+ assert big_step(if bval(b, s') then Seq(body, While(b, body)) else SKIP, s', t);
+ }
+}
+
+// big-step and small-step semantics agree
+lemma BigStep_SmallStepStar_Same(c: com, s: state, t: state)
+ requires Total(s)
+ ensures big_step(c, s, t) <==> small_step_star(c, s, SKIP, t)
+{
+ if big_step(c, s, t) {
+ BigStep_implies_SmallStepStar(c, s, t);
+ }
+ if small_step_star(c, s, SKIP, t) {
+ SmallStepStar_implies_BigStep(c, s, t);
+ }
+}
+
+predicate final(c: com, s: state)
+ requires Total(s)
+{
+ !exists c',s' :: small_step(c, s, c', s')
+}
+
+// lemma 7.17:
+lemma final_is_skip(c: com, s: state)
+ requires Total(s)
+ ensures final(c, s) <==> c == SKIP
+{
+ if c == SKIP {
+ assert final(c, s);
+ } else {
+ var _, _ := only_skip_has_no_next_state(c, s);
+ }
+}
+lemma only_skip_has_no_next_state(c: com, s: state) returns (c': com, s': state)
+ requires Total(s) && c != SKIP
+ ensures small_step(c, s, c', s')
+{
+ match c
+ case SKIP =>
+ case Assign(x, a) =>
+ c', s' := SKIP, s[x := aval(a, s)];
+ case Seq(c0, c1) =>
+ if c0 == SKIP {
+ c', s' := c1, s;
+ } else {
+ c', s' := only_skip_has_no_next_state(c0, s);
+ c' := Seq(c', c1);
+ }
+ case If(b, thn, els) =>
+ c', s' := if bval(b, s) then thn else els, s;
+ case While(b, body) =>
+ c', s' := If(b, Seq(body, While(b, body)), SKIP), s;
+}
+
+lemma lemma_7_18(c: com, s: state)
+ requires Total(s)
+ ensures (exists t :: big_step(c, s, t)) <==>
+ (exists c',s' :: small_step_star(c, s, c', s') &&
+ (small_step_star_ends_in_Total_state(c, s, c', s'); final(c', s')))
+{
+ if exists t :: big_step(c, s, t) {
+ var t :| big_step(c, s, t);
+ BigStep_SmallStepStar_Same(c, s, t);
+ small_step_star_ends_in_Total_state(c, s, SKIP, t);
+ calc ==> {
+ true;
+ big_step(c, s, t);
+ small_step_star(c, s, SKIP, t);
+ { assert final(SKIP, t); }
+ small_step_star(c, s, SKIP, t) && final(SKIP, t);
+ }
+ }
+ if exists c',s' :: small_step_star(c, s, c', s') &&
+ (small_step_star_ends_in_Total_state(c, s, c', s'); final(c', s')) {
+ var c',s' :| small_step_star(c, s, c', s') &&
+ (small_step_star_ends_in_Total_state(c, s, c', s'); final(c', s'));
+ final_is_skip(c', s');
+ BigStep_SmallStepStar_Same(c, s, s');
+ }
+}
diff --git a/Test/dafny4/NipkowKlein-chapter7.dfy.expect b/Test/dafny4/NipkowKlein-chapter7.dfy.expect new file mode 100644 index 00000000..e08b3632 --- /dev/null +++ b/Test/dafny4/NipkowKlein-chapter7.dfy.expect @@ -0,0 +1,2 @@ +
+Dafny program verifier finished with 54 verified, 0 errors
diff --git a/Test/hofs/ReadsReads.dfy b/Test/hofs/ReadsReads.dfy index d0a8b43b..e11473bd 100644 --- a/Test/hofs/ReadsReads.dfy +++ b/Test/hofs/ReadsReads.dfy @@ -28,12 +28,12 @@ module ReadsRequiresReads { function MyReadsBad(f : A -> B, a : A) : set<object> { - f.reads(a) + f.reads(a) // error: MyReadsBad does not have permission to read what f.reads(a) reads } function MyReadsBad2(f : A -> B, a : A) : set<object> { - (f.reads)(a) + (f.reads)(a) // error: MyReadsBad2 does not have permission to read what f.reads(a) reads } function MyReadsOk'(f : A -> B, a : A, o : object) : bool @@ -44,7 +44,7 @@ module ReadsRequiresReads { function MyReadsBad'(f : A -> B, a : A, o : object) : bool { - o in f.reads(a) + o in f.reads(a) // error: MyReadsBad' does not have permission to read what f.reads(a) reads } function MyRequiresOk(f : A -> B, a : A) : bool @@ -55,7 +55,7 @@ module ReadsRequiresReads { function MyRequiresBad(f : A -> B, a : A) : bool { - f.requires(a) + f.requires(a) // error: MyRequiresBad does not have permission to read what f.requires(a) reads } } @@ -64,6 +64,7 @@ module WhatWeKnowAboutReads { lemma IndeedNothing() { assert ReadsNothing.reads() == {}; + assert ((ReadsNothing).reads)() == {}; } method NothingHere() { @@ -83,9 +84,9 @@ module WhatWeKnowAboutReads { var s' := new S; if * { assert s in ReadsSomething.reads(s) || ReadsSomething.reads(s) == {}; } else if * { assert s in ReadsSomething.reads(s); - } else if * { assert ReadsSomething.reads(s) == {}; + } else if * { assert ReadsSomething.reads(s) == {}; // error } else if * { assert s' !in ReadsSomething.reads(s); - } else if * { assert s' in ReadsSomething.reads(s); + } else if * { assert s' in ReadsSomething.reads(s); // error } } @@ -95,9 +96,9 @@ module WhatWeKnowAboutReads { var f := (u) reads u => (); if * { assert s in f.reads(s) || f.reads(s) == {}; } else if * { assert s in f.reads(s); - } else if * { assert f.reads(s) == {}; + } else if * { assert f.reads(s) == {}; // error } else if * { assert s' !in f.reads(s); - } else if * { assert s' in f.reads(s); + } else if * { assert s' in f.reads(s); // error } } } @@ -131,3 +132,11 @@ module ReadsAll { f(0) + f(1) + f(2) } } + +module ReadsOnFunctions { + lemma Requires_Reads_What_Function_Reads(f: int -> int) + { + var g := f.requires; + assert g.reads(10) == f.reads(10); + } +} diff --git a/Test/hofs/ReadsReads.dfy.expect b/Test/hofs/ReadsReads.dfy.expect index 44a95b6d..73002b73 100644 --- a/Test/hofs/ReadsReads.dfy.expect +++ b/Test/hofs/ReadsReads.dfy.expect @@ -14,26 +14,23 @@ ReadsReads.dfy(58,7): Error: insufficient reads clause to invoke function Execution trace:
(0,0): anon0
(0,0): anon3_Else
-ReadsReads.dfy(66,33): Error: assertion violation
-Execution trace:
- (0,0): anon0
-ReadsReads.dfy(86,50): Error: assertion violation
+ReadsReads.dfy(87,50): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon16_Then
-ReadsReads.dfy(88,29): Error: assertion violation
+ReadsReads.dfy(89,29): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon18_Then
-ReadsReads.dfy(98,37): Error: assertion violation
+ReadsReads.dfy(99,37): Error: assertion violation
Execution trace:
(0,0): anon0
- ReadsReads.dfy(95,14): anon15_Else
+ ReadsReads.dfy(96,14): anon15_Else
(0,0): anon19_Then
-ReadsReads.dfy(100,29): Error: assertion violation
+ReadsReads.dfy(101,29): Error: assertion violation
Execution trace:
(0,0): anon0
- ReadsReads.dfy(95,14): anon15_Else
+ ReadsReads.dfy(96,14): anon15_Else
(0,0): anon21_Then
-Dafny program verifier finished with 17 verified, 9 errors
+Dafny program verifier finished with 20 verified, 8 errors
|