1 files changed, 0 insertions, 91 deletions
diff --git a/Chalice/tests/examples/linkedlist.chalice b/Chalice/tests/examples/linkedlist.chalice
deleted file mode 100644
index a9859aaa..00000000
--- a/Chalice/tests/examples/linkedlist.chalice
+++ /dev/null
@@ -1,91 +0,0 @@
-/* Recursive implementation and specification of a linked list. */
-
-class Node {
-  var next: Node;
-  var value: int;
-
-  method init(v: int)
-    requires acc(next) && acc(value);
-    ensures valid && size() == 1 && (forall y:int :: contains(y) <==> y==v);
-  {
-    next := null;
-    value := v;
-    fold this.valid;
-  }
-
-  method add(x: int) 
-    requires valid;
-    ensures valid;
-    ensures size() == old(size())+1;
-    ensures (forall y:int :: contains(y)==(old(contains(y)) || x==y));
-  {
-    unfold this.valid;
-    if(next==null) {
-      var n : Node;
-      n := new Node;
-      call n.init(x);
-      next := n;
-      // unfold next.valid; fold next.valid; // makes it work
-    } else {
-
-      call next.add(x);
-    }
-    fold this.valid;
-  }
-  
-    method addother(i:int)
-      requires valid
-      ensures valid && (forall x:int :: contains(x)==(old(contains(x)) || x==i))
-    {
-      unfold valid
-      if(next!=null)
-      { 
-        call next.addother(i)
-      }
-      else
-      {  
-        next:=new Node
-        next.value:=i
-        next.next:=null
-        fold next.valid
-      }
-      fold valid
-  }
-
-  method addFirst(x: int) returns (rt: Node)
-    requires valid;
-    ensures rt!=null && rt.valid;
-    ensures rt.size() == old(size()) + 1;
-  {
-    var n: Node;
-    n := new Node;
-    n.value := x;
-    n.next := this; 
-    fold n.valid;
-    rt := n;
-  }
-
-  function at(i: int): int
-    requires valid && 0<=i && i<size();
-  {
-    unfolding valid in i==0 ? value : next.at(i-1)
-  }
-
-  function size(): int
-    requires valid;
-    ensures result > 0
-  {
-    unfolding this.valid in (next!=null ? 1+ next.size() : 1)
-  }
-  
-  function contains(i:int):bool
-    requires valid
-  {
-    unfolding valid in i==value || (next!=null && next.contains(i))
-  }
-
-
-  predicate valid {
-    acc(next) && acc(value) && (next!=null ==> next.valid)
-  }
-}
-\ No newline at end of file