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
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
class List module Collections {
var contents: seq<int>;
method init()
requires acc(contents);
ensures valid && size(100)==0;
{
contents := nil<int>;
fold valid;
}
method add(x: int)
requires valid;
ensures valid && size(100) == old(size(100)+1) && get(size(100)-1, 100) == x;
ensures forall i in [0..size(100)-1] :: get(i, 100) == old(get(i, 100));
{
unfold valid;
contents := contents ++ [x];
fold valid;
}
function get(index: int, f: int): int
requires 0<f && f<=100 && acc(valid, f) && (0<=index && index<size(f));
ensures forall i in [1..f] :: get(index, f) == get(index, i);
{
unfolding acc(valid, f) in contents[index]
}
function size(f: int): int
requires 0<f && f<=100 && acc(valid, f);
ensures 0<=result;
ensures forall i in [1..f] :: size(f) == size(i);
{
unfolding acc(valid, f) in |contents|
}
predicate valid {
acc(contents)
}
}
class Iterator module Collections {
var list: List;
var index: int;
var frac: int;
method init(l: List, f: int)
requires 0<f && f<=100;
requires acc(list) && acc(index) && acc(frac);
requires l!=null;
requires acc(l.valid, f);
ensures valid;
ensures getList()==l;
ensures getFraction()==f;
{
list := l;
this.index := 0;
frac := f;
fold valid;
}
method next() returns (rt: int)
requires valid && hasNext();
ensures valid;
ensures getList()==old(getList());
ensures getFraction()==old(getFraction());
{
unfold valid;
rt := list.get(index, frac);
index := index + 1;
fold valid;
}
method dispose()
requires valid;
ensures acc(old(getList()).valid, old(getFraction()));
{
unfold valid;
}
function hasNext(): bool
requires valid;
{
unfolding valid in index<list.size(frac)
}
function getFraction(): int
requires valid;
ensures 0<result && result<=100;
{
unfolding valid in frac
}
function getList(): List
requires valid;
ensures getList()!=null;
{
unfolding valid in list
}
predicate valid
{
acc(list) && acc(index) && acc(frac) && 0<frac && frac<=100 && list!=null && acc(list.valid, frac) && 0<=index && index<=list.size(frac)
}
}
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;
assert list!=null; // needed here: triggering problem?
assert list.size(100)==2;
assert list.size(50)==2;
call iter1.init(list, 10);
// create a second iterator
var iter2 := new Iterator;
assert list!=null; // needed here: triggering problem?
call iter2.init(list, 10);
// iterate over the list
while(iter1.hasNext())
invariant iter1.valid && iter1.getList()==list && iter1.getFraction()==10;
{
call tmp := iter1.next();
}
// iterate over the list
while(iter2.hasNext())
invariant iter2.valid && iter2.getList()==list && iter2.getFraction()==10;
{
call tmp := iter2.next();
}
// dispose the iterators
call iter1.dispose();
call iter2.dispose();
// full access to the list
assert list.valid;
assert list.size(50)==2;
}
}
|
