Dafny induction:

* implemented induction tactic for result-less, non-mutating ghost methods
* refine heuristics for determining if a variables is usefully passed to a recursive function
* disallow certain "ensures" to use two-state features (needed for soundness of the parallel-statement translation, see comments in Resolver.cs and ParallelResolveErrors.dfy)
* added command-line flags /induction and /inductionHeuristic (everything is on by default)

6 files changed, 177 insertions, 68 deletions

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 04d60716..b2914776 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -970,7 +970,11 @@ ParallelResolveErrors.dfy(72,20): Error: trying to break out of more loop levels
 ParallelResolveErrors.dfy(73,20): Error: break label is undefined or not in scope: OutsideLoop

 ParallelResolveErrors.dfy(82,24): Error: trying to break out of more loop levels than there are enclosing loops

 ParallelResolveErrors.dfy(83,24): Error: break label is undefined or not in scope: OutsideLoop

-13 resolution/type errors detected in ParallelResolveErrors.dfy

+ParallelResolveErrors.dfy(94,43): Error: fresh expressions are not allowed in this context

+ParallelResolveErrors.dfy(101,50): Error: old expressions are not allowed in this context

+ParallelResolveErrors.dfy(124,12): Error: old expressions are not allowed in this context

+ParallelResolveErrors.dfy(144,45): Error: fresh expressions are not allowed in this context

+17 resolution/type errors detected in ParallelResolveErrors.dfy

 

 -------------------- Parallel.dfy --------------------

 Parallel.dfy(31,5): Error BP5002: A precondition for this call might not hold.

@@ -1051,7 +1055,7 @@ Execution trace:
     (0,0): anon20_Then

     (0,0): anon5

 

-Dafny program verifier finished with 20 verified, 8 errors

+Dafny program verifier finished with 24 verified, 8 errors

 

 -------------------- TypeParameters.dfy --------------------

 TypeParameters.dfy(44,22): Error: assertion violation

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 817120ce..539974fd 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -187,3 +187,14 @@ method DuplicateUpdate() {
     }

   }

 }

+

+ghost method DontDoMuch(x: int)

+{

+}

+

+method OmittedRange() {

+  parallel (x) { }

+  parallel (x) {

+    DontDoMuch(x);

+  }

+}

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index 4e0be32e..9afa311a 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -85,3 +85,67 @@ method M1() {
     }

   }

 }

+

+// -------------------------------------------------------------------------------------

+// Some soundness considerations

+// -------------------------------------------------------------------------------------

+

+ghost static method X_M0(y: int)

+  ensures exists o: object :: o != null && fresh(o);  // error: not allowed 'fresh' here

+{

+  var p := new object;

+}

+

+class X_C { ghost var data: int; }

+ghost static method X_M1(y: int)

+  ensures exists c: X_C :: c != null && c.data != old(c.data);  // error: not allowed 'old' here

+{

+  var c := new X_C;

+  c.data := c.data + 1;

+}

+

+method X_Main() {

+  if (*) {

+    parallel (x) { X_M0(x); }

+  } else {

+    parallel (x) { X_M1(x); }

+  }

+  assert false;

+}

+

+

+// The following seems to be a legitimate use of a two-state predicate in the postcondition of the parallel statement

+method X_Legit(c: X_C)

+  requires c != null;

+  modifies c;

+{

+  c.data := c.data + 1;

+  parallel (x | c.data <= x)

+    ensures old(c.data) < x;  // error: not allowed 'old' here

+  {

+  }

+}

+

+// X_M2 is like X_M0, but with an out-parameter

+ghost static method X_M2(y: int) returns (r: int)

+  ensures exists o: object :: o != null && fresh(o);  // 'fresh' is allowed here (because there's something coming "out" of this ghost method, namely 'r'

+{

+  var p := new object;

+}

+

+// The following method exhibits a case where M2 and a two-state parallel ensures would lead to an unsoundness

+// with the current translation.

+method X_AnotherMain(c: X_C)

