Dafny:

* For every loop decreases clause N, generate a free loop invariant N <= N0, where N0 is the value of N just before the loop.
* Added Test/dafny1/KatzManna.dfy, which contains the 3 programs (and their termination annotations) from the Katz and Manna 1975 paper "A closer look at termination" (which benefits from the feature above).

1 files changed, 22 insertions, 0 deletions

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index 974dadab..35ff53b0 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -170,3 +170,25 @@ class Node {
                         next.Valid())

   }

 }

+

+method DecreasesYieldsAnInvariant(z: int) {

+  var x := 100;

+  var y := 1;

+  var z := z;  // make parameter into a local variable

+  while (x != y)

+    // inferred: decreases |x - y|;

+    invariant  (0 < x && 0 < y) || (x < 0 && y < 0);

+  {

+    if (z == 52) {

+      break;

+    } else if (x < y) {

+      y := y - 1;

+    } else {

+      x := x - 1;

+    }

+    x := -x;

+    y := -y;

+    z := z + 1;

+  }

+  assert x - y < 100;  // follows from the fact that no loop iteration increases what's in the 'decreases' clause

+}