Dafny: added COST Verification Competition challenge programs to test suite

7 files changed, 832 insertions, 1 deletions

diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer
index d052c463..81db547b 100644
--- a/Test/dafny2/Answer
+++ b/Test/dafny2/Answer
@@ -6,3 +6,23 @@ Dafny program verifier finished with 37 verified, 0 errors
 -------------------- TreeBarrier.dfy --------------------

 

 Dafny program verifier finished with 8 verified, 0 errors

+

+-------------------- COST-verif-comp-2011-1-MaxArray.dfy --------------------

+

+Dafny program verifier finished with 2 verified, 0 errors

+

+-------------------- COST-verif-comp-2011-2-MaxTree-class.dfy --------------------

+

+Dafny program verifier finished with 8 verified, 0 errors

+

+-------------------- COST-verif-comp-2011-2-MaxTree-datatype.dfy --------------------

+

+Dafny program verifier finished with 5 verified, 0 errors

+

+-------------------- COST-verif-comp-2011-3-TwoDuplicates.dfy --------------------

+

+Dafny program verifier finished with 4 verified, 0 errors

+

+-------------------- COST-verif-comp-2011-4-FloydCycleDetect.dfy --------------------

+

+Dafny program verifier finished with 23 verified, 0 errors

diff --git a/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy b/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
new file mode 100644
index 00000000..f67d7870
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-1-MaxArray.dfy
@@ -0,0 +1,79 @@
+/*

+Rustan Leino, 5 Oct 2011

+

+COST Verification Competition, Challenge 1: Maximum in an array

+http://foveoos2011.cost-ic0701.org/verification-competition

+

+Given: A non-empty integer array a.

+

+Verify that the index returned by the method max() given below points to

+an element maximal in the array.

+

+public class Max {

+    public static int max(int[] a) {

+        int x = 0;

+        int y = a.length-1;

+

+        while (x != y) {

+            if (a[x] <= a[y]) x++;

+                else y--;

+        }

+        return x;

+    }

+}

+*/

+

+// Remarks:

+

+// The verification of the loop makes use of a local ghost variable 'm'.  To the

+// verifier, this variable is like any other, but the Dafny compiler ignores it.

+// In other words, ghost variables and ghost assignments (and specifications,

+// for that matter) are included in the program just for the purpose of reasoning

+// about the program, and they play no role at run time.

+

+// The only thing that needs to be human-trusted about this program is the

+// specification of 'max' (and, since verification challenge asked to prove

+// something about a particular piece of code, that the body of 'max', minus

+// the ghost constructs, is really that code).

+

+// 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 2 seconds)

+// without further human intervention.

+

+method max(a: array<int>) returns (x: int)

+  requires a != null && a.Length != 0;

+  ensures 0 <= x < a.Length;

+  ensures forall i :: 0 <= i < a.Length ==> a[i] <= a[x];

+{

+  x := 0;

+  var y := a.Length - 1;

+  ghost var m := y;

+  while (x != y)

+    invariant 0 <= x <= y < a.Length;

+    invariant m == x || m == y;

+    invariant forall i :: 0 <= i < x ==> a[i] <= a[m];

+    invariant forall i :: y < i < a.Length ==> a[i] <= a[m];

+  {

+    if (a[x] <= a[y]) {

+      x := x + 1;  m := y;

+    } else {

+      y := y - 1;  m := x;

+    }

+  }

+  return x;

+}

diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
new file mode 100644
index 00000000..1c01eefc
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
@@ -0,0 +1,133 @@
+/*

+Rustan Leino, 5 Oct 2011

+

+COST Verification Competition, Challenge 2: Maximum in a tree

+http://foveoos2011.cost-ic0701.org/verification-competition

+

+Given: A non-empty binary tree, where every node carries an integer.

+

+Implement and verify a program that computes the maximum of the values

+in the tree.

+

+Please base your program on the following data structure signature:

+

+public class Tree {

+    int value;

+    Tree left;

+    Tree right;

+}

+

+You may represent empty trees as null references or as you consider

+appropriate.

+*/

