From 41ad2e0dbb6283acf5edfbcbef8bdf3f2b045998 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Sun, 21 Oct 2012 13:02:27 -0700
Subject: added some calculational proofs from Dijkstra's writings

---
 Test/dafny3/Answer       |  4 +++
 Test/dafny3/Dijkstra.dfy | 84 ++++++++++++++++++++++++++++++++++++++++++++++++
 Test/dafny3/runtest.bat  |  2 +-
 3 files changed, 89 insertions(+), 1 deletion(-)
 create mode 100644 Test/dafny3/Dijkstra.dfy

(limited to 'Test/dafny3')

diff --git a/Test/dafny3/Answer b/Test/dafny3/Answer
index ae65e2d9..240883dd 100644
--- a/Test/dafny3/Answer
+++ b/Test/dafny3/Answer
@@ -6,3 +6,7 @@ Dafny program verifier finished with 15 verified, 0 errors
 -------------------- Streams.dfy --------------------
 
 Dafny program verifier finished with 38 verified, 0 errors
+
+-------------------- Dijkstra.dfy --------------------
+
+Dafny program verifier finished with 11 verified, 0 errors
diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy
new file mode 100644
index 00000000..d3ff244a
--- /dev/null
+++ b/Test/dafny3/Dijkstra.dfy
@@ -0,0 +1,84 @@
+// Example taken from:
+// 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.
+
+
+function f(n: nat) : nat
+
+ghost method theorem(n: nat)
+  requires forall m: nat :: f(f(m)) < f(m + 1);
+  ensures f(n) == n;
+{
+  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)
+  ensures j <= n ==> j <= f(n);
+{
+  // The case for j == 0 is trivial
+  if (0 < j <= n) {
+    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);
+    }
+  }
+}
+
+// The other directorion: f(n) <= n
+ghost method lemma_pong(n: nat)
+  requires forall m: nat :: f(f(m)) < f(m + 1);  // (0)
+  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;
+  }
+}
+
+ghost method lemma_monotonicity_0(a: nat, b: nat)
+  requires forall m: nat :: f(f(m)) < f(m + 1);
+  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 <= {
+      f(a);
+      { lemma_monotonicity_1(a); }
+      f(a + 1);
+      { 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)
+  ensures f(n) <= f(n + 1);
+{
+  calc <= {
+    f(n);
+    { lemma_ping(f(n), f(n)); }
+    f(f(n));
+    // (0)
+    f(n + 1);
+  }
+}
diff --git a/Test/dafny3/runtest.bat b/Test/dafny3/runtest.bat
index 9265dcd0..f995daff 100644
--- a/Test/dafny3/runtest.bat
+++ b/Test/dafny3/runtest.bat
@@ -4,7 +4,7 @@ setlocal
 set BINARIES=..\..\Binaries
 set DAFNY_EXE=%BINARIES%\Dafny.exe
 
-for %%f in (Iter.dfy Streams.dfy) do (
+for %%f in (Iter.dfy Streams.dfy Dijkstra.dfy) do (
   echo.
   echo -------------------- %%f --------------------
   %DAFNY_EXE% /compile:0 /dprint:out.dfy.tmp %* %%f
-- 
cgit v1.2.3