+  requires c != null;

+  modifies c;

+{

+  c.data := c.data + 1;

+  parallel (x: int)

+    ensures exists o: object :: o != null && fresh(o);  // error: not allowed 'fresh' here

+  {

+    var s := X_M2(x);

+  }

+  assert false;

+}

+

+// -------------------------------------------------------------------------------------

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 0a99ca95..d53ae14b 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -81,11 +81,11 @@ Dafny program verifier finished with 6 verified, 0 errors
 

 -------------------- Induction.dfy --------------------

 

-Dafny program verifier finished with 29 verified, 0 errors

+Dafny program verifier finished with 33 verified, 0 errors

 

 -------------------- Rippling.dfy --------------------

 

-Dafny program verifier finished with 137 verified, 0 errors

+Dafny program verifier finished with 141 verified, 0 errors

 

 -------------------- MoreInduction.dfy --------------------

 

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 15cc1ffe..3585dde6 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -56,6 +56,23 @@ class IntegerInduction {
   {

   }

 

+  // The following two ghost methods are the same as the previous two, but

+  // here no body is given--and the proof still goes through (thanks to

+  // Dafny's ghost-method induction tactic).

+

+  ghost method Lemma_Auto(n: int)

+    requires 0 <= n;

+    ensures 2 * Gauss(n) == n*(n+1);

+  {

+  }

+

+  ghost method Theorem1_Auto(n: int)

+    requires 0 <= n;

+    ensures SumOfCubes(n) == Gauss(n) * Gauss(n);

+    ensures 2 * Gauss(n) == n*(n+1);

+  {

+  }

+

   // Here is another proof.  It makes use of Dafny's induction heuristics to

   // prove the lemma.

 

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 6f6a7ba7..4a1c4bbe 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -298,248 +298,248 @@ function AlwaysTrueFunction(): FunctionValue
 // -----------------------------------------------------------------------------------

 

 ghost method P1()

-  ensures (forall n, xs :: concat(take(n, xs), drop(n, xs)) == xs);

+  ensures forall n, xs :: concat(take(n, xs), drop(n, xs)) == xs;

 {

 }

 

 ghost method P2()

-  ensures (forall n, xs, ys :: add(count(n, xs), count(n, ys)) == count(n, (concat(xs, ys))));

+  ensures forall n, xs, ys :: add(count(n, xs), count(n, ys)) == count(n, (concat(xs, ys)));

 {

 }

 

 ghost method P3()

-  ensures (forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == True);

+  ensures forall n, xs, ys :: leq(count(n, xs), count(n, concat(xs, ys))) == True;

 {

 }

 

 ghost method P4()

-  ensures (forall n, xs :: add(Suc(Zero), count(n, xs)) == count(n, Cons(n, xs)));

+  ensures forall n, xs :: add(Suc(Zero), count(n, xs)) == count(n, Cons(n, xs));

 {

 }

 

 ghost method P5()

-  ensures (forall n, xs, x ::

+  ensures forall n, xs, x ::

     add(Suc(Zero), count(n, xs)) == count(n, Cons(x, xs))

-    ==> n == x);

+    ==> n == x;

 {

 }

 

 ghost method P6()

-  ensures (forall m, n :: minus(n, add(n, m)) == Zero);

+  ensures forall m, n :: minus(n, add(n, m)) == Zero;

 {

 }

 

 ghost method P7()

-  ensures (forall m, n :: minus(add(n, m), n) == m);

+  ensures forall m, n :: minus(add(n, m), n) == m;

 {

 }

 

 ghost method P8()

-  ensures (forall k, m, n :: minus(add(k, m), add(k, n)) == minus(m, n));

+  ensures forall k, m, n :: minus(add(k, m), add(k, n)) == minus(m, n);

 {

 }

 

 ghost method P9()

-  ensures (forall i, j, k :: minus(minus(i, j), k) == minus(i, add(j, k)));

+  ensures forall i, j, k :: minus(minus(i, j), k) == minus(i, add(j, k));

 {

 }

 

 ghost method P10()

-  ensures (forall m :: minus(m, m) == Zero);

+  ensures forall m :: minus(m, m) == Zero;

 {

 }

 

 ghost method P11()

-  ensures (forall xs :: drop(Zero, xs) == xs);

+  ensures forall xs :: drop(Zero, xs) == xs;

 {

 }

 

 ghost method P12()

-  ensures (forall n, xs, f :: drop(n, map(f, xs)) == map(f, drop(n, xs)));

+  ensures forall n, xs, f :: drop(n, map(f, xs)) == map(f, drop(n, xs));

 {

 }

 

 ghost method P13()

-  ensures (forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs));

