1 files changed, 0 insertions, 27 deletions
diff --git a/Test/dafny1/ListReverse.dfy b/Test/dafny1/ListReverse.dfy
deleted file mode 100644
index ef029b88..00000000
--- a/Test/dafny1/ListReverse.dfy
+++ /dev/null
@@ -1,27 +0,0 @@
-
-class Node {
-  var nxt: Node;
-
-  method ReverseInPlace(x: Node, r: set<Node>) returns (reverse: Node)
-    requires null !in r;
-    requires x == null || x in r;
-    requires (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure
-    modifies r;
-    ensures reverse == null || reverse in r;
-    ensures (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure
-  {
-    var current := x;
-    reverse := null;
-    while (current != null)
-      invariant current == null || current in r;
-      invariant reverse == null || reverse in r;
-      invariant (forall y :: y in r ==> y.nxt == null || y.nxt in r);  // region closure
-      decreases *;  // omit loop termination check
-    {
-      var tmp := current.nxt;
-      current.nxt := reverse;
-      reverse := current;
-      current := tmp;
-    }
-  }
-}