From 0c77817fae2b4743820c47634dfbe8fd9036a533 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 22 Mar 2013 10:30:27 -0700
Subject: Updated two test files.

---
 Test/dafny3/Answer       |  2 +-
 Test/dafny3/Dijkstra.dfy | 79 ++++++++++++++++++++++++++++--------------------
 2 files changed, 47 insertions(+), 34 deletions(-)

(limited to 'Test/dafny3')

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