diff options
Diffstat (limited to 'Chalice/tests/examples/linkedlist.chalice')
| -rw-r--r-- | Chalice/tests/examples/linkedlist.chalice | 34 |
1 files changed, 32 insertions, 2 deletions
diff --git a/Chalice/tests/examples/linkedlist.chalice b/Chalice/tests/examples/linkedlist.chalice index acde86ab..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;
@@ -46,14 +68,22 @@ class Node { function at(i: int): int
requires valid && 0<=i && i<size();
{
- unfolding valid in i==0 ? value : next.at(i-1) // no warning anymore... fishy!
+ unfolding valid in i==0 ? value : next.at(i-1)
}
function size(): int
requires valid;
+ ensures result > 0
{
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)
|