From a94dd46ee878bb7883a96072b4f17ac61a836cd8 Mon Sep 17 00:00:00 2001
From: Unknown <Alex@Mingus.ethz.ch>
Date: Tue, 18 Sep 2012 16:38:28 +0200
Subject: 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 :)

---
 Chalice/tests/examples/linkedlist.chalice | 31 ++++++++++++++++++++++++++++++-
 1 file changed, 30 insertions(+), 1 deletion(-)

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)
-- 
cgit v1.2.3