From 6eec3f506008f7522f9dadbc06a4e871a5faa1ae Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 9 Jul 2014 17:28:55 -0700 Subject: Improved AnalyzeList encoding in a way that performs way better. Cleaned up file to use some improved Dafny constructs. --- .../COST-verif-comp-2011-4-FloydCycleDetect.dfy | 106 ++++++++------------- ...T-verif-comp-2011-4-FloydCycleDetect.dfy.expect | 2 +- 2 files changed, 42 insertions(+), 66 deletions(-) (limited to 'Test/dafny2') diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy index ee56e14a..2aa14db7 100644 --- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy +++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy @@ -66,13 +66,13 @@ links) and false when it is not. // The proof is long. One interesting aspect of it is that it is all constructed // as a program fed to a program verifier. Since the additional properties -// are specified using ghost variables, ghost methods, and other ghost constructs, +// are specified using ghost variables, lemmas, and other ghost constructs, // the run-time execution of the program is not affected by including the // proof as part of the program, because the Dafny compiler ignores all ghost // constructs. // The proof (and in particular the proof of termination), makes use of two -// numbers, called 'A' and 'B' and computed by the call to the ghost method +// numbers, called 'A' and 'B' and computed by the call to the lemma // 'AnalyzeList'. 'A' is the number of steps from 'this' before a cycle is // reached. If there is no cycle, 'A' is the length of the list. 'B' is the // length of the cycle, if any. But, you ask, how are 'A' and 'B' obtained? @@ -81,15 +81,15 @@ links) and false when it is not. // that 'AnalyzeList' uses a simpler algorithm, namely a depth-first traversal // from 'this' that uses a set to keep track of which nodes have been visited. // This set would not be nice to have to represent at run time, but since -// 'AnalyzeList' is a ghost method, the variable holding the set does not survive -// compilation. So, 'Cyclic' first calls ghost method 'Analyze' to traverse +// 'AnalyzeList' is a lemma, the variable holding the set does not survive +// compilation. So, 'Cyclic' first calls lemma 'Analyze' to traverse // the list and then, equipped with 'A' and 'B' to carry out the proof of Floyd's // algorithm, proceeds with Floyd's algorithm. // The ghost constructs in 'Cyclic' add some clutter to the program text. To // alleviate matter a little, I have include the word "Lemma" in the names of -// all ghost methods (except ghost method 'AnalyzeList', which I guess didn't -// feel to me like a "lemma" per se). +// all lemmas (except lemma 'AnalyzeList', which I guess didn't feel to me like +// a "lemma" per se). // The Dafny verifier, which builds on verification engine Boogie, which in turn // builds on the SMT solver Z3, needs help throughout this proof. To give it @@ -120,7 +120,7 @@ links) and false when it is not. // the program matches your execution environment. The only input fed to // the Dafny verifier/compiler is the program text below; Dafny then automatically // verifies and compiles the program (for this program in less than 30 seconds, -// 25 seconds of which is spent verifying the ghost method AnalyzeList) +// 25 seconds of which is spent verifying the lemma AnalyzeList) // without further human intervention. class Node { @@ -159,7 +159,7 @@ class Node { ghost var A, B := AnalyzeList(S); var tortoise, hare:= this, next; ghost var t, h := 0, 1; - while (hare != tortoise) + while hare != tortoise invariant tortoise != null && tortoise in S && hare in S; invariant 0 <= t < h && Nexxxt(t, S) == tortoise && Nexxxt(h, S) == hare; // What follows of the invariant is for proving termination: @@ -167,7 +167,7 @@ class Node { invariant forall k :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S); decreases A + B - t; { - if (hare == null || hare.next == null) { + if hare == null || hare.next == null { ghost var distanceToNull := if hare == null then h else h+1; Lemma_NullImpliesNoCycles(distanceToNull, S); assert !exists k,l :: 0 <= k && 0 <= l && Nexxxt(k, S) != null && Nexxxt(k, S).next != null && Nexxxt(k, S).next.Nexxxt(l, S) == Nexxxt(k, S); // this is a copy of the postcondition of lemma NullImpliesNoCycles @@ -189,7 +189,7 @@ class Node { // details below--the specification of 'Cyclic' above and the fact that Dafny verifies // the program suffice. (Of course, one also needs to trust the verifier.) - ghost method AnalyzeList(S: set) returns (A: int, B: int) + lemma AnalyzeList(S: set) returns (A: int, B: int) requires IsClosed(S); // find an A and B (0 <= A && 1 <= B) such that: // the first A steps are no on a cycle, and @@ -199,59 +199,35 @@ class Node { ensures forall k,l :: 0 <= k < l < A ==> Nexxxt(k, S) != Nexxxt(l, S); { // since S is finite, we can just go ahead and compute the transitive closure of "next" from "this" - var p, steps, Visited := this, 0, {null}; - while (p !in Visited) + var p, steps, Visited, NexxxtInverse: map := this, 0, {null}, map[]; + while p !in Visited invariant 0 <= steps && p == Nexxxt(steps, S) && p in S && null in Visited && Visited <= S; - invariant forall t :: 0 <= t < steps ==> Nexxxt(t, S) in Visited; - invariant forall q :: q in (Visited - {null}) ==> exists t :: 0 <= t < steps && Nexxxt(t, S) == q; - invariant forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S); + invariant forall t :: 0 <= t < steps ==> + Nexxxt(t, S) in Visited && + Nexxxt(t, S) in NexxxtInverse && NexxxtInverse[Nexxxt(t, S)] == t; + invariant forall q :: q in Visited && q != null ==> + q in NexxxtInverse && 0 <= NexxxtInverse[q] < steps && Nexxxt(NexxxtInverse[q], S) == q; decreases S - Visited; { - p, steps, Visited := p.next, steps + 1, Visited + {p}; - - // with all: 3s - // without this: 20s - assert forall t :: 0 <= t < steps ==> Nexxxt(t, S) in Visited; - // without this: 5s - assert forall q :: q in (Visited - {null}) ==> exists t :: 0 <= t < steps && Nexxxt(t, S) == q; - // without this: >60s - assert forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S); + p, steps, Visited, NexxxtInverse := p.next, steps + 1, Visited + {p}, NexxxtInverse[p := steps]; } - if (p == null) { + if p == null { A, B := steps, 1; } else { - A := FindA(S, steps, p); + A := NexxxtInverse[p]; B := steps - A; Lemma_NexxxtIsTransitive(A, B, S); } } - ghost method FindA(S: set, steps: int, p: Node) returns (A: int) - requires IsClosed(S); - requires 0 <= steps && p == Nexxxt(steps, S) && p in S && p != null; - requires exists k :: 0 <= k < steps && Nexxxt(k, S) == p; - ensures 0 <= A < steps; - ensures Nexxxt(A, S) == p; - ensures forall k :: 0 <= k < A ==> Nexxxt(k, S) != p; - { - A := 0; - while (Nexxxt(A, S) != p) - invariant 0 <= A < steps; - invariant forall k :: 0 <= k < A ==> Nexxxt(k, S) != p; - decreases steps - A; - { - A := A + 1; - } - } - - ghost method CrucialLemma(a: int, b: int, S: set) + lemma CrucialLemma(a: int, b: int, S: set) requires IsClosed(S); requires 0 <= a && 1 <= b; requires forall k,l :: 0 <= k < l < a ==> Nexxxt(k, S) != Nexxxt(l, S); requires Nexxxt(a, S) == null || Nexxxt(a, S).Nexxxt(b, S) == Nexxxt(a, S); ensures exists T :: 0 <= T < a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S); { - if (Nexxxt(a, S) == null) { + if Nexxxt(a, S) == null { Lemma_NullIsTerminal(1+2*a, S); assert Nexxxt(a, S) == null ==> Nexxxt(1+2*a, S) == null; } else { @@ -266,7 +242,7 @@ class Node { // as many steps as the hare (but fewer than "b" steps more than the hare). var t, h := a, 1+2*a; // steps traveled by the tortoise and the hare, respectively var vt := a; // steps traveled by the virtual tortoise - while (vt < h) + while vt < h invariant t <= vt < h+b; invariant Nexxxt(t, S) == Nexxxt(vt, S); { @@ -281,7 +257,7 @@ class Node { // Now, let the hare catch up with the virtual tortoise by simulating "catchup" steps // of the algorithm. var i := 0; - while (i < catchup) + while i < catchup invariant 0 <= i <= catchup; invariant t == a + i && h == 1 + 2*t && t <= vt; invariant Nexxxt(t, S) == Nexxxt(vt, S) == Nexxxt(h + catchup - i, S); @@ -292,14 +268,14 @@ class Node { } } - ghost method Lemma_AboutCycles(a: int, b: int, k: int, S: set) + lemma Lemma_AboutCycles(a: int, b: int, k: int, S: set) requires IsClosed(S); requires 0 <= a <= k && 1 <= b && Nexxxt(a, S) != null && Nexxxt(a, S).Nexxxt(b, S) == Nexxxt(a, S); ensures Nexxxt(k + b, S) == Nexxxt(k, S); { Lemma_NexxxtIsTransitive(a, b, S); var n := a; - while (n < k) + while n < k invariant a <= n <= k; invariant Nexxxt(n + b, S) == Nexxxt(n, S); { @@ -307,16 +283,16 @@ class Node { } } - ghost method Lemma_NexxxtIsTransitive(x: int, y: int, S: set) + lemma Lemma_NexxxtIsTransitive(x: int, y: int, S: set) requires IsClosed(S) && 0 <= x && 0 <= y; ensures Nexxxt(x, S) != null ==> Nexxxt(x, S).Nexxxt(y, S) == Nexxxt(x + y, S); { - if (Nexxxt(x, S) != null) + if Nexxxt(x, S) != null { assert forall j :: 0 <= j ==> Nexxxt(x, S).Nexxxt(j, S) == Nexxxt(x + j, S); // Dafny's induction tactic kicks in /* Alternatively, here's a manual proof by induction (but only up to the needed y): var j := 0; - while (j < y) + while j < y invariant 0 <= j <= y; invariant Nexxxt(x, S).Nexxxt(j, S) == Nexxxt(x + j, S); { @@ -326,23 +302,23 @@ class Node { } } - ghost method Lemma_NullIsTerminal(d: int, S: set) + lemma Lemma_NullIsTerminal(d: int, S: set) requires IsClosed(S) && 0 <= d; ensures forall k :: 0 <= k < d && Nexxxt(d, S) != null ==> Nexxxt(k, S) != null; { var j := d; - while (0 < j) + while 0 < j invariant 0 <= j <= d; invariant forall k :: j <= k < d && Nexxxt(k, S) == null ==> Nexxxt(d, S) == null; { j := j - 1; - if (Nexxxt(j, S) == null) { + if Nexxxt(j, S) == null { assert Nexxxt(j+1, S) == null; } } } - ghost method Lemma_NullImpliesNoCycles(n: int, S: set) + lemma Lemma_NullImpliesNoCycles(n: int, S: set) requires IsClosed(S) && 0 <= n && Nexxxt(n, S) == null; ensures !exists k,l :: 0 <= k && 0 <= l && Nexxxt(k, S) != null && Nexxxt(k, S).next != null && Nexxxt(k, S).next.Nexxxt(l, S) == Nexxxt(k, S); { @@ -353,14 +329,14 @@ class Node { Lemma_NullImpliesNoCycles_part2(n, S); } - ghost method Lemma_NullImpliesNoCycles_part0(n: int, S: set) + lemma Lemma_NullImpliesNoCycles_part0(n: int, S: set) requires IsClosed(S) && 0 <= n && Nexxxt(n, S) == null; ensures forall k,l :: n <= k && 0 <= l && Nexxxt(k, S) != null && Nexxxt(k, S).next != null ==> Nexxxt(k, S).next.Nexxxt(l, S) != Nexxxt(k, S); { assert forall k :: n <= k ==> Nexxxt(k, S) == null; // Dafny proves this thanks to its induction tactic } - ghost method Lemma_NullImpliesNoCycles_part1(n: int, S: set) + lemma Lemma_NullImpliesNoCycles_part1(n: int, S: set) requires IsClosed(S) && 0 <= n && Nexxxt(n, S) == null; ensures forall k,l :: 0 <= k && n <= l && Nexxxt(k, S) != null && Nexxxt(k, S).next != null ==> Nexxxt(k, S).next.Nexxxt(l, S) != Nexxxt(k, S); { @@ -369,22 +345,22 @@ class Node { assert forall kl :: n <= kl ==> Nexxxt(kl, S) == null; } - ghost method Lemma_NullImpliesNoCycles_part2(n: int, S: set) + lemma Lemma_NullImpliesNoCycles_part2(n: int, S: set) requires IsClosed(S) && 0 <= n && Nexxxt(n, S) == null; ensures forall k,l :: 0 <= k < n && 0 <= l < n && Nexxxt(k, S) != null && Nexxxt(k, S).next != null ==> Nexxxt(k, S).next.Nexxxt(l, S) != Nexxxt(k, S); { var kn := 0; - while (kn < n) + while kn < n invariant 0 <= kn <= n; invariant forall k,l :: 0 <= k < kn && 0 <= l < n && Nexxxt(k, S) != null && Nexxxt(k, S).next != null ==> Nexxxt(k, S).next.Nexxxt(l, S) != Nexxxt(k, S); { var ln := 0; - while (ln < n) + while ln < n invariant 0 <= ln <= n; invariant forall k,l :: 0 <= k < kn && 0 <= l < n && Nexxxt(k, S) != null && Nexxxt(k, S).next != null ==> Nexxxt(k, S).next.Nexxxt(l, S) != Nexxxt(k, S); invariant forall l :: 0 <= l < ln && Nexxxt(kn, S) != null && Nexxxt(kn, S).next != null ==> Nexxxt(kn, S).next.Nexxxt(l, S) != Nexxxt(kn, S); { - if (Nexxxt(kn, S) != null && Nexxxt(kn, S).next != null) { + if Nexxxt(kn, S) != null && Nexxxt(kn, S).next != null { assert Nexxxt(kn+1, S) != null; Lemma_NexxxtIsTransitive(kn+1, ln, S); assert Nexxxt(kn, S).next.Nexxxt(ln, S) == Nexxxt(kn+1+ln, S); // follows from the transitivity lemma on the previous line @@ -393,9 +369,9 @@ class Node { // finally, here comes the central part of the argument, namely: // if Nexxxt(kn, S).Nexxxt(1+ln, S) == Nexxxt(kn, S), then for any h (0 <= h), Nexxxt(kn, S).Nexxxt(h*(1+ln), S) == Nexxxt(kn, S), but // that can't be for n <= h*(1+ln), since Nexxxt(kn, S) != null and Nexxxt(n.., S) == null. - if (Nexxxt(kn, S).Nexxxt(1+ln, S) == Nexxxt(kn, S)) { + if Nexxxt(kn, S).Nexxxt(1+ln, S) == Nexxxt(kn, S) { var nn := 1+ln; - while (nn < n) + while nn < n invariant 0 <= nn; invariant Nexxxt(kn, S).Nexxxt(nn, S) == Nexxxt(kn, S); { diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy.expect b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy.expect index 9d7e625f..5add7af7 100644 --- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy.expect +++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 25 verified, 0 errors +Dafny program verifier finished with 23 verified, 0 errors -- cgit v1.2.3