+

+// Remarks:

+

+// The specification of this program uses the common dynamic-frames idiom in Dafny:  the

+// ghost field 'Contents' stores the abstract value of an object, the ghost field 'Repr'

+// stores the set of (references to) objects that make up the representation of the object

+// (which in this case is the Tree itself plus the 'Repr' sets of the left and right

+// subtrees), and a function 'Valid()' that returns 'true' when an object is in a

+// consistent state (that is, when an object satisfies the "class invariant").

+

+// The design I used was to represent an empty tree as a Tree object whose left and

+// right pointers point to the object iself.  This is convenient, because it lets

+// clients of Tree and the implementation of Tree always use non-null pointers to

+// Tree objects.

+

+// What needs to be human-trusted about this program is that the 'requires' and

+// 'ensures' clauses (that is, the pre- and postconditions, respectively) of

+// 'ComputeMax' are correct.  And, since the specification talks about the ghost

+// variable 'Contents', one also needs to trust that the 'Valid()' function

+// constrains 'Contents' in a way that a human thinks matches the intuitive

+// definition of what the contents of a tree is.

+

+// To give a taste of that the 'Valid()' function does not over-constrain the

+// object, I have included two instance constructors, 'Empty()' and 'Node(...)'.

+// To take this a step further, one could also write a 'Main' method that

+// builds somme tree and then calls 'ComputeMax', but I didn't do that here.

+

+// 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 2.5 seconds)

+// without further human intervention.

+

+class Tree {

+  // an empty tree is represented by a Tree object with left==this==right

+  var value: int;

+  var left: Tree;

+  var right: Tree;

+

+  ghost var Contents: seq<int>;

+  ghost var Repr: set<object>;

+  function Valid(): bool

+    reads this, Repr;

+  {

+    this in Repr &&

+    left != null && right != null &&

+    ((left == this == right && Contents == []) ||

+     (left in Repr && left.Repr <= Repr && this !in left.Repr &&

+      right in Repr && right.Repr <= Repr && this !in right.Repr &&

+      left.Valid() && right.Valid() &&

+      Contents == left.Contents + [value] + right.Contents))

+  }

+

+  function method IsEmpty(): bool

+    requires Valid();

+    reads Repr;

+    ensures IsEmpty() <==> Contents == [];

+  {

+    left == this

+  }

+

+  constructor Empty()

+    modifies this;

+    ensures Valid() && Contents == [];

+  {

+    left, right := this, this;

+    Contents := [];

+    Repr := {this};

+  }

+

+  constructor Node(lft: Tree, val: int, rgt: Tree)

+    requires lft != null && rgt != null && lft.Valid() && rgt.Valid();

+    requires this !in lft.Repr && this !in rgt.Repr;

+    modifies this;

+    ensures Valid() && Contents == lft.Contents + [val] + rgt.Contents;

+  {

+    left, value, right := lft, val, rgt;

+    Contents := lft.Contents + [val] + rgt.Contents;

+    Repr := lft.Repr + {this} + rgt.Repr;

+  }

+

+  method ComputeMax() returns (mx: int)

+    requires Valid() && !IsEmpty();

+    ensures forall x :: x in Contents ==> x <= mx;

+    ensures exists x :: x in Contents && x == mx;

+    decreases Repr;

+  {

+    mx := value;

+    if (!left.IsEmpty()) {

+      var m := left.ComputeMax();

+      mx := if mx < m  then m else mx;

+    }

+    if (!right.IsEmpty()) {

+      var m := right.ComputeMax();

+      mx := if mx < m then m else mx;

+    }

+  }

+}

diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
new file mode 100644
index 00000000..8dd7bd2d
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-datatype.dfy
@@ -0,0 +1,65 @@
+// This Dafny program was inspired by Claude Marche's Why3ML program that solves

