Chalice: testing refinement of a linked list

2 files changed, 232 insertions, 73 deletions

diff --git a/Chalice/examples/refinement/List.chalice b/Chalice/examples/refinement/List.chalice
index af334093..c3d8175c 100644
--- a/Chalice/examples/refinement/List.chalice
+++ b/Chalice/examples/refinement/List.chalice
@@ -1,109 +1,159 @@
-/* Recursive implementation and specification of a linked list. */

+/** 

+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  

 

-class Node {

-  var next: Node;

-  var value: int;

+Do we shadows the abstract variables in the later concrete programs?

 

-  method init(v: int)

-    requires acc(next) && acc(value);

-    ensures valid && size() == 1;

-  {

-    next := null;

-    value := v;

-    fold this.valid;

-  }

+How do we handle generic sequence in List2

+*/

 

-  method append(x: int) 

-    requires valid;

-    ensures valid;

-    ensures size() == old(size())+1;

-  {

-    unfold this.valid;

-    if(next==null) {

-      var n : Node;

-      n := new Node;

-      call n.init(x);

-      next := n;

-    } else {

-      call next.append(x);

-    }

-    fold this.valid;

-  }

+class List0 {

+  var rep: seq<int>;

 

-  method prepend(x: int) returns (rt: Node)

-    requires valid;

-    ensures rt!=null && rt.valid;

-    ensures rt.size() == old(size()) + 1;

+  method init() 

+    requires acc(this.*);

+    ensures acc(rep);

   {

-    var n: Node;

-    n := new Node;

-    n.value := x;

-    n.next := this; 

-    fold n.valid;

-    rt := n;

+    rep := [0];

   }

 

-  function at(i: int): int

-    requires valid && 0<=i && i<size();

+  function length(): int

+    requires acc(rep);

   {

-    unfolding valid in i==0 ? value : next.at(i-1)  

+    |rep|

   }

 

-  function size(): int

-    requires valid;

+  method get(i: int) returns (v: int)

+    requires acc(rep);

+    requires 0 <= i && i < length();

+    ensures acc(rep);

   {

-    unfolding this.valid in (next!=null ? 1 + next.size() : 1)

+    v := rep[i];

   }

 

-  predicate valid {

-    acc(next) && acc(value) && 

-    (next!=null ==> next.valid)  

+  method pick() returns (v: int) 

+    requires acc(rep);

+    ensures acc(rep);

+  {

+    var i: int;

+    assume 0 <= i && i < length();

+    v := rep[i];

   }

 }

 

-// abstract sequence of integers

-class LinkedList {

+class List1 {

   ghost var rep: seq<int>;

 

-  var first: Node;

+  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 valid;

-  {    

-    first := null;   

-    assert coupling(rep, first); 

-    fold valid;

+    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 append(x: int)

-    requires valid;

-    ensures valid;

+  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();

   {

-    unfold valid;

-    rep := rep ++ [x];

-    fold valid;

+    if (i == 0) {

+      v := data;

+    } else {

+      v := l[i-1].data;

+    }

+    assert v == rep[i];

   }

+}

 

-  method prepend(x: int)

-    requires valid;

-    ensures valid;

+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(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next);

   {

-    unfold valid;

-    rep := [x] ++ rep;

-    fold valid;

+    /** 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] &&

+    /** 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])    

   }

 

-  predicate valid {

-    acc(rep) && acc(first) && (first != null ==> first.valid)

+  method init()

+    requires acc(this.*);

+    ensures acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l)  && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();

+  {

+    rep := [0];

+    data := 0;

+    l := nil<List2>;    

+    next := null;

+    size := 1;

   }

 

-  function coupling(a: seq<int>, c: Node) : bool

-    requires c != null ==> c.valid;

+  function length(): int

+    requires acc(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();

   {

-    c == null ? a == nil<int> : 

-      (|a| > 0 && a[0] == c.value && coupling(a[1..], c.next))

+    size

   }

 

+  method checkLength() 

+    requires acc(rep) && 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(rep) && 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(rep) && acc(l) && acc(data) && acc(l[*].data) && acc(l[*].l) && acc(size) && acc(next) && acc(l[*].size) && acc(l[*].next) && inv();

+  {

+    if (i == 0) {

+      v := data;

+    } else {

+      call w := next.get(i-1);

+      v := w;

+      assert v == l[i-1].data;

+    }

+  }

 }

+

diff --git a/Chalice/examples/refinement/ListPredicate.chalice b/Chalice/examples/refinement/ListPredicate.chalice
new file mode 100644
index 00000000..af334093
--- /dev/null
+++ b/Chalice/examples/refinement/ListPredicate.chalice
@@ -0,0 +1,109 @@
+/* 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;

+  {

+    next := null;

+    value := v;

+    fold this.valid;

+  }

+

+  method append(x: int) 

+    requires valid;

+    ensures valid;

+    ensures size() == old(size())+1;

+  {

+    unfold this.valid;

+    if(next==null) {

+      var n : Node;

+      n := new Node;

+      call n.init(x);

+      next := n;

+    } else {

+      call next.append(x);

+    }

+    fold this.valid;

+  }

+

+  method prepend(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;

+  {

+    unfolding this.valid in (next!=null ? 1 + next.size() : 1)

+  }

+

+  predicate valid {

+    acc(next) && acc(value) && 

+    (next!=null ==> next.valid)  

+  }

+}

+

+// abstract sequence of integers

+class LinkedList {

+  ghost var rep: seq<int>;

+

+  var first: Node;

+

+  method init()

+    requires acc(this.*);

+    ensures valid;

+  {    

+    first := null;   

+    assert coupling(rep, first); 

+    fold valid;

+  }

+

+  method append(x: int)

+    requires valid;

+    ensures valid;

+  {

+    unfold valid;

+    rep := rep ++ [x];

+    fold valid;

+  }

+

+  method prepend(x: int)

+    requires valid;

+    ensures valid;

+  {

+    unfold valid;

+    rep := [x] ++ rep;

+    fold valid;

+  }

+

+  predicate valid {

+    acc(rep) && acc(first) && (first != null ==> first.valid)

+  }

+

+  function coupling(a: seq<int>, c: Node) : bool

+    requires c != null ==> c.valid;

+  {

+    c == null ? a == nil<int> : 

+      (|a| > 0 && a[0] == c.value && coupling(a[1..], c.next))

+  }

+

+

+}