diff options
Diffstat (limited to 'Chalice/tests/predicates/LinkedList-various.chalice')
| -rw-r--r-- | Chalice/tests/predicates/LinkedList-various.chalice | 176 |
1 files changed, 176 insertions, 0 deletions
diff --git a/Chalice/tests/predicates/LinkedList-various.chalice b/Chalice/tests/predicates/LinkedList-various.chalice new file mode 100644 index 00000000..a888b647 --- /dev/null +++ b/Chalice/tests/predicates/LinkedList-various.chalice @@ -0,0 +1,176 @@ +class Node
+{
+ var v:int;
+ var n:Node;
+
+ predicate inv
+ { acc(v) && acc(n) && (n!=null ==> n.inv) }
+
+ function len():int
+ requires inv;
+ ensures result>0;
+ {
+ unfolding inv in (n==null) ? 1 : 1+n.len()
+ }
+
+ function get(i:int):int
+ requires inv && 0<=i && i<len();
+ {
+ unfolding inv in (i==0) ? v : n.get(i-1)
+ }
+
+ method addLast(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(old(len()))==x;
+ ensures (forall i:int :: 0<=i && i<old(len()) ==> get(i)==old(get(i)));
+ {
+ unfold inv;
+ if(n==null)
+ {
+ n:=new Node;
+ n.v:=x; n.n:=null;
+ fold n.inv;
+ }
+ else
+ {
+ call n.addLast(x);
+ }
+ fold inv;
+ }
+
+ method append(p:List)
+ requires inv && p!=null && p.inv;
+ ensures inv;
+ ensures len()==old(len()+p.len());
+ ensures (forall i in [0..old(len())] :: get(i)==old(get(i)));
+ ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len())));
+ {
+ unfold inv;
+ if(n==null)
+ {
+ unfold p.inv;
+ n:=p.c;
+ }
+ else
+ {
+ call n.append(p);
+ }
+ fold inv;
+ }
+
+ method remove(i:int)
+ requires inv && i>=0 && i<len()-1;
+ ensures inv;
+ ensures len()==old(len())-1;
+ ensures (forall j in [0..i+1] :: get(j)==old(get(j)));
+ ensures (forall j in [i+1..len()] :: get(j)==old(get(j+1)));
+ {
+ unfold inv;
+ if(i==0)
+ {
+ unfold n.inv;
+ n:=n.n;
+ }
+ else
+ {
+ call n.remove(i-1);
+ }
+ fold inv;
+ }
+}
+
+class List
+{
+ var c:Node;
+
+ predicate inv { acc(c) && (c!=null ==> c.inv) }
+
+ function len():int
+ requires inv;
+ ensures result>=0;
+ {
+ unfolding inv in (c==null) ? 0 : c.len()
+ }
+
+ function get(i:int):int
+ requires inv && 0<=i && i<len();
+ {
+ unfolding inv in c.get(i)
+ }
+
+ method addFirst(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(0)==x;
+ ensures (forall i:int :: 1<=i && i<len() ==> get(i)==old(get(i-1)));
+ {
+ var p:Node;
+
+ unfold inv;
+ p:=new Node; p.v:=x; p.n:=c; c:=p;
+ fold c.inv;
+ assert c.len()==old(len())+1
+ fold inv;
+ }
+
+ method addLast(x:int)
+ requires inv;
+ ensures inv;
+ ensures len()==old(len())+1 && get(old(len()))==x;
+ ensures (forall i:int :: 0<=i && i<old(len()) ==> get(i)==old(get(i)));
+ {
+ unfold inv;
+ if(c==null)
+ {
+ c:=new Node;
+ c.v:=x; c.n:=null;
+ fold c.inv;
+ }
+ else
+ {
+ call c.addLast(x);
+ }
+ fold inv;
+ }
+
+ method append(p:List)
+ requires inv && p!=null && p.inv;
+ ensures inv;
+ ensures len()==old(len()+p.len());
+ ensures (forall i in [0..old(len())] :: get(i)==old(get(i)));
+ ensures (forall i in [old(len())..len()] :: get(i)==old(p.get(i-len())));
+ {
+ unfold inv;
+ if(c==null)
+ {
+ unfold p.inv;
+ c:=p.c;
+ }
+ else
+ {
+ call c.append(p);
+ }
+ fold inv;
+ }
+
+ method remove(i:int)
+ requires inv && i>=0 && i<len();
+ ensures inv;
+ ensures len()==old(len())-1;
+ ensures (forall j in [0..i] :: get(j)==old(get(j)));
+ ensures (forall j in [i..len()] :: get(j)==old(get(j+1)));
+ {
+ unfold inv;
+ if(i==0)
+ {
+ unfold c.inv;
+ c:=c.n;
+ }
+ else
+ {
+ call c.remove(i-1);
+ }
+ fold inv;
+ }
+}
\ No newline at end of file |