Beefed up loop invariant to prove a functional postcondition in a test case.

1 files changed, 9 insertions, 6 deletions

diff --git a/Test/dafny1/KatzManna.dfy b/Test/dafny1/KatzManna.dfy
index 38b2963e..60b70c1a 100644
--- a/Test/dafny1/KatzManna.dfy
+++ b/Test/dafny1/KatzManna.dfy
@@ -1,10 +1,13 @@
-method NinetyOne(x: int) returns (z: int)

-  requires 0 <= x;

-//  ensures z == (if x > 101 then x-10 else 91);

+method NinetyOne(x: int, ghost proveFunctionalPostcondition: bool) returns (z: int)

+  ensures proveFunctionalPostcondition ==> z == if x > 101 then x-10 else 91;

 {

   var y1 := x;

   var y2 := 1;

   while (true)

+    // the following two invariants are needed only to prove the postcondition

+    invariant proveFunctionalPostcondition ==> 100 < x ==> y1 == x;

+    invariant proveFunctionalPostcondition ==> x <= 100 < y1 && y2 == 1 ==> y1 == 101;

+    // the following two lines justify termination, as in the paper by Katz and Manna

     invariant (y1 <= 111 && y2 >= 1) || (y1 == x && y2 == 1);

     decreases -2*y1 + 21*y2 + 2*(if x < 111 then 111 else x);

   {

@@ -53,15 +56,15 @@ method Determinant(X: array2<int>, M: int) returns (z: int)
   var y := X[1-1,1-1];

   var a := 1;

   while (a != M)

-    invariant 1 <= a && a <= M;

+    invariant 1 <= a <= M;

   {

     var b := a + 1;

     while (b != M+1)

-      invariant a+1 <= b && b <= M+1;

+      invariant a+1 <= b <= M+1;

     {

       var c := M;

       while (c != a)

-        invariant a <= c && c <= M;

+        invariant a <= c <= M;

       {

         assume X[a-1,a-1] != 0;

         X[b-1, c-1] := X[b-1,c-1] - X[b-1,a-1] / X[a-1,a-1] * X[a-1,c-1];