Updated two test files.

2 files changed, 47 insertions, 34 deletions

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index b258fe3d..9c6a2598 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -9,7 +9,7 @@ Dafny program verifier finished with 50 verified, 0 errors
 

 -------------------- Dijkstra.dfy --------------------

 

-Dafny program verifier finished with 11 verified, 0 errors

+Dafny program verifier finished with 12 verified, 0 errors

 

 -------------------- CachedContainer.dfy --------------------

 

diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy
index 7497618c..ef94f291 100644
--- a/Test/dafny3/Dijkstra.dfy
+++ b/Test/dafny3/Dijkstra.dfy
@@ -2,83 +2,96 @@
 // Edsger W. Dijkstra: Heuristics for a Calculational Proof. Inf. Process. Lett. (IPL) 53(3):141-143 (1995)

 // Transcribed into Dafny by Valentin Wüstholz and Nadia Polikarpova.

 

-

+// f is an arbitrary function on the natural numbers

 function f(n: nat) : nat

 

-ghost method theorem(n: nat)

-  requires forall m: nat :: f(f(m)) < f(m + 1);

-  ensures f(n) == n;

+// Predicate P() says that f satisfies a peculiar property

+predicate P()

 {

-  calc

-  {

-    f(n);

-    { lemma_ping(n, n); lemma_pong(n); }

-    n;

+  forall m: nat :: f(f(m)) < f(m + 1)

+}

+

+// The following theorem says that if f satisfies the peculiar property,

+// then f is the identity function.  The body of the method, and the methods

+// that follow, give the proof.

+ghost method theorem()

+  requires P();

+  ensures forall n: nat :: f(n) == n;

+{

+  forall (n: nat) {

+    calc {

+      f(n);

+    ==  { lemma_ping(n, n); lemma_pong(n); }

+      n;

+    }

   }

 }

 

 // Aiming at n <= f(n), but strengthening it for induction

 ghost method lemma_ping(j: nat, n: nat)

-  requires forall m: nat :: f(f(m)) < f(m + 1); // (0)

+  requires P();

   ensures j <= n ==> j <= f(n);

 {

   // The case for j == 0 is trivial

-  if (0 < j <= n) {

+  if 0 < j {

     calc {

-      j <= n;

-      { lemma_ping(j - 1, n - 1); }

-      j - 1 <= f(n - 1);

-      ==> { lemma_ping(j - 1, f(n - 1)); }

-      j - 1 <= f(f(n - 1));

-      // (0)

-      j - 1 <= f(f(n - 1)) && f(f(n - 1)) < f(n);

-      ==> j - 1 < f(n);

       j <= f(n);

+    ==

+      j - 1 < f(n);

+    <== // P with m := n - 1

+      j - 1 <= f(f(n - 1)) && 1 <= n;

+    <== { lemma_ping(j - 1, f(n - 1)); }

+      j - 1 <= f(n - 1) && 1 <= n;

+    <== { lemma_ping(j - 1, n - 1); }

+      j - 1 <= n - 1 && 1 <= n;

+    == // 0 < j

+      j <= n;

     }

   }

 }

 

 // The other directorion: f(n) <= n

 ghost method lemma_pong(n: nat)

-  requires forall m: nat :: f(f(m)) < f(m + 1);  // (0)

+  requires P();

   ensures f(n) <= n;

 {

   calc {

-    true;

-    // (0) with m := n

-    f(f(n)) < f(n + 1);

-    { lemma_monotonicity_0(n + 1, f(n)); }

-    f(n) < n + 1;

     f(n) <= n;

+  ==

+    f(n) < n + 1;

+  <==  { lemma_monotonicity_0(n + 1, f(n)); }

+    f(f(n)) < f(n + 1);

+  ==  // P with m := n

+    true;        

   }

 }

 

 ghost method lemma_monotonicity_0(a: nat, b: nat)

-  requires forall m: nat :: f(f(m)) < f(m + 1);

+  requires P();

   ensures a <= b ==> f(a) <= f(b);  // or, equivalently:  f(b) < f(a) ==> b < a

   decreases b - a;

 {

   // The case for a == b is trivial

   if (a < b) {

-    calc <= {

+    calc {

       f(a);

-      { lemma_monotonicity_1(a); }

+    <=  { lemma_monotonicity_1(a); }

       f(a + 1);

-      { lemma_monotonicity_0(a + 1, b); }

+    <=  { lemma_monotonicity_0(a + 1, b); }

       f(b);

     }

   }

 }

 

 ghost method lemma_monotonicity_1(n: nat)

-  requires forall m: nat :: f(f(m)) < f(m + 1);  // (0)

+  requires P();

   ensures f(n) <= f(n + 1);

 {

-  calc <= {

+  calc {

     f(n);

-    { lemma_ping(f(n), f(n)); }

+  <=  { lemma_ping(f(n), f(n)); }

     f(f(n));

-    // (0)

+  <=  // (0)

     f(n + 1);

   }

 }