Chalice: Updated linkedlist.chalice to include quantified specification, but now the test does not pass.. this is a problem with triggering the framing axiom, if the way the function is mentioned in a state is under a quantifier... but it's about to be fixed :)

1 files changed, 30 insertions, 1 deletions

diff --git a/Chalice/tests/examples/linkedlist.chalice b/Chalice/tests/examples/linkedlist.chalice
index 410bb091..a9859aaa 100644
--- a/Chalice/tests/examples/linkedlist.chalice
+++ b/Chalice/tests/examples/linkedlist.chalice
@@ -6,7 +6,7 @@ class Node {
 

   method init(v: int)

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

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

+    ensures valid && size() == 1 && (forall y:int :: contains(y) <==> y==v);

   {

     next := null;

     value := v;

@@ -17,6 +17,7 @@ class Node {
     requires valid;

     ensures valid;

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

+    ensures (forall y:int :: contains(y)==(old(contains(y)) || x==y));

   {

     unfold this.valid;

     if(next==null) {

@@ -24,11 +25,32 @@ class Node {
       n := new Node;

       call n.init(x);

       next := n;

+      // unfold next.valid; fold next.valid; // makes it work

     } else {

+

       call next.add(x);

     }

     fold this.valid;

   }

+  

+    method addother(i:int)

+      requires valid

+      ensures valid && (forall x:int :: contains(x)==(old(contains(x)) || x==i))

+    {

+      unfold valid

+      if(next!=null)

+      { 

+        call next.addother(i)

+      }

+      else

+      {  

+        next:=new Node

+        next.value:=i

+        next.next:=null

+        fold next.valid

+      }

+      fold valid

+  }

 

   method addFirst(x: int) returns (rt: Node)

     requires valid;

@@ -55,6 +77,13 @@ class Node {
   {

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

   }

+  

+  function contains(i:int):bool

+    requires valid

+  {

+    unfolding valid in i==value || (next!=null && next.contains(i))

+  }

+

 

   predicate valid {

     acc(next) && acc(value) && (next!=null ==> next.valid)