+  ensures forall n, x, xs :: drop(Suc(n), Cons(x, xs)) == drop(n, xs);

 {

 }

 

 ghost method P14()

-  ensures (forall xs, ys, p :: filter(p, concat(xs, ys)) == concat(filter(p, xs), filter(p, ys)));

+  ensures forall xs, ys, p :: filter(p, concat(xs, ys)) == concat(filter(p, xs), filter(p, ys));

 {

 }

 

 ghost method P15()

-  ensures (forall x, xs :: len(ins(x, xs)) == Suc(len(xs)));

+  ensures forall x, xs :: len(ins(x, xs)) == Suc(len(xs));

 {

 }

 

 ghost method P16()

-  ensures (forall x, xs :: xs == Nil ==> last(Cons(x, xs)) == x);

+  ensures forall x, xs :: xs == Nil ==> last(Cons(x, xs)) == x;

 {

 }

 

 ghost method P17()

-  ensures (forall n :: leq(n, Zero) == True <==> n == Zero);

+  ensures forall n :: leq(n, Zero) == True <==> n == Zero;

 {

 }

 

 ghost method P18()

-  ensures (forall i, m :: less(i, Suc(add(i, m))) == True);

+  ensures forall i, m :: less(i, Suc(add(i, m))) == True;

 {

 }

 

 ghost method P19()

-  ensures (forall n, xs :: len(drop(n, xs)) == minus(len(xs), n));

+  ensures forall n, xs :: len(drop(n, xs)) == minus(len(xs), n);

 {

 }

 

 ghost method P20()

-  ensures (forall xs :: len(sort(xs)) == len(xs));

+  ensures forall xs :: len(sort(xs)) == len(xs);

 {

   // proving this theorem requires an additional lemma:

-  assert (forall k, ks :: len(ins(k, ks)) == len(Cons(k, ks)));

+  assert forall k, ks :: len(ins(k, ks)) == len(Cons(k, ks));

   // ...and one manually introduced case study:

-  assert (forall ys ::

+  assert forall ys ::

            sort(ys) == Nil ||

-           (exists z, zs :: sort(ys) == Cons(z, zs)));

+           exists z, zs :: sort(ys) == Cons(z, zs);

 }

 

 ghost method P21()

-  ensures (forall n, m :: leq(n, add(n, m)) == True);

+  ensures forall n, m :: leq(n, add(n, m)) == True;

 {

 }

 

 ghost method P22()

-  ensures (forall a, b, c :: max(max(a, b), c) == max(a, max(b, c)));

+  ensures forall a, b, c :: max(max(a, b), c) == max(a, max(b, c));

 {

 }

 

 ghost method P23()

-  ensures (forall a, b :: max(a, b) == max(b, a));

+  ensures forall a, b :: max(a, b) == max(b, a);

 {

 }

 

 ghost method P24()

-  ensures (forall a, b :: max(a, b) == a <==> leq(b, a) == True);

+  ensures forall a, b :: max(a, b) == a <==> leq(b, a) == True;

 {

 }

 

 ghost method P25()

-  ensures (forall a, b :: max(a, b) == b <==> leq(a, b) == True);

+  ensures forall a, b :: max(a, b) == b <==> leq(a, b) == True;

 {

 }

 

 ghost method P26()

