1 files changed, 159 insertions, 0 deletions
diff --git a/Chalice/tests/refinements/experiments/List.chalice b/Chalice/tests/refinements/experiments/List.chalice
new file mode 100644
index 00000000..efcec2c8
--- /dev/null
+++ b/Chalice/tests/refinements/experiments/List.chalice
@@ -0,0 +1,159 @@
+/** 
+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;
+    }
+  }
+}
+