1 files changed, 0 insertions, 92 deletions
diff --git a/Test/VSComp2010/Problem3-FindZero.dfy b/Test/VSComp2010/Problem3-FindZero.dfy
deleted file mode 100644
index 3d24255d..00000000
--- a/Test/VSComp2010/Problem3-FindZero.dfy
+++ /dev/null
@@ -1,92 +0,0 @@
-// VSComp 2010, problem 3, find a 0 in a linked list and return how many nodes were skipped
-// until the first 0 (or end-of-list) was found.
-// Rustan Leino, 18 August 2010.
-//
-// The difficulty in this problem lies in specifying what the return value 'r' denotes and in
-// proving that the program terminates.  Both of these are addressed by declaring a ghost
-// field 'List' in each linked-list node, abstractly representing the linked-list elements
-// from the node to the end of the linked list.  The specification can now talk about that
-// sequence of elements and can use 'r' as an index into the sequence, and termination can
-// be proved from the fact that all sequences in Dafny are finite.
-//
-// We only want to deal with linked lists whose 'List' field is properly filled in (which
-// can only happen in an acyclic list, for example).  To that avail, the standard idiom in
-// Dafny is to declare a predicate 'Valid()' that is true of an object when the data structure
-// representing object's abstract value is properly formed.  The definition of 'Valid()'
-// is what one intuitively would think of as the ''object invariant'', and it is mentioned
-// explicitly in method pre- and postconditions.  As part of this standard idiom, one also
-// declared a ghost variable 'Repr' that is maintained as the set of objects that make up
-// the representation of the aggregate object--in this case, the Node itself and all its
-// successors.
-
-class Node {
-  ghost var List: seq<int>;
-  ghost var Repr: set<Node>;
-  var head: int;
-  var next: Node;
-
-  function Valid(): bool
-    reads this, Repr;
-  {
-    this in Repr &&
-    1 <= |List| && List[0] == head &&
-    (next == null ==> |List| == 1) &&
-    (next != null ==>
-      next in Repr && next.Repr <= Repr && this !in next.Repr && next.Valid() && next.List == List[1..])
-  }
-
-  static method Cons(x: int, tail: Node) returns (n: Node)
-    requires tail == null || tail.Valid();
-    ensures n != null && n.Valid();
-    ensures if tail == null then n.List == [x] else n.List == [x] + tail.List;
-  {
-    n := new Node;
-    n.head := x;
-    n.next := tail;
-    if (tail == null) {
-      n.List := [x];
-      n.Repr := {n};
-    } else {
-      n.List := [x] + tail.List;
-      n.Repr := {n} + tail.Repr;
-    }
-  }
-}
-
-static method Search(ll: Node) returns (r: int)
-  requires ll == null || ll.Valid();
-  ensures ll == null ==> r == 0;
-  ensures ll != null ==>
-            0 <= r && r <= |ll.List| &&
-            (r < |ll.List| ==> ll.List[r] == 0 && 0 !in ll.List[..r]) &&
-            (r == |ll.List| ==> 0 !in ll.List);
-{
-  if (ll == null) {
-    r := 0;
-  } else {
-    var jj := ll;
-    var i := 0;
-    while (jj != null && jj.head != 0)
-      invariant jj != null ==> jj.Valid() && i + |jj.List| == |ll.List| && ll.List[i..] == jj.List;
-      invariant jj == null ==> i == |ll.List|;
-      invariant 0 !in ll.List[..i];
-      decreases |ll.List| - i;
-    {
-      jj := jj.next;
-      i := i + 1;
-    }
-    r := i;
-  }
-}
-
-method Main()
-{
-  var list: Node := null;
-  list := list.Cons(0, list);
-  list := list.Cons(5, list);
-  list := list.Cons(0, list);
-  list := list.Cons(8, list);
-  var r := Search(list);
-  print "Search returns ", r, "\n";
-  assert r == 1;
-}