Dafny: Added two additional heuristics for guessing missing loop decreases clauses (for loop guard A!=B and for loop guards with multiple conjuncts)

12 files changed, 190 insertions, 93 deletions

diff --git a/Test/VSI-Benchmarks/b1.dfy b/Test/VSI-Benchmarks/b1.dfy
index 1ab76a78..cd4a18c2 100644
--- a/Test/VSI-Benchmarks/b1.dfy
+++ b/Test/VSI-Benchmarks/b1.dfy
@@ -1,75 +1,71 @@
-// Note: To prove termination of calls, methods need

-// a termination measure, but Dafny does not yet support

-// termination measures for methods (but it will in

-// the foreseeable future).

-

 // Spec# and Boogie and Chalice:  The program will be

 // the same, except that these languages do not check

-// for any kind of termination.

+// for any kind of termination.  Also, in Spec#, there

+// is an issue of potential overflows.

+

+// Benchmark1

 

-class Benchmark1 {

-  method Add(x: int, y: int) returns (r: int)

-    ensures r == x+y;

-  {

-    r := x;

-    if (y < 0) {

-      var n := y;

-      while (n != 0)

-        invariant r == x+y-n && 0 <= -n;

-        decreases -n;

-      {

-        r := r - 1;

-        n := n + 1;

-      }

-    } else {

-      var n := y;

-      while (n != 0)

-        invariant r == x+y-n && 0 <= n;

-        decreases n;

-      {

-        r := r + 1;

-        n := n - 1;

-      }

+method Add(x: int, y: int) returns (r: int)

+  ensures r == x+y;

+{

+  r := x;

+  if (y < 0) {

+    var n := y;

+    while (n != 0)

+      invariant r == x+y-n && 0 <= -n;

+    {

+      r := r - 1;

+      n := n + 1;

+    }

+  } else {

+    var n := y;

+    while (n != 0)

+      invariant r == x+y-n && 0 <= n;

+    {

+      r := r + 1;

+      n := n - 1;

     }

   }

+}

 

-  method Mul(x: int, y: int) returns (r: int)

-    ensures r == x*y;

-    decreases x < 0, x;

-  {

-    if (x == 0) {

-      r := 0;

-    } else if (x < 0) {

-      call r := Mul(-x, y);

-      r := -r;

-    } else {

-      call r := Mul(x-1, y);

-      call r := Add(r, y);

-    }

+method Mul(x: int, y: int) returns (r: int)

+  ensures r == x*y;

+  decreases x < 0, x;

+{

+  if (x == 0) {

+    r := 0;

+  } else if (x < 0) {

+    call r := Mul(-x, y);

+    r := -r;

+  } else {

+    call r := Mul(x-1, y);

+    call r := Add(r, y);

   }

+}

 

-  method Main() {

-    call TestAdd(3, 180);

-    call TestAdd(3, -180);

-    call TestAdd(0, 1);

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

 

-    call TestMul(3, 180);

-    call TestMul(3, -180);

-    call TestMul(180, 3);

-    call TestMul(-180, 3);

-    call TestMul(0, 1);

-    call TestMul(1, 0);

-  }

+method Main() {

+  call TestAdd(3, 180);

+  call TestAdd(3, -180);

+  call TestAdd(0, 1);

 

-  method TestAdd(x: int, y: int) {

-    print x, " + ", y, " = ";

-    call z := Add(x, y);

-    print z, "\n";

-  }

+  call TestMul(3, 180);

+  call TestMul(3, -180);

+  call TestMul(180, 3);

+  call TestMul(-180, 3);

+  call TestMul(0, 1);

+  call TestMul(1, 0);

+}

 

-  method TestMul(x: int, y: int) {

-    print x, " * ", y, " = ";

-    call z := Mul(x, y);

-    print z, "\n";

-  }

+method TestAdd(x: int, y: int) {

+  print x, " + ", y, " = ";

+  call z := Add(x, y);

+  print z, "\n";

+}

+

+method TestMul(x: int, y: int) {

+  print x, " * ", y, " = ";

+  call z := Mul(x, y);

+  print z, "\n";

 }

diff --git a/Test/VSI-Benchmarks/b2.dfy b/Test/VSI-Benchmarks/b2.dfy
index fd20a72b..1021ee85 100644
--- a/Test/VSI-Benchmarks/b2.dfy
+++ b/Test/VSI-Benchmarks/b2.dfy
@@ -14,7 +14,6 @@ class Benchmark2 {
       invariant 0 <= low && low <= high && high <= |a|;

       invariant (forall i :: 0 <= i && i < low ==> a[i] < key);

       invariant (forall i :: high <= i && i < |a| ==> key < a[i]);

-      decreases high - low;

     {

       var mid := low + (high - low) / 2;

       var midVal := a[mid];

diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy
index 6d9c3ddd..d9acfe04 100644
--- a/Test/VSI-Benchmarks/b3.dfy
+++ b/Test/VSI-Benchmarks/b3.dfy
@@ -88,8 +88,6 @@ class Benchmark3 {
       // the current array is that permutation of the input array

       invariant (forall i: int :: 0 <= i && i < |perm| ==> r.contents[i] == old(q.contents)[perm[i]]);

       invariant (forall i: int :: 0 <= i && i < |p| ==> q.contents[i] == old(q.contents)[p[i]]);

-   

-    decreases |q.contents|;

     {  

       call m,k := RemoveMin(q);

       perm := perm + [p[k]]; //adds  index of min to perm

diff --git a/Test/VSI-Benchmarks/b8.dfy b/Test/VSI-Benchmarks/b8.dfy
index 34e0cfef..a37f86e4 100644
--- a/Test/VSI-Benchmarks/b8.dfy
+++ b/Test/VSI-Benchmarks/b8.dfy
@@ -78,14 +78,13 @@ class Glossary {
     var wr := new WriterStream;

     call wr.Create();

     

-    while (0<|q.contents|)

+    while (0 < |q.contents|)

       invariant wr.Valid() && fresh(wr.footprint);

       invariant glossary.Valid();

       invariant glossary !in wr.footprint && null !in glossary.keys;

       invariant (forall d :: d in glossary.values ==> null !in d);

       invariant q !in wr.footprint;

       invariant (forall k :: k in q.contents ==> k in glossary.keys);

-      decreases |q.contents|;

     {

       call term := q.Dequeue();

       call present,definition := glossary.Find(term);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index cc248c20..7456ffaa 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -101,26 +101,26 @@ Execution trace:
     SmallTests.dfy(81,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-SmallTests.dfy(95,5): Error: call may violate caller's modifies clause

+SmallTests.dfy(116,5): Error: call may violate caller's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon3

-SmallTests.dfy(108,7): Error: call may violate caller's modifies clause

+SmallTests.dfy(129,7): Error: call may violate caller's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-SmallTests.dfy(110,7): Error: call may violate caller's modifies clause

+SmallTests.dfy(131,7): Error: call may violate caller's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Else

-SmallTests.dfy(150,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

+SmallTests.dfy(171,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon3

 

-Dafny program verifier finished with 24 verified, 9 errors

+Dafny program verifier finished with 28 verified, 9 errors

 

 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

@@ -226,7 +226,7 @@ Execution trace:
     (0,0): anon16_LoopBody

     Definedness.dfy(151,5): anon17_Else

     (0,0): anon9

-Definedness.dfy(172,44): Error: loop invariant must be well defined

+Definedness.dfy(170,44): Error: loop invariant must be well defined

 Execution trace:

     (0,0): anon0

     Definedness.dfy(162,5): anon16_LoopHead

@@ -235,28 +235,28 @@ Execution trace:
     (0,0): anon3

     (0,0): anon18_Then

     (0,0): anon6

-    Definedness.dfy(170,5): anon19_LoopHead

+    Definedness.dfy(169,5): anon19_LoopHead

     (0,0): anon19_LoopBody

     (0,0): anon20_Then

-Definedness.dfy(193,21): Error: collection expression must be well defined

+Definedness.dfy(191,21): Error: collection expression must be well defined

 Execution trace:

     (0,0): anon0

-Definedness.dfy(195,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

+Definedness.dfy(193,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

-Definedness.dfy(197,33): Error: range expression must be well defined

+Definedness.dfy(195,33): Error: range expression must be well defined

 Execution trace:

     (0,0): anon0

-Definedness.dfy(203,18): Error: RHS of assignment must be well defined

+Definedness.dfy(201,18): Error: RHS of assignment must be well defined

 Execution trace:

     (0,0): anon0

-Definedness.dfy(212,23): Error: loop invariant must be well defined

+Definedness.dfy(210,23): Error: loop invariant must be well defined

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(210,5): anon7_LoopHead

+    Definedness.dfy(208,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(212,23): Error BP5004: This loop invariant might not hold on entry.

+Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

 

@@ -335,8 +335,44 @@ Execution trace:
 Dafny program verifier finished with 2 verified, 1 error

 

 -------------------- Termination.dfy --------------------

+Termination.dfy(102,3): Error: cannot prove termination; try supplying a decreases clause for the loop

+Execution trace:

+    (0,0): anon0

+    Termination.dfy(102,3): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    Termination.dfy(102,3): anon8_Else

+    (0,0): anon3

+    Termination.dfy(102,12): anon9_Else

+    (0,0): anon5

+Termination.dfy(110,3): Error: cannot prove termination; try supplying a decreases clause for the loop

+Execution trace:

+    (0,0): anon0

+    Termination.dfy(110,3): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    Termination.dfy(110,3): anon8_Else

+    (0,0): anon3

+    Termination.dfy(110,16): anon9_Else

+    (0,0): anon5

+Termination.dfy(119,3): Error: decreases expression might not decrease

+Execution trace:

+    (0,0): anon0

+    Termination.dfy(119,3): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    Termination.dfy(119,3): anon8_Else

+    (0,0): anon3

+    Termination.dfy(119,16): anon9_Else

+    (0,0): anon5

+Termination.dfy(120,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

+Execution trace:

+    (0,0): anon0

+    Termination.dfy(119,3): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    Termination.dfy(119,3): anon8_Else

+    (0,0): anon3

+    Termination.dfy(119,16): anon9_Else

+    (0,0): anon5

 

-Dafny program verifier finished with 13 verified, 0 errors

+Dafny program verifier finished with 22 verified, 4 errors

 

 -------------------- Use.dfy --------------------

 Use.dfy(16,18): Error: assertion violation

@@ -363,7 +399,7 @@ Execution trace:
 Use.dfy(138,5): Error: assertion violation

 Execution trace:

     (0,0): anon0

-Use.dfy(209,19): Error: assertion violation

+Use.dfy(208,19): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index b69fa4f6..d557de21 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -161,14 +161,12 @@ class StatementTwoShoes {
     var i := 0;

     while (i < 100)

       invariant i <= 100;

-      decreases 100 - i;

       invariant F(123 - i) == this;

     {

       i := i + 1;

     }

     i := 0;

     while (i < 100)

-      decreases 100 - i;

       invariant F(if i==77 then -3 else i) == this;  // error: expression may not be well defined

     {

       i := i + 1;

@@ -210,7 +208,6 @@ class StatementTwoShoes {
     while (i < 100)

       // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking

       invariant 5 / x != 5 / x;  // error: not well-defined, and error: loop invariant does not hold initially

-      decreases 100 - i;

     {

       i := i + 1;

     }

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 4e3fab69..87bfd35f 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -85,6 +85,27 @@ class Modifies {
     }

   }

 

+  method Aprime(p: Modifies)

+    modifies this, p;

+  {

+    x := x + 1;

+    while (p != null && p.x < 75)

+      decreases if p != null then 75 - p.x else 0;  // given explicitly (but see Adoubleprime below)

+    {

+      p.x := p.x + 1;

+    }

+  }

+

+  method Adoubleprime(p: Modifies)

+    modifies this, p;

+  {

+    x := x + 1;

+    while (p != null && p.x < 75)  // here, the decreases clause is heuristically inferred (to be the

+    {                              // same as the one in Aprime above)

+      p.x := p.x + 1;

+    }

+  }

+

   method B(p: Modifies)

     modifies this;

   {

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 39361b7b..27004653 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -5,7 +5,7 @@ class Termination {
     var i := 0;

     while (i < N)

       invariant i <= N;

-      decreases N - i;

+      // this will be heuristically inferred:  decreases N - i;

     {

       i := i + 1;

     }

@@ -95,3 +95,59 @@ datatype List<T> {
   Nil;

   Cons(T, List<T>);

 }

+

+method FailureToProveTermination0(N: int)

+{

+  var n := N;

+  while (n < 100) {  // error: may not terminate

+    n := n - 1;

+  }

+}

+

+method FailureToProveTermination1(x: int, y: int, N: int)

+{

+  var n := N;

+  while (x < y && n < 100)  // error: cannot prove termination from the heuristically chosen termination metric

+  {

+    n := n + 1;

+  }

+}

+

+method FailureToProveTermination2(x: int, y: int, N: int)

+{

+  var n := N;

+  while (x < y && n < 100)  // error: cannot prove termination from the given (bad) termination metric

+    decreases n - x;

+  {

+    n := n + 1;

+  }

+}

+

+method FailureToProveTermination3(x: int, y: int, N: int)

+{

+  var n := N;

+  while (x < y && n < 100)

+    decreases 100 - n;

+  {

+    n := n + 1;

+  }

+}

+

+method FailureToProveTermination4(x: int, y: int, N: int)

+{

+  var n := N;

+  while (n < 100 && x < y)

+    decreases 100 - n;

+  {

+    n := n + 1;

+  }

+}

+

+method FailureToProveTermination5(b: bool, N: int)

+{

+  var n := N;

+  while (b && n < 100)  // here, the heuristics are good enough to prove termination

+  {

+    n := n + 1;

+  }

+}

diff --git a/Test/dafny0/Use.dfy b/Test/dafny0/Use.dfy
index aaf41190..20928f41 100644
--- a/Test/dafny0/Use.dfy
+++ b/Test/dafny0/Use.dfy
@@ -191,7 +191,6 @@ class Recursive {
     while (k < n)

       invariant k <= n;

       invariant Gauss(k) == (k+1)*k / 2;

-      decreases n - k;

     {

       k := k + 1;

     }

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index a46e83a3..3e64a4bd 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -64,7 +64,6 @@ class Main {
         invariant (forall n :: n in S ==>

                 n.childrenVisited == old(n.childrenVisited) &&

                 n.children == old(n.children));

-        decreases |root.children| - i;

       {

         var c := root.children[i];

         if (c != null) {

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index 72415fea..9e4da459 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -96,7 +96,6 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
       while (j < N)

         invariant j <= N;

         invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);

-        decreases N - j;

       {

         call TheoremSeq(args[j], v, val);

         j := j + 1;

diff --git a/Test/vacid0/SparseArray.dfy b/Test/vacid0/SparseArray.dfy
index da1f63bb..0e6aff05 100644
--- a/Test/vacid0/SparseArray.dfy
+++ b/Test/vacid0/SparseArray.dfy
@@ -55,7 +55,6 @@ class SparseArray<T> {
       // TODO: why doesn't this work instead of the next line?  invariant (forall x :: x in s ==> x == zero);

       invariant (forall i :: 0 <= i && i < |s| ==> s[i] == zero);

       invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);

-      decreases N - k;

     {

       s := s + [zero];

       id := id + [k];

@@ -110,7 +109,6 @@ class SparseArray<T> {
     var i := 0;

     while (i < n)

       invariant i <= n && |arr| == i;

-      decreases n - i;

     {

       var g: G;

       arr := arr + [g];