blob: fda9ca7483e5eac243ca9852c33b634cd2748856 (
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
135
|
class Collection<T> {
ghost var footprint:set<object>;
var elements:seq<T>;
function Valid():bool
reads this, footprint;
{
this in footprint
}
method GetCount() returns (c:int)
requires Valid();
ensures 0<=c;
{
c:=|elements|;
}
method Init()
modifies this;
ensures Valid() && fresh(footprint -{this});
{
elements := [];
footprint := {this};
}
method GetItem(i:int ) returns (x:T)
requires Valid();
requires 0<=i && i<|elements|;
ensures elements[i] ==x;
{
x:=elements[i];
}
method Add(x:T )
requires Valid();
modifies footprint;
ensures Valid() && fresh(footprint - old(footprint));
ensures elements == old(elements) + [x];
{
elements:= elements + [x];
}
method GetIterator() returns (iter:Iterator<T>)
requires Valid();
ensures iter != null && iter.Valid();
ensures fresh(iter.footprint) && iter.pos == -1;
ensures iter.c == this;
{
iter:= new Iterator<T>.Init(this);
}
}
class Iterator<T> {
var c:Collection<T>;
var pos:int;
ghost var footprint:set<object>;
function Valid():bool
reads this, footprint;
{
this in footprint && c != null && -1 <= pos && null !in footprint
}
method Init(coll:Collection<T>)
requires coll != null;
modifies this;
ensures Valid() && fresh(footprint - {this}) && pos == -1;
ensures c == coll;
{
c := coll;
pos := -1;
footprint := {this};
}
method MoveNext() returns (b:bool)
requires Valid();
modifies footprint;
ensures fresh(footprint - old(footprint)) && Valid() && pos == old(pos) + 1;
ensures b == HasCurrent() && c == old(c);
{
pos := pos+1;
b := pos < |c.elements|;
}
function HasCurrent():bool //???
requires Valid();
reads this, c;
{
0 <= pos && pos < |c.elements|
}
method GetCurrent() returns (x:T)
requires Valid() && HasCurrent();
ensures c.elements[pos] == x;
{
x := c.elements[pos];
}
}
class Client
{
method Main()
{
var c := new Collection<int>.Init();
c.Add(33);
c.Add(45);
c.Add(78);
var s := [];
var iter := c.GetIterator();
var b := iter.MoveNext();
while (b)
invariant iter.Valid() && b == iter.HasCurrent() && fresh(iter.footprint);
invariant c.Valid() && fresh(c.footprint) && iter.footprint !! c.footprint; //disjoint footprints
invariant 0 <= iter.pos && iter.pos <=|c.elements| && s == c.elements[..iter.pos] ;
invariant iter.c == c;
decreases |c.elements| - iter.pos;
{
var x := iter.GetCurrent();
s := s + [x];
b := iter.MoveNext();
}
assert s == c.elements; //verifies that the iterator returns the correct things
c.Add(100);
}
}
|
