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

4 files changed, 60 insertions, 68 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);