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 /Test/dafny3/Dijkstra.dfy | |
| parent | 5a83f112c46196e2a48cb88796751d1a131df122 (diff) | |
added some calculational proofs from Dijkstra's writings
Diffstat (limited to 'Test/dafny3/Dijkstra.dfy')
| -rw-r--r-- | Test/dafny3/Dijkstra.dfy | 84 |
1 files changed, 84 insertions, 0 deletions
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);
+ }
+}
|