1 files changed, 0 insertions, 93 deletions
diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy
deleted file mode 100644
index 62636ce5..00000000
--- a/Test/dafny0/ListContents.dfy
+++ /dev/null
@@ -1,93 +0,0 @@
-class Node<T> {
-  var list: seq<T>;
-  var footprint: set<Node<T>>;
-
-  var data: T;
-  var next: Node<T>;
-
-  function Valid(): bool
-    reads this, footprint;
-  {
-    this in this.footprint && null !in this.footprint &&
-    (next == null ==> list == [data]) &&
-    (next != null ==>
-        next in footprint && next.footprint <= footprint &&
-        this !in next.footprint &&
-        list == [data] + next.list &&
-        next.Valid())
-  }
-
-  method Init(d: T)
-    modifies this;
-    ensures Valid() && fresh(footprint - {this});
-    ensures list == [d];
-  {
-    data := d;
-    next := null;
-    list := [d];
-    footprint := {this};
-  }
-
-  method SkipHead() returns (r: Node<T>)
-    requires Valid();
-    ensures r == null ==> |list| == 1;
-    ensures r != null ==> r.Valid() && r.footprint <= footprint;
-    ensures r != null ==> r.list == list[1..];
-  {
-    r := next;
-  }
-
-  method Prepend(d: T) returns (r: Node<T>)
-    requires Valid();
-    ensures r != null && r.Valid() && fresh(r.footprint - old(footprint));
-    ensures r.list == [d] + list;
-  {
-    r := new Node<T>;
-    r.data := d;
-    r.next := this;
-    r.footprint := {r} + this.footprint;
-    r.list := [r.data] + this.list;
-  }
-
-  method ReverseInPlace() returns (reverse: Node<T>)
-    requires Valid();
-    modifies footprint;
-    ensures reverse != null && reverse.Valid();
-    ensures fresh(reverse.footprint - old(footprint));
-    ensures |reverse.list| == |old(list)|;
-    ensures (forall i :: 0 <= i && i < |old(list)| ==> old(list)[i] == reverse.list[|old(list)|-1-i]);
-  {
-    var current := next;
-    reverse := this;
-    reverse.next := null;
-    reverse.footprint := {reverse};
-    reverse.list := [data];
-
-    while (current != null)
-      invariant reverse != null && reverse.Valid();
-      invariant reverse.footprint <= old(footprint);
-      invariant current == null ==> |old(list)| == |reverse.list|;
-      invariant current != null ==>
-        current.Valid() &&
-        current in old(footprint) && current.footprint <= old(footprint) &&
-        current.footprint !! reverse.footprint &&
-        |old(list)| == |reverse.list| + |current.list| &&
-        (forall i :: 0 <= i && i < |current.list| ==> current.list[i] == old(list)[|reverse.list|+i]);
-      invariant
-        (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
-      decreases if current != null then |current.list| else -1;
-    {
-      var nx := current.next;
-      assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma
-
-      // ..., reverse, current, nx, ...
-      assert current.data == current.list[0]; // lemma
-      current.next := reverse;
-      current.footprint := {current} + reverse.footprint;
-      current.list := [current.data] + reverse.list;
-
-      reverse := current;
-      current := nx;
-    }
-  }
-}