1 files changed, 27 insertions, 0 deletions
diff --git a/Test/dafny1/ListReverse.dfy b/Test/dafny1/ListReverse.dfy
new file mode 100644
index 00000000..ef029b88
--- /dev/null
+++ b/Test/dafny1/ListReverse.dfy
@@ -0,0 +1,27 @@
+
+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;
+    }
+  }
+}