1 files changed, 0 insertions, 133 deletions
diff --git a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy b/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
deleted file mode 100644
index 1c01eefc..00000000
--- a/Test/dafny2/COST-verif-comp-2011-2-MaxTree-class.dfy
+++ /dev/null
@@ -1,133 +0,0 @@
-/*
-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;
-    }
-  }
-}