diff options
Diffstat (limited to 'Chalice/tests/predicates/LinkedList-various.chalice')
| -rw-r--r-- | Chalice/tests/predicates/LinkedList-various.chalice | 176 |
1 files changed, 0 insertions, 176 deletions
diff --git a/Chalice/tests/predicates/LinkedList-various.chalice b/Chalice/tests/predicates/LinkedList-various.chalice deleted file mode 100644 index a888b647..00000000 --- a/Chalice/tests/predicates/LinkedList-various.chalice +++ /dev/null @@ -1,176 +0,0 @@ -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 |