summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-10-21 13:02:27 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2012-10-21 13:02:27 -0700
commit41ad2e0dbb6283acf5edfbcbef8bdf3f2b045998 (patch)
tree5df26689871eb8f8bec62514fa73afe11d3c8041
parent5a83f112c46196e2a48cb88796751d1a131df122 (diff)
added some calculational proofs from Dijkstra's writings
-rw-r--r--Test/dafny3/Answer4
-rw-r--r--Test/dafny3/Dijkstra.dfy84
-rw-r--r--Test/dafny3/runtest.bat2
3 files changed, 89 insertions, 1 deletions
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