-  ensures (forall x, xs, ys :: mem(x, xs) == True ==> mem(x, concat(xs, ys)) == True);

+  ensures forall x, xs, ys :: mem(x, xs) == True ==> mem(x, concat(xs, ys)) == True;

 {

 }

 

 ghost method P27()

-  ensures (forall x, xs, ys :: mem(x, ys) == True ==> mem(x, concat(xs, ys)) == True);

+  ensures forall x, xs, ys :: mem(x, ys) == True ==> mem(x, concat(xs, ys)) == True;

 {

 }

 

 ghost method P28()

-  ensures (forall x, xs :: mem(x, concat(xs, Cons(x, Nil))) == True);

+  ensures forall x, xs :: mem(x, concat(xs, Cons(x, Nil))) == True;

 {

 }

 

 ghost method P29()

-  ensures (forall x, xs :: mem(x, ins1(x, xs)) == True);

+  ensures forall x, xs :: mem(x, ins1(x, xs)) == True;

 {

 }

 

 ghost method P30()

-  ensures (forall x, xs :: mem(x, ins(x, xs)) == True);

+  ensures forall x, xs :: mem(x, ins(x, xs)) == True;

 {

 }

 

 ghost method P31()

-  ensures (forall a, b, c :: min(min(a, b), c) == min(a, min(b, c)));

+  ensures forall a, b, c :: min(min(a, b), c) == min(a, min(b, c));

 {

 }

 

 ghost method P32()

-  ensures (forall a, b :: min(a, b) == min(b, a));

+  ensures forall a, b :: min(a, b) == min(b, a);

 {

 }

 

 ghost method P33()

-  ensures (forall a, b :: min(a, b) == a <==> leq(a, b) == True);

+  ensures forall a, b :: min(a, b) == a <==> leq(a, b) == True;

 {

 }

 

 ghost method P34()

-  ensures (forall a, b :: min(a, b) == b <==> leq(b, a) == True);

+  ensures forall a, b :: min(a, b) == b <==> leq(b, a) == True;

 {

 }

 

 ghost method P35()

-  ensures (forall xs :: dropWhileAlways(AlwaysFalseFunction(), xs) == xs);

+  ensures forall xs :: dropWhileAlways(AlwaysFalseFunction(), xs) == xs;

 {

 }

 

 ghost method P36()

-  ensures (forall xs :: takeWhileAlways(AlwaysTrueFunction(), xs) == xs);

+  ensures forall xs :: takeWhileAlways(AlwaysTrueFunction(), xs) == xs;

 {

 }

 

 ghost method P37()

-  ensures (forall x, xs :: not(mem(x, delete(x, xs))) == True);

+  ensures forall x, xs :: not(mem(x, delete(x, xs))) == True;

 {

 }

 

 ghost method P38()

-  ensures (forall n, xs :: count(n, concat(xs, Cons(n, Nil))) == Suc(count(n, xs)));

+  ensures forall n, xs :: count(n, concat(xs, Cons(n, Nil))) == Suc(count(n, xs));

 {

 }

 

 ghost method P39()

-  ensures (forall n, x, xs ::

-            add(count(n, Cons(x, Nil)), count(n, xs)) == count(n, Cons(x, xs)));

+  ensures forall n, x, xs ::

+            add(count(n, Cons(x, Nil)), count(n, xs)) == count(n, Cons(x, xs));

 {

 }

 

 ghost method P40()

-  ensures (forall xs :: take(Zero, xs) == Nil);

+  ensures forall xs :: take(Zero, xs) == Nil;

 {

 }

 

 ghost method P41()

-  ensures (forall n, xs, f :: take(n, map(f, xs)) == map(f, take(n, xs)));

+  ensures forall n, xs, f :: take(n, map(f, xs)) == map(f, take(n, xs));

 {

 }

 

 ghost method P42()

-  ensures (forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs)));

+  ensures forall n, x, xs :: take(Suc(n), Cons(x, xs)) == Cons(x, take(n, xs));

 {

 }

 

 ghost method P43(p: FunctionValue)

