1 files changed, 0 insertions, 112 deletions
diff --git a/Chalice/tests/refinements/Counter.chalice b/Chalice/tests/refinements/Counter.chalice
deleted file mode 100644
index d1efae76..00000000
--- a/Chalice/tests/refinements/Counter.chalice
+++ /dev/null
@@ -1,112 +0,0 @@
-class Counter0 {
-  var x: int;
-  
-  method init() 
-    requires acc(x); 
-    ensures acc(x) && x == 0;
-  {
-    x := 0;  
-  }
-
-  method inc()
-    requires acc(x);
-    ensures acc(x) && x == old(x) + 1;
-  {
-    x := x + 1;
-  } 
-
-  method dec()
-    requires acc(x);
-    ensures acc(x) && x == old(x) - 1;
-  {    
-    x := x - 1;  
-  }
-
-  method magic() returns (c: Cell)
-    requires acc(x);
-    ensures acc(x) && acc(c.n) && x == old(x);
-  {
-    var c [acc(c.n)]
-  }
-}
-
-class Counter1 refines Counter0 {
-  var y: int;
-  var z: int;  
-  replaces x by acc(y) && acc(z) && x == y - z && y >= 0 && z >= 0;
-  
-  refines init() 
-  {
-    this.y := 0; 
-    this.z := 0;
-  }
-
-  refines inc()
-  {    
-    this.y := this.y + 1;
-  }
-
-  refines dec() 
-  {
-    this.z := this.z + 1;
-  }      
-
-  refines magic() returns (c: Cell)
-  {
-    c := new Cell;
-  } 
-}
-
-class Cell {var n: int}
-
-/** TODO: 
-Two-step data refinement doesn't work for the following reason:
-the spec of Counter1 uses the abstract field x which disappears at the concrete method body level.
-I'm not sure what a good solution to this problem...
-*/
-
-class Counter2 refines Counter0 {
-  var a: Cell;
-  var b: Cell;
-  replaces x by acc(a) && acc(b) && acc(a.n) && acc(b.n) && x == a.n - b.n;
-  
-  refines init() 
-  {    
-    this.a := new Cell;
-    this.b := new Cell;
-    this.a.n := 0;
-    this.b.n := 0;
-  }
-
-  refines inc() 
-  {
-    this.a.n := this.a.n + 1;
-  }
-
-  refines dec()
-  {
-    var i := this.b.n + 1;
-    this.b := new Cell;
-    this.b.n := i;
-  }
-
-  refines magic() returns (c: Cell)
-  {
-    c := a;
-  }
-}
-
-class Client {
-  method main() 
-  {
-    var c := new Counter0;
-    call c.init();
-    call c.inc();
-    call c.inc();
-    call c.dec();
-    call d := c.magic();
-    d.n := 100;
-    assert c.x == 1;
-  }
-}
-