Chalice: try using output coupling assertion as loop invariant

1 files changed, 11 insertions, 13 deletions

diff --git a/Chalice/examples/refinement/List.chalice b/Chalice/examples/refinement/List.chalice
index c3d8175c..2919d35c 100644
--- a/Chalice/examples/refinement/List.chalice
+++ b/Chalice/examples/refinement/List.chalice
@@ -97,7 +97,7 @@ class List1 {
 }

 

 class List2 {

-  ghost var rep: seq<int>;

+  // ghost var rep: seq<int>;  

   ghost var l: seq<List2>;

 

   var data: int;

@@ -105,14 +105,11 @@ class 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);

+    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..]) &&

-    /** coupling */ |l| + 1 == |rep| && 

-    (forall i in [0..|l|] :: l[i].data == rep[i+1]) &&

-    data == rep[0] &&

-    /** coupling */ size == |l| + 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) && 

@@ -121,9 +118,8 @@ class List2 {
 

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

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

@@ -131,28 +127,30 @@ class List2 {
   }

 

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

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

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

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

+    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 {

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

       v := w;

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

     }

   }

 }