-  ensures (forall xs :: concat(takeWhileAlways(p, xs), dropWhileAlways(p, xs)) == xs);

+  ensures forall xs :: concat(takeWhileAlways(p, xs), dropWhileAlways(p, xs)) == xs;

 {

 }

 

 ghost method P44()

-  ensures (forall x, xs, ys :: zip(Cons(x, xs), ys) == zipConcat(x, xs, ys));

+  ensures forall x, xs, ys :: zip(Cons(x, xs), ys) == zipConcat(x, xs, ys);

 {

 }

 

 ghost method P45()

-  ensures (forall x, xs, y, ys ::

+  ensures forall x, xs, y, ys ::

             zip(Cons(x, xs), Cons(y, ys)) ==

-            PCons(Pair.Pair(x, y), zip(xs, ys)));

+            PCons(Pair.Pair(x, y), zip(xs, ys));

 {

 }

 

 ghost method P46()

-  ensures (forall ys :: zip(Nil, ys) == PNil);

+  ensures forall ys :: zip(Nil, ys) == PNil;

 {

 }

 

 ghost method P47()

-  ensures (forall a :: height(mirror(a)) == height(a));

+  ensures forall a :: height(mirror(a)) == height(a);

 {

   // proving this theorem requires a previously proved lemma:

   P23();

@@ -548,40 +548,53 @@ ghost method P47()
 // ...

 

 ghost method P54()

-  ensures (forall m, n :: minus(add(m, n), n) == m);

+  ensures forall m, n :: minus(add(m, n), n) == m;

 {

   // the proof of this theorem follows from two lemmas:

-  assert (forall m, n :: minus(add(n, m), n) == m);

-  assert (forall m, n :: add(m, n) == add(n, m));

+  assert forall m, n :: minus(add(n, m), n) == m;

+  assert forall m, n :: add(m, n) == add(n, m);

 }

 

 ghost method P65()

-  ensures (forall i, m :: less(i, Suc(add(m, i))) == True);

+  ensures forall i, m :: less(i, Suc(add(m, i))) == True;

 {

   if (*) {

     // the proof of this theorem follows from two lemmas:

-    assert (forall i, m :: less(i, Suc(add(i, m))) == True);

-    assert (forall m, n :: add(m, n) == add(n, m));

+    assert forall i, m :: less(i, Suc(add(i, m))) == True;

+    assert forall m, n :: add(m, n) == add(n, m);

   } else {

     // a different way to prove it uses the following lemma:

-    assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));

+    assert forall x,y :: add(x, Suc(y)) == Suc(add(x,y));

   }

 }

 

 ghost method P67()

-  ensures (forall m, n :: leq(n, add(m, n)) == True);

+  ensures forall m, n :: leq(n, add(m, n)) == True;

 {

   if (*) {

     // the proof of this theorem follows from two lemmas:

-    assert (forall m, n :: leq(n, add(n, m)) == True);

-    assert (forall m, n :: add(m, n) == add(n, m));

+    assert forall m, n :: leq(n, add(n, m)) == True;

+    assert forall m, n :: add(m, n) == add(n, m);

   } else {

     // a different way to prove it uses the following lemma:

-    assert (forall x,y :: add(x, Suc(y)) == Suc(add(x,y)));

+    assert forall x,y :: add(x, Suc(y)) == Suc(add(x,y));

   }

 }

 

 // ---------

+// Here is a alternate way of writing down the proof obligations:

+

+ghost method P1_alt(n: Nat, xs: List)

+  ensures concat(take(n, xs), drop(n, xs)) == xs;

+{

+}

+

+ghost method P2_alt(n: Nat, xs: List, ys: List)

+  ensures add(count(n, xs), count(n, ys)) == count(n, (concat(xs, ys)));

+{

+}

+

+// ---------

 

 ghost method Lemma_RevConcat(xs: List, ys: List)

   ensures reverse(concat(xs, ys)) == concat(reverse(ys), reverse(xs));