1 files changed, 0 insertions, 163 deletions
diff --git a/Chalice/tests/examples/cell.chalice b/Chalice/tests/examples/cell.chalice
deleted file mode 100644
index 1cf82950..00000000
--- a/Chalice/tests/examples/cell.chalice
+++ /dev/null
@@ -1,163 +0,0 @@
-class Cell module Library {
-  var x: int;
-
-  method init(v: int)
-    requires acc(this.x) && 0<=v;
-    ensures valid && this.get() == v;
-  {
-    x := v;
-    fold valid;
-  }
-
-  method set(v: int)
-    requires valid && 0<=v;
-    ensures valid && get()==v;
-  {
-    unfold valid;
-    x := v;
-    fold valid;
-  }
-  
-  method increment()
-    requires valid;
-    ensures valid && get() == old(get()) + 1;
-  {
-    unfold valid;
-    x := x + 1;
-    fold valid;
-  }
-
-  method dispose()
-    requires valid && acc(mu);
-    ensures true;
-  {
-    unfold valid;
-    free this;
-  }
-
-  function get(): int
-    requires valid;
-    ensures 0<=result;
-  {
-    unfolding valid in x
-  }
-
-  predicate valid {
-    acc(this.x) && 0<=x
-  }
-
-  invariant valid;
-}
-
-class Interval module Library2 {
-  var left: Cell;
-  var right: Cell;
-
-  method init(l: int, r: int)
-    requires 0<=l && l <= r;
-    requires acc(left) && acc(right);
-    ensures valid;
-    ensures getLeft()==l;
-    ensures getRight()==r;
-  {
-    left := new Cell;
-    call left.init(l);
-    right := new Cell;
-    call right.init(r);
-    fold valid;
-  }
-
-  method setLeft(l: int)
-    requires valid;
-    requires 0<=l && l<=getRight();
-    ensures valid;
-    ensures getLeft()==l && getRight()==old(getRight());
-  {
-    unfold valid;
-    call left.set(l);
-    fold valid;
-  }
-
-  method setRight(r: int)
-    requires valid;
-    requires 0<=r && getLeft()<=r;
-    ensures valid;
-    ensures getLeft()==old(getLeft()) && getRight()==r;
-  {
-    unfold valid;
-    call right.set(r);
-    fold valid;
-  }
-
-  method shift(v: int)
-    requires valid;
-    requires 0<=v;
-    ensures valid;
-    ensures getLeft()==old(getLeft())+v && getRight()==old(getRight())+v;
-  {
-    unfold valid;
-    call left.set(left.get()+v);
-    call right.set(right.get()+v);
-    fold valid;
-  }
-
-  function getLeft() : int
-    requires valid;
-  {
-    unfolding valid in left.get()
-  }
-
-  function getRight() : int
-    requires valid;
-  {
-    unfolding valid in right.get()
-  }
-  
-  predicate valid
-  {
-    acc(left) && acc(right) && left!=null && right!=null && left.valid && right.valid && left.get() <= right.get()
-  }
-}
-
-class Program module Main {
-  method main(){
-    var c1 := new Cell;
-    call c1.init(5);
-    call c1.set(6);
-
-    var c2 := new Cell;
-    call c2.init(10);
-    call c2.set(11);
-
-    assert c1.get() == 6;
-  }
-
-  method main2(){
-    var c: Cell;
-
-    c := new Cell;
-    call c.init(0);
-    call c.dispose();
-
-    assert c.valid; // should fail
-  }
-
-  method main3() returns (rt: Cell)
-    ensures rt!=null && rt.valid && rt.get() == 0;
-  {
-    rt := new Cell;
-    call rt.init(0);
-  }
-
-  method main4() {
-    var c: Cell;
-
-    c := new Cell;
-    call c.init(0);
-    share c;
-
-    acquire c;
-    call c.set(1);
-    release c;
-  }
-}
-\ No newline at end of file