blob: 5b75c1ca1cb912c3f6d0a8d7e653d34480bfb252 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
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;
}
}
|
