diff options
Diffstat (limited to 'Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy')
| -rw-r--r-- | Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy | 404 |
1 files changed, 0 insertions, 404 deletions
diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy deleted file mode 100644 index 774008b8..00000000 --- a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy +++ /dev/null @@ -1,404 +0,0 @@ -/*
-Rustan Leino, 6 Oct 2011
-
-COST Verification Competition, Challenge 4: Cyclic list
-http://foveoos2011.cost-ic0701.org/verification-competition
-
-Given: A Java linked data structure with the signature:
-
-public class Node {
- Node next;
-
- public boolean cyclic() {
- //...
- }
-}
-
-Implement and verify the method cyclic() to return true when the data
-structure is cyclic (i.e., this Node can be reached by following next
-links) and false when it is not.
-*/
-
-// Remarks:
-
-// I found the problem statement slightly ambiguous. What I implemented was a
-// method 'Cyclic' that returns true when 'this' can reach a cycle. That is,
-// 'this' does not itself have to be on the cycle in order for the method to
-// return true.
-
-// I wanted to assume as little as possible about the state of the data structure
-// when 'Cyclic' is called. The proof of the algorithm (indeed, the correctness
-// of the algorithm) requires the number of nodes to be finite. To specify
-// this, I included to 'Cyclic' a parameter 'S' that contains all nodes that
-// are reachable from 'this'. The specification says that 'S' contains 'this'
-// and 'null', and that is closed under the 'next' field. This parameter and
-// its associated 'IsClosed' condition are threaded through all functions and
-// methods in the program. The set 'S' is used only for specification purposes,
-// so I declared it to be a ghost parameter of 'Cyclic'. Other than including
-// 'S' and 'IsClosed(S)' in the specification, the program does not assume anything
-// about the state of 'this' and the other objects in 'S'.
-
-// The algorithm I implement and verify is due to Bob Floyd and is sometimes
-// known as the "tortoise and hare" algorithm. The idea is simple: Use 2 pointers,
-// called 'tortoise' and 'hare', and advance 'hare' twice as quickly as 'tortoise'.
-// Eventually, 'hare' will reach 'null' (in which case 'this' does not reach a
-// cycle) or 'hare' will become equal to 'tortoise' (in which 'this' does reach a
-// cycle). Formally and mechanically proving the correctness of the algorithm
-// is much harder, I found.
-
-// Because this file is long, it is especially important to know what a human needs
-// to trust in order to believe that the program is correct. The main thing
-// is the specification of 'Cyclic', and in particular its postcondition, which
-// expresses what it means for 'this' to be able to reach a cycle. Since this
-// postcondition mentions the function 'Reaches', it is also necessary to trust
-// the definition of 'Reaches' (but it is not necessary to trust the 'ensures'
-// clause of the function). Function 'Reaches' is in turn defined in terms
-// of 'Nexxxt(k,...)' which stands for 'k' applications of the field 'next'
-// (and returns 'null' if 'null' is ever reached along the way). Other than
-// these things, the rest of the program is implementation details and proof
-// details. Well, one may want to inspect the body of 'Cyclic' to see that it
-// does indeed implement Floyd's algorithm--for this inspection, ignore all
-// ghost things, like ghost variables, updates to ghost variables, assert
-// statements, and calls to lemmas.
-
-// 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,
-// 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
-// '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?
-// If these are used to prove the termination of 'Cyclic', then how does one
-// prove the termination of the computation of 'A' and 'B'? The answer is
-// 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
-// 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).
-
-// 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
-// hints about which properties to prove, the program uses assert statements and
-// calls to lemmas. These do not provide the verifier with new facts or
-// assumptions--they only instruct the verifier to verify something, after which
-// the verifier can make use of what it just verified. In a number of places,
-// the assert statements mention universally quantified properties whose proof
-// require induction; Dafny heuristically detects these and applies its induction
-// tactic (in the absence of that induction tactic, more handholding would be
-// required in the program text to guide the verifier through the proof, see
-// 'Lemma_NexxxtIsTransitive', for example).
-
-// About Dafny:
-// As always (when it is successful), Dafny verifies that the program does not
-// cause any run-time errors (like array index bounds errors), that the program
-// terminates, that expressions and functions are well defined, and that all
-// specifications are satisfied. The language prevents type errors by being type
-// safe, prevents dangling pointers by not having an "address-of" or "deallocate"
-// operation (which is accommodated at run time by a garbage collector), and
-// prevents arithmetic overflow errors by using mathematical integers (which
-// is accommodated at run time by using BigNum's). By proving that programs
-// terminate, Dafny proves that a program's time usage is finite, which implies
-// that the program's space usage is finite too. However, executing the
-// program may fall short of your hopes if you don't have enough time or
-// space; that is, the program may run out of space or may fail to terminate in
-// your lifetime, because Dafny does not prove that the time or space needed by
-// 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)
-// without further human intervention.
-
-class Node {
- var next: Node;
-
- function IsClosed(S: set<Node>): bool
- reads S;
- {
- this in S && null in S &&
- forall n :: n in S && n != null && n.next != null ==> n.next in S
- }
-
- function Nexxxt(k: int, S: set<Node>): Node
- requires IsClosed(S) && 0 <= k;
- ensures Nexxxt(k, S) in S; // a consequence of the definition
- reads S;
- decreases k;
- {
- if k == 0 then this
- else if Nexxxt(k-1, S) == null then null
- else Nexxxt(k-1, S).next
- }
-
- function Reaches(sink: Node, S: set<Node>): bool
- requires IsClosed(S);
- ensures Reaches(sink, S) ==> sink in S; // a consequence of the definition
- reads S;
- {
- exists k :: 0 <= k && Nexxxt(k, S) == sink
- }
-
- method Cyclic(ghost S: set<Node>) returns (reachesCycle: bool)
- requires IsClosed(S);
- ensures reachesCycle <==> exists n :: n != null && Reaches(n, S) && n.next != null && n.next.Reaches(n, S);
- {
- ghost var A, B := AnalyzeList(S);
- var tortoise, hare:= this, next;
- ghost var t, h := 0, 1;
- 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:
- invariant h == 1 + 2*t && t <= A + B;
- invariant forall k :: 0 <= k < t ==> Nexxxt(k, S) != Nexxxt(1+2*k, S);
- decreases A + B - t;
- {
- 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
- return false;
- }
- Lemma_NullIsTerminal(h+1, S);
- assert Nexxxt(t+1, S) != null;
- tortoise, t, hare, h := tortoise.next, t+1, hare.next.next, h+2;
- CrucialLemma(A, B, S);
- }
- Lemma_NullIsTerminal(h, S);
- Lemma_NexxxtIsTransitive(t+1, h - (t+1), S);
- assert tortoise.next.Reaches(tortoise, S);
- return true;
- }
-
- // What follows in this file are details that are relevant only to the proof. That is,
- // to trust that the algorithm is correct, it is not necessary to go through the
- // 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<Node>) 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
- // either next^A == null or next^A == next^(A+B).
- ensures 0 <= A && 1 <= B;
- ensures forall k,l :: 0 <= k < l < A ==> Nexxxt(k, S) != Nexxxt(l, S);
- ensures Nexxxt(A, S) == null || Nexxxt(A, S).Nexxxt(B, S) == Nexxxt(A, 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)
- invariant 0 <= steps && p == Nexxxt(steps, S) && p in S && null in Visited;
- invariant Visited <= S;
- invariant forall t :: 0 <= t < steps ==> Nexxxt(t, S) in Visited;
- invariant forall q :: q in Visited ==> q == null || exists t :: 0 <= t < steps && Nexxxt(t, S) == q;
- invariant forall k,l :: 0 <= k < l < steps ==> Nexxxt(k, S) != Nexxxt(l, S);
- decreases S - Visited;
- {
- p, steps, Visited := p.next, steps + 1, Visited + {p};
- }
- if (p == null) {
- A, B := steps, 1;
- } else {
- assert exists k :: 0 <= k < steps && Nexxxt(k, S) == p;
- // find this k
- 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;
- }
- B := steps - A;
- assert Nexxxt(A, S) != null;
- Lemma_NexxxtIsTransitive(A, B, S);
- }
- }
-
- ghost method CrucialLemma(a: int, b: int, S: set<Node>)
- 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) {
- Lemma_NullIsTerminal(1+2*a, S);
- assert Nexxxt(a, S) == null ==> Nexxxt(1+2*a, S) == null;
- } else {
- assert Nexxxt(a, S) != null && Nexxxt(a, S).Nexxxt(b, S) == Nexxxt(a, S);
- Lemma_NexxxtIsTransitive(a, b, S);
- assert Nexxxt(a + b, S) == Nexxxt(a, S);
- // When the tortoise has done "a" steps, both it and the hare have reached the cycle.
- // Since the cycle has length "b", the hare has at most "b" steps to catch up with the
- // tortoise. Well, you may think of the tortoise as being the one that has to catch up,
- // since the tortoise has not traveled as far. So, let's imagine a virtual tortoise
- // that is in the same position as the tortoise, but who got there by taking at least
- // 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)
- invariant t <= vt < h+b;
- invariant Nexxxt(t, S) == Nexxxt(vt, S);
- {
- Lemma_AboutCycles(a, b, vt, S);
- vt := vt + b; // let the virtual tortoise take another lap
- }
- // Good. Since the virtual tortoise has now taken at least as many steps as the hare,
- // we can compute (as a non-negative number) the steps that hare is trailing behind the
- // virtual tortoise.
- var catchup := vt - h;
- assert 0 <= catchup < b;
- // Now, let the hare catch up with the virtual tortoise by simulating "catchup" steps
- // of the algorithm.
- var i := 0;
- 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);
- {
- i, t, vt, h := i+1, t+1, vt+1, h+2;
- }
- assert a <= t < a + b && Nexxxt(t, S) == Nexxxt(1 + 2*t, S);
- }
- }
-
- ghost method Lemma_AboutCycles(a: int, b: int, k: int, S: set<Node>)
- 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)
- invariant a <= n <= k;
- invariant Nexxxt(n + b, S) == Nexxxt(n, S);
- {
- n := n + 1;
- }
- }
-
- ghost method Lemma_NexxxtIsTransitive(x: int, y: int, S: set<Node>)
- 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)
- {
- 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)
- invariant 0 <= j <= y;
- invariant Nexxxt(x, S).Nexxxt(j, S) == Nexxxt(x + j, S);
- {
- j := j + 1;
- }
- */
- }
- }
-
- ghost method Lemma_NullIsTerminal(d: int, S: set<Node>)
- 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)
- 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) {
- assert Nexxxt(j+1, S) == null;
- }
- }
- }
-
- ghost method Lemma_NullImpliesNoCycles(n: int, S: set<Node>)
- 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);
- {
- // The proof of this lemma is more complicated than necessary, because Dafny does not know that
- // "if P(k,l) holds for one arbitrary (k,l), then it holds for all (k,l)".
- Lemma_NullImpliesNoCycles_part0(n, S);
- Lemma_NullImpliesNoCycles_part1(n, S);
- Lemma_NullImpliesNoCycles_part2(n, S);
- }
-
- ghost method Lemma_NullImpliesNoCycles_part0(n: int, S: set<Node>)
- 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<Node>)
- 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);
- {
- // Each of the following assertions makes use of Dafny's induction tactic
- assert forall k,l :: 0 <= k && 0 <= l && Nexxxt(k, S) != null && Nexxxt(k, S).next != null ==> Nexxxt(k, S).next.Nexxxt(l, S) == Nexxxt(k+1+l, S);
- assert forall kl :: n <= kl ==> Nexxxt(kl, S) == null;
- }
-
- ghost method Lemma_NullImpliesNoCycles_part2(n: int, S: set<Node>)
- 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)
- 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)
- 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) {
- 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
- Lemma_NexxxtIsTransitive(kn, 1+ln, S);
- assert Nexxxt(kn+1+ln, S) == Nexxxt(kn, S).Nexxxt(1+ln, S); // follows from the transitivity lemma on the previous line
- // 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)) {
- var nn := 1+ln;
- while (nn < n)
- invariant 0 <= nn;
- invariant Nexxxt(kn, S).Nexxxt(nn, S) == Nexxxt(kn, S);
- {
- assert Nexxxt(kn, S) ==
- Nexxxt(kn, S).Nexxxt(nn, S) ==
- Nexxxt(kn, S).Nexxxt(1+ln, S) ==
- Nexxxt(kn, S).Nexxxt(nn, S).Nexxxt(1+ln, S);
- Nexxxt(kn, S).Lemma_NexxxtIsTransitive(1+ln, nn, S);
- assert Nexxxt(kn, S).Nexxxt(nn+1+ln, S) == Nexxxt(kn, S);
- nn := nn + 1+ln;
- }
- Lemma_NexxxtIsTransitive(kn, nn, S);
- assert Nexxxt(kn, S).Nexxxt(nn, S) == Nexxxt(kn+nn, S);
- assert forall j :: n <= j ==> Nexxxt(j, S) == null; // this uses Dafny's induction tactic
- assert false; // we have reached a contradiction
- }
- assert Nexxxt(kn+1, S).Nexxxt(ln, S) != Nexxxt(kn, S);
- }
- ln := ln + 1;
- }
- kn := kn + 1;
- }
- }
-}
|