diff options
| author |  mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
|---|---|---|
| committer | mikebarnett <unknown> | 2009-07-15 21:03:41 +0000 |
| commit | ce1c2de044c91624370411e23acab13b0381949b (patch) | |
| tree | 592539996fe08050ead5ee210c973801611dde40 /Chalice/examples/iterator2.chalice | |
Initial set of files.
Diffstat (limited to 'Chalice/examples/iterator2.chalice')
| -rw-r--r-- | Chalice/examples/iterator2.chalice | 134 |
1 files changed, 134 insertions, 0 deletions
diff --git a/Chalice/examples/iterator2.chalice b/Chalice/examples/iterator2.chalice new file mode 100644 index 00000000..5b75c1ca --- /dev/null +++ b/Chalice/examples/iterator2.chalice @@ -0,0 +1,134 @@ +/* Iterator pattern in Chalice. */
+
+class List module Collections {
+ var contents: seq<int>;
+
+ method init()
+ requires acc(contents);
+ ensures valid && size()==0;
+ {
+ contents := nil<int>;
+ fold valid;
+ }
+
+ method add(x: int)
+ requires valid;
+ ensures valid && size() == old(size()+1) && get(size()-1) == x; // I don't know why this happens.
+ ensures forall { i in [0:size()-1]; get(i) == old(get(i)) };
+ {
+ unfold valid;
+ contents := contents ++ [x];
+ fold valid;
+ }
+
+ function get(index: int): int
+ requires rd(valid) && 0<=index && index<size();
+ {
+ unfolding rd(valid) in contents[index]
+ }
+
+ function size(): int
+ requires rd(valid);
+ ensures 0<=result;
+ {
+ unfolding rd(valid) in |contents|
+ }
+
+ predicate valid {
+ acc(contents)
+ }
+}
+
+class Iterator module Collections {
+ var list: List;
+ var index: int;
+
+ method init(l: List)
+ requires acc(list) && acc(index);
+ requires l!=null;
+ requires rd(l.valid);
+ ensures valid;
+ ensures getList()==l;
+ {
+ list := l;
+ this.index := 0;
+ fold valid;
+ }
+
+ method next() returns (rt: int)
+ requires valid && hasNext();
+ ensures valid;
+ ensures getList()==old(getList());
+ {
+ unfold valid;
+ rt := list.get(index);
+ index := index + 1;
+ fold valid;
+ }
+
+ method dispose()
+ requires valid;
+ ensures rd(old(getList()).valid);
+ {
+ unfold valid;
+ }
+
+ function hasNext(): bool
+ requires valid;
+ {
+ unfolding valid in index<list.size()
+ }
+
+ function getList(): List
+ requires valid;
+ ensures result!=null;
+ {
+ unfolding valid in list
+ }
+
+ predicate valid
+ {
+ acc(list) && acc(index) && list!=null && rd(list.valid) && 0<=index && index<=list.size()
+ }
+}
+
+class Program module Main {
+ method main(){
+ var tmp: int;
+ //create a new list
+ var list := new List;
+ call list.init();
+ call list.add(5);
+ call list.add(6);
+
+ // create a new iterator
+ var iter1 := new Iterator;
+ call iter1.init(list);
+
+ // create a second iterator
+ var iter2 := new Iterator;
+ call iter2.init(list);
+
+ // iterate over the list
+ while(iter1.hasNext())
+ invariant iter1.valid && iter1.getList()==list;
+ {
+ call tmp := iter1.next();
+ }
+
+ // iterate over the list
+ while(iter2.hasNext())
+ invariant iter2.valid && iter2.getList()==list;
+ {
+ call tmp := iter2.next();
+ }
+
+ // dispose the iterators
+ call iter1.dispose();
+ call iter2.dispose();
+
+ // full access to the list
+ assert list.valid;
+ assert list.size()==2;
+ }
+}
\ No newline at end of file |