+// Challenge 2 of the COST Verification Competition.  It particular, it uses an

+// inductive datatype for the Tree data structure, and it uses a Contains function

+// defined on such trees.  This makes the whole program short and sweet, keeps

+// proof annotation overhead to a minimum, and--best of all--makes for a convincing

+// specification of Max.

+// Rustan Leino, 7 Oct 2011

+

+// Remarks:

+

+// A little detail about the implementation of 'Max' below is that the precondition

+// 't != Null' means that the 'match' statement does not need to include a case

+// for 'Null'.  The correctness of the omission of cases is checked by the program

+// verifier.

+

+// 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 2 seconds)

+// without further human intervention.

+

+datatype Tree = Null | Node(Tree, int, Tree);

+

+function Contains(t: Tree, v: int): bool

+{

+  match t

+  case Null => false

+  case Node(left, x, right) => x == v || Contains(left, v) || Contains(right, v)

+}

+

+method Max(t: Tree) returns (result: int)

+  requires t != Null;

+  ensures Contains(t, result) && forall v :: Contains(t, v) ==> v <= result;

+{

+  match (t) {

+    case Node(left, x, right) =>

+      result := MaxAux(right, x);

+      result := MaxAux(left, result);

+  }

+}

+

+method MaxAux(t: Tree, acc: int) returns (result: int)

+  ensures result == acc || Contains(t, result);

+  ensures acc <= result && forall v :: Contains(t, v) ==> v <= result;

+{

+  match (t) {

+    case Null => result := acc;

+    case Node(left, x, right) =>

+      result := MaxAux(right, if x < acc then acc else x);

+      result := MaxAux(left, result);

+  }

+}

diff --git a/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy
new file mode 100644
index 00000000..069baa61
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-3-TwoDuplicates.dfy
@@ -0,0 +1,118 @@
+/*

+Rustan Leino, 5 Oct 2011

+

+COST Verification Competition, Challenge 3: Two equal elements

+http://foveoos2011.cost-ic0701.org/verification-competition

+

+Given: An integer array a of length n+2 with n>=2. It is known that at

+least two values stored in the array appear twice (i.e., there are at

+least two duplets).

+

+Implement and verify a program finding such two values.

+

+You may assume that the array contains values between 0 and n-1.

+*/

+

+// Remarks:

+

+// The implementation of method 'Search' takes one pass through the elements of

+// the given array.  To keep track of what it has seen, it allocates an array as

+// temporary storage--I imagine that this is what the competition designers

+// had in mind, since the problem description says one can assume the values

+// of the given array to lie in the range 0..n.

+

+// To keep track of whether it already has found one duplicate, the method

+// sets the output variables p and q as follows:

+//   p != q   - no duplicates found yet

+//   p == q   - one duplicate found so far, namely the value stored in p and q

+// Note, the loop invariant does not need to say anything about the state

+// of two duplicates having been found, because when the second duplicate is

+// found, the method returns.

+

+// What needs to be human-trusted about this program is the specification of

+// 'Search'.  The specification straightforwardly lists the assumptions stated

+// in the problem description, including the given fact that the array contains

+// (at least) two distinct elements that each occurs (at least) twice.  To

+// trust the specification of 'Search', a human also needs to trust the definition

+// of 'IsDuplicate' and its auxiliary function 'IsPrefixDuplicate'.

+

+// 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 11 seconds)

+// without further human intervention.

+

+function IsDuplicate(a: array<int>, p: int): bool

+  requires a != null;

+  reads a;

+{

+  IsPrefixDuplicate(a, a.Length, p)

+}

+

+function IsPrefixDuplicate(a: array<int>, k: int, p: int): bool

+  requires a != null && 0 <= k <= a.Length;

+  reads a;

+{

+  exists i,j :: 0 <= i < j < k && a[i] == a[j] == p

+}

+

+method Search(a: array<int>) returns (p: int, q: int)

