diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-21 13:02:27 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-21 13:02:27 -0700 |
| commit | 41ad2e0dbb6283acf5edfbcbef8bdf3f2b045998 (patch) | |
| tree | 5df26689871eb8f8bec62514fa73afe11d3c8041 | |
| parent | 5a83f112c46196e2a48cb88796751d1a131df122 (diff) | |
added some calculational proofs from Dijkstra's writings
| -rw-r--r-- | Test/dafny3/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny3/Dijkstra.dfy | 84 | ||||
| -rw-r--r-- | Test/dafny3/runtest.bat | 2 |
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
|