From fadc6a922eb99b83b898b55286e48f63ed0df751 Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Fri, 11 Jun 2010 02:02:36 +0000
Subject: Dafny:  Added two additional heuristics for guessing missing loop
 decreases clauses (for loop guard A!=B and for loop guards with multiple
 conjuncts)

---
 Test/VSI-Benchmarks/b1.dfy | 122 ++++++++++++++++++++++-----------------------
 Test/VSI-Benchmarks/b2.dfy |   1 -
 Test/VSI-Benchmarks/b3.dfy |   2 -
 Test/VSI-Benchmarks/b8.dfy |   3 +-
 4 files changed, 60 insertions(+), 68 deletions(-)

(limited to 'Test/VSI-Benchmarks')

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);
-- 
cgit v1.2.3