+  requires a != null && 4 <= a.Length;

+  requires exists p,q :: p != q && IsDuplicate(a, p) && IsDuplicate(a, q);  // two distinct duplicates exist

+  requires forall i :: 0 <= i < a.Length ==> 0 <= a[i] < a.Length - 2;  // the elements of "a" in the range [0.. a.Length-2]

+  ensures p != q && IsDuplicate(a, p) && IsDuplicate(a, q);

+{

+  // allocate an array "d" and initialize its elements to -1.

+  var d := new int[a.Length-2];

+  var i := 0;

+  while (i < d.Length)

+    invariant 0 <= i <= d.Length && forall j :: 0 <= j < i ==> d[j] == -1;

+  {

+    d[i], i := -1, i+1;

+  }

+

+  i, p, q := 0, 0, 1;

+  while (true)

+    invariant 0 <= i < a.Length;

+    invariant forall j :: 0 <= j < d.Length ==>

+                (d[j] == -1 && forall k :: 0 <= k < i ==> a[k] != j) ||

+                (0 <= d[j] < i && a[d[j]] == j);

+    invariant p == q ==> IsDuplicate(a, p);

+    invariant forall k :: 0 <= k < i && IsPrefixDuplicate(a, i, a[k]) ==> p == q == a[k];

+    decreases a.Length - i;

+  {

+    var k := d[a[i]];

+    assert k < i;  // note, this assertion is really for human consumption; it is not needed by the verifier, and it does not change the performance of the verifier

+    if (k == -1) {

+      // a[i] does not exist in a[..i]

+      d[a[i]] := i;

+    } else {

+      // we have encountered a duplicate

+      assert a[i] == a[k] && IsDuplicate(a, a[i]);  // note, this assertion is really for human consumption; it is not needed by the verifier, and it does not change the performance of the verifier

+      if (p != q) {

+        // this is the first duplicate encountered

+        p, q := a[i], a[i];

+      } else if (p == a[i]) {

+        // this is another copy of the same duplicate we have seen before

+      } else {

+        // this is the second duplicate

+        q := a[i];

+        return;

+      }

+    }

+    i := i + 1;

+  }

+}

diff --git a/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
new file mode 100644
index 00000000..d846269d
--- /dev/null
+++ b/Test/dafny2/COST-verif-comp-2011-4-FloydCycleDetect.dfy
@@ -0,0 +1,410 @@
+/*

+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);

+    // The next line most straightforwardly expresses the postcondition of this method:

+    //   ensures exists T :: 0 <= T <= a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S);

+    // However, Dafny does an unfortunate (I would say performance-buggy) translation of existential

+    // quantifiers, which the alternative formulation of "exists x :: P(x)" as

+    // "(forall x :: !P(x)) ==> false" works around.  This translation issue should be fixed.

+    ensures (forall T :: !(0 <= T <= a+b && Nexxxt(T, S) == Nexxxt(1+2*T, S))) ==> false;

+  {

+    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);

+      assert exists T :: 0 <= 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;

+    }

+  }

+}

diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat
index 62b0b6fe..f6f25429 100644
--- a/Test/dafny2/runtest.bat
+++ b/Test/dafny2/runtest.bat
@@ -5,7 +5,13 @@ set BOOGIEDIR=..\..\Binaries
 set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

 set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe

 

-for %%f in (SnapshotableTrees.dfy TreeBarrier.dfy) do (

+for %%f in (SnapshotableTrees.dfy TreeBarrier.dfy

+    COST-verif-comp-2011-1-MaxArray.dfy

+    COST-verif-comp-2011-2-MaxTree-class.dfy

+    COST-verif-comp-2011-2-MaxTree-datatype.dfy

+    COST-verif-comp-2011-3-TwoDuplicates.dfy

+    COST-verif-comp-2011-4-FloydCycleDetect.dfy

+  ) do (

   echo.

   echo -------------------- %%f --------------------