summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Unknown <Alex@Mingus.ethz.ch>2012-09-18 16:38:28 +0200
committerGravatar Unknown <Alex@Mingus.ethz.ch>2012-09-18 16:38:28 +0200
commita94dd46ee878bb7883a96072b4f17ac61a836cd8 (patch)
tree8dd512387b9ddb31f2d22c1f6af2cb3913ed0ac5
parent4ad9ff8d765055fa0885a519b543b4df54a11340 (diff)
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 :)
-rw-r--r--Chalice/tests/examples/linkedlist.chalice31
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)