1 files changed, 0 insertions, 159 deletions
diff --git a/Chalice/tests/refinements/experiments/List.chalice b/Chalice/tests/refinements/experiments/List.chalice
deleted file mode 100644
index efcec2c8..00000000
--- a/Chalice/tests/refinements/experiments/List.chalice
+++ /dev/null
@@ -1,159 +0,0 @@
-/** 
-Interesting issues:
-  * using functions in refinement to write getters
-  * using functions to write coupling invariant
-  * refining to a recursive implementation
-  * restricting refinement (List1 must have at least one item)
-  * refining a method with an output variable  
-
-Do we shadows the abstract variables in the later concrete programs?
-
-How do we handle generic sequence in List2
-*/
-
-class List0 {
-  var rep: seq<int>;
-
-  method init() 
-    requires acc(this.*);
-    ensures acc(rep);
-  {
-    rep := [0];
-  }
-
-  function length(): int
-    requires acc(rep);
-  {
-    |rep|
-  }
-
-  method get(i: int) returns (v: int)
-    requires acc(rep);
-    requires 0 <= i && i < length();
-    ensures acc(rep);
-  {
-    v := rep[i];
-  }
-
-  method pick() returns (v: int) 
-    requires acc(rep);
-    ensures acc(rep);
-  {
-    var i: int;
-    assume 0 <= i && i < length();
-    v := rep[i];
-  }
-}
-
-class List1 {
-  ghost var rep: seq<int>;
-
-  var data: int;
-  var l: seq<List1>;
-
-  function inv(): bool
-    requires acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l);
-  {
-    /** valid */ |l| >= 0 &&  
-    (forall i in [0..|l|] :: l[i] != null && l[i].l == l[i+1..]) &&
-    /** coupling */ |l| + 1 == |rep| && 
-    (forall i in [0..|l|] :: l[i].data == rep[i+1]) &&
-    data == rep[0]  
-  }
-
-  method init()
-    requires acc(this.*);
-    ensures acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && inv();
-  {
-    rep := [0];
-    data := 0;
-    l := nil<List1>;    
-  }
-
-  function length(): int
-    requires acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && inv();
-  {
-    |l| + 1
-  }
-
-  method checkLength() 
-    requires acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && inv();
-  {
-    assert |l| + 1 == |rep|;
-  }
-
-  method get(i: int) returns (v: int)
-    requires acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && inv();
-    requires 0 <= i && i < length();
-    ensures acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && inv();
-  {
-    if (i == 0) {
-      v := data;
-    } else {
-      v := l[i-1].data;
-    }
-    assert v == rep[i];
-  }
-}
-
-class List2 {
-  // ghost var rep: seq<int>;  
-  ghost var l: seq<List2>;
-
-  var data: int;
-  var next: List2;
-  var size: int;
-
-  function inv(): bool
-    requires acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next);
-  {
-    /** valid */ |l| >= 0 &&  
-    (forall i in [0..|l|] :: l[i] != null && l[i].l == l[i+1..]) &&
-    /** new coupling */ size == |l| + 1 &&
-    (next == null ==> |l| == 0) &&
-    (next != null ==> |l| > 0 && next == l[0] && l[|l|-1].next == null) &&
-    (forall i in [0..|l|] :: l[i].size == size - i - 1) && 
-    (forall i in [0..|l|-1] :: l[i].next == l[i+1]) 
-  }
-
-  method init()
-    requires acc(this.*);
-    ensures acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l)  && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();
-  {
-    data := 0;
-    l := nil<List2>;    
-    next := null;
-    size := 1;
-  }
-
-  function length(): int
-    requires acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();
-  {
-    size
-  }
-
-  method checkLength() 
-    requires acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();
-  {
-    assert size == |l| + 1;
-  }
-
-  method get(i: int) returns (v: int)
-    requires acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();
-    requires 0 <= i && i < length();
-    ensures acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();
-    /** loop invariant: assertion on coupling of abstract and concrete outputs */     
-    ensures i == 0 ==> v == data;
-    ensures i > 0 ==> i-1 < |l| && l[i-1] != null && v == l[i-1].data;  
-  {
-    if (i == 0) {
-      v := data;
-    } else {
-      assert next != null;      
-      assert l == [next] ++ next.l;
-      call w := next.get(i-1);
-      v := w;
-    }
-  }
-}
-