1 files changed, 0 insertions, 169 deletions
diff --git a/Test/dafny1/SeparationLogicList.dfy b/Test/dafny1/SeparationLogicList.dfy
deleted file mode 100644
index 56a64bd6..00000000
--- a/Test/dafny1/SeparationLogicList.dfy
+++ /dev/null
@@ -1,169 +0,0 @@
-// This file contains three variations of the separation-logic lseg linked-list example.
-
-// In this first variation, the auxiliary information about the contents represented by a linked list
-// and the subpart of the heap that the list occupies is passed around as additional parameters.  In
-// separation logic, the contents (here called 'q') would indeed be passed around in that way, whereas
-// separating conjunction and the abstract predicate ListSegment would take care of staking out which
-// subpart of the heap is being occupied by the linked-list representation.
-class Node<T> {
-  var data: T;
-  var next: Node<T>;
-
-  static function ListSegment(q: seq<T>, from: Node<T>, to: Node<T>, S: set<Node<T>>): bool
-    reads S;
-  {
-    if q == []
-    then from == to
-    else from != null && from in S && from.data == q[0] && ListSegment(q[1..], from.next, to, S - {from})
-  }
-
-  static method Create(x: T) returns (l: Node<T>, ghost S: set<Node<T>>)
-    ensures ListSegment([x], l, null, S) && fresh(S);
-  {
-    // By using the following non-deterministic 'if' statement, the example shows that 'Create' can be
-    // implemented either directly or by call 'Cons'.
-    if (*) {
-      l := new Node<T>;
-      l.data := x;
-      l.next := null;
-      S := {l};
-    } else {
-      l, S := Cons(x, null, [], {});
-    }
-  }
-
-  static method Cons(x: T, tail: Node<T>, ghost q: seq<T>, ghost S: set<Node<T>>) returns (l: Node<T>, ghost U: set<Node<T>>)
-    requires ListSegment(q, tail, null, S);
-    ensures ListSegment([x] + q, l, null, U) && fresh(U - S);
-  {
-    l := new Node<T>;
-    l.data := x;
-    l.next := tail;
-    U := S + {l};
-  }
-}
-
-// The following class is a variation of the one above.  The difference is that, in this one, each node
-// keeps track of its own contents (called 'q' above) and representation (called 'S' and 'U' above).
-class ListNode<T> {
-  ghost var Contents: seq<T>;
-  ghost var Repr: set<ListNode<T>>;
-
-  var data: T;
-  var next: ListNode<T>;
-
-  static function IsList(l: ListNode<T>): bool
-    reads l, l.Repr;
-  {
-    if l == null then
-      true
-    else if l.next == null then
-      l in l.Repr && l.Contents == [l.data]
-    else
-      {l, l.next} <= l.Repr && l.Contents == [l.data] + l.next.Contents && l.next.Repr <= l.Repr - {l} && IsList(l.next)
-  }
-
-  static method Create(x: T) returns (l: ListNode<T>)
-    ensures IsList(l) && l != null && l.Contents == [x] && fresh({l} + l.Repr);
-  {
-    // By using the following non-deterministic 'if' statement, the example shows that 'Create' can be
-    // implemented either directly or by call 'Cons'.
-    if (*) {
-      l := new ListNode<T>;
-      l.data := x;
-      l.next := null;
-      l.Repr := {l};
-      l.Contents := [x];
-    } else {
-      l := Cons(x, null);
-    }
-  }
-
-  static method Cons(x: T, tail: ListNode<T>) returns (l: ListNode<T>)
-    requires IsList(tail);
-    ensures IsList(l) && l != null;
-    ensures tail == null ==> l.Contents == [x] && fresh({l} + l.Repr);
-    ensures tail != null ==> l.Contents == [x] + tail.Contents && fresh({l} + l.Repr - tail.Repr);
-  {
-    l := new ListNode<T>;
-    l.data := x;
-    l.next := tail;
-    if (tail != null) {
-      l.Repr := tail.Repr + {l};
-      l.Contents := [x] + tail.Contents;
-    } else {
-      l.Repr := {l};
-      l.Contents := [x];
-    }
-  }
-}
-
-// In this final variation, a list, empty or not, is represented by a List object.  The representation
-// of a List object includes a number of linked-list nodes.  To make the treatment of the empty list
-// nicer than in the class above, the List object starts its list with a sentinel object whose 'data'
-// field is not used.
-class List<T>
-{
-  ghost var Contents: seq<T>;
-  ghost var Repr: set<object>;
-  var head: LLNode<T>;
-
-  function IsList(): bool
-    reads this, Repr;
-  {
-    this in Repr && head != null && head in Repr &&
-    head.Repr <= Repr && this !in head.Repr && head.IsWellFormed() &&
-    Contents == head.TailContents
-  }
-
-  method Init()
-    modifies this;
-    ensures IsList() && Contents == [] && fresh(Repr - {this});
-  {
-    var h := new LLNode<T>;
-    h.next := null;
-    h.TailContents := [];
-    h.Repr := {h};
-
-    head := h;
-    Contents := [];
-    Repr := {this} + h.Repr;
-  }
-
-  method Cons(x: T)
-    requires IsList();
-    modifies Repr;
-    ensures IsList() && Contents == [x] + old(Contents) && fresh(Repr - old(Repr));
-  {
-    head.data := x;
-    assert head.IsWellFormed();  // head remains well-formed even after assigning to an object (namely, head) in head.Repr
-
-    var h := new LLNode<T>;
-    h.next := head;
-    h.TailContents := [x] + head.TailContents;
-    h.Repr := {h} + head.Repr;
-
-    head := h;
-    Contents := [x] + Contents;
-    Repr := Repr + {h};
-  }
-}
-
-class LLNode<T>
-{
-  var data: T;
-  var next: LLNode<T>;
-  ghost var TailContents: seq<T>;
-  ghost var Repr: set<object>;
-
-  function IsWellFormed(): bool
-    reads this, Repr;
-  {
-    this in Repr &&
-    (next == null ==> TailContents == []) &&
-    (next != null ==>
-      next in Repr &&
-      next.Repr <= Repr && this !in next.Repr && next.IsWellFormed() &&
-      TailContents == [next.data] + next.TailContents)
-  }
-}