1 files changed, 0 insertions, 199 deletions
diff --git a/Test/VSI-Benchmarks/b5.dfy b/Test/VSI-Benchmarks/b5.dfy
deleted file mode 100644
index 612b96ba..00000000
--- a/Test/VSI-Benchmarks/b5.dfy
+++ /dev/null
@@ -1,199 +0,0 @@
-
-
-class Queue<T> {
-  var head: Node<T>;
-  var tail: Node<T>;
-
-  ghost var contents: seq<T>;
-  ghost var footprint: set<object>;
-  ghost var spine: set<Node<T>>;
-
-  function Valid(): bool
-    reads this, footprint;
-  {
-    this in footprint && spine <= footprint &&
-    head != null && head in spine &&
-    tail != null && tail in spine &&
-    tail.next == null &&
-    (forall n ::
-      n in spine ==>
-        n != null && n.footprint <= footprint && this !in n.footprint &&
-        n.Valid() &&
-        (n.next == null ==> n == tail)) &&
-    (forall n ::
-      n in spine ==>
-        n.next != null ==> n.next in spine) &&
-    contents == head.tailContents
-  }
-
-  method Init()
-    modifies this;
-    ensures Valid() && fresh(footprint - {this});
-    ensures |contents| == 0;
-  {
-    var n := new Node<T>.Init();
-    head := n;
-    tail := n;
-    contents := n.tailContents;
-    footprint := {this} + n.footprint;
-    spine := {n};
-  }
-
-  method IsEmpty() returns (isEmpty: bool)
-    requires Valid();
-    ensures isEmpty <==> |contents| == 0;
-  {
-    isEmpty := head == tail;
-  }
-
-  method Enqueue(t: T)
-    requires Valid();
-    modifies footprint;
-    ensures Valid() && fresh(footprint - old(footprint));
-    ensures contents == old(contents) + [t];
-  {
-    var n := new Node<T>.Init();
-    n.data := t;
-    tail.next := n;
-    tail := n;
-
-    parallel (m | m in spine) {
-      m.tailContents := m.tailContents + [t];
-    }
-    contents := head.tailContents;
-
-    parallel (m | m in spine) {
-      m.footprint := m.footprint + n.footprint;
-    }
-    footprint := footprint + n.footprint;
-
-    spine := spine + {n};
-  }
-
-  method Front() returns (t: T)
-    requires Valid();
-    requires 0 < |contents|;
-    ensures t == contents[0];
-  {
-    t := head.next.data;
-  }
-
-  method Dequeue()
-    requires Valid();
-    requires 0 < |contents|;
-    modifies footprint;
-    ensures Valid() && fresh(footprint - old(footprint));
-    ensures contents == old(contents)[1..];
-  {
-    var n := head.next;
-    head := n;
-    contents := n.tailContents;
-  }
-  
-  
-  method Rotate()
-    requires Valid();
-    requires 0 < |contents|;
-    modifies footprint;
-    ensures Valid() && fresh(footprint - old(footprint));
-    ensures contents == old(contents)[1..] + old(contents)[..1];
-  {
-    var t := Front();
-    Dequeue();
-    Enqueue(t);
-  }
-
-  method RotateAny()
-    requires Valid();
-    requires 0 < |contents|;
-    modifies footprint;
-    ensures Valid() && fresh(footprint - old(footprint));
-    ensures |contents| == |old(contents)|;
-    ensures (exists i :: 0 <= i && i <= |contents| &&
-              contents == old(contents)[i..] + old(contents)[..i]);
-  {
-    var t := Front();
-    Dequeue();
-    Enqueue(t);
-  }
-
-}
-
-class Node<T> {
-  var data: T;
-  var next: Node<T>;
-
-  ghost var tailContents: seq<T>;
-  ghost var footprint: set<object>;
-
-  function Valid(): bool
-    reads this, footprint;
-  {
-    this in footprint &&
-    (next != null ==> next in footprint && next.footprint <= footprint) &&
-    (next == null ==> tailContents == []) &&
-    (next != null ==> tailContents == [next.data] + next.tailContents)
-  }
-
-  method Init()
-    modifies this;
-    ensures Valid() && fresh(footprint - {this});
-    ensures next == null;
-  {
-    next := null;
-    tailContents := [];
-    footprint := {this};
-  }
-}
-
-class Main<U> {
-  method A<T>(t: T, u: T, v: T)
-  {
-    var q0 := new Queue<T>.Init();
-    var q1 := new Queue<T>.Init();
-
-    q0.Enqueue(t);
-    q0.Enqueue(u);
-
-    q1.Enqueue(v);
-
-    assert |q0.contents| == 2;
-
-    var w := q0.Front();
-    assert w == t;
-    q0.Dequeue();
-
-    w := q0.Front();
-    assert w == u;
-
-    assert |q0.contents| == 1;
-    assert |q1.contents| == 1;
-  }
-
-  method Main2(t: U, u: U, v: U, q0: Queue<U>, q1: Queue<U>)
-    requires q0 != null && q0.Valid();
-    requires q1 != null && q1.Valid();
-    requires q0.footprint !! q1.footprint;
-    requires |q0.contents| == 0;
-    modifies q0.footprint, q1.footprint;
-    ensures fresh(q0.footprint - old(q0.footprint));
-    ensures fresh(q1.footprint - old(q1.footprint));
-  {
-    q0.Enqueue(t);
-    q0.Enqueue(u);
-
-    q1.Enqueue(v);
-
-    assert |q0.contents| == 2;
-
-    var w := q0.Front();
-    assert w == t;
-    q0.Dequeue();
-
-    w := q0.Front();
-    assert w == u;
-
-    assert |q0.contents| == 1;
-    assert |q1.contents| == old(|q1.contents|) + 1;
-  }
-}