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
|
class LazyInitArray<T> {
ghost var Contents: seq<T>;
var Zero: T;
/*private*/ var a: array<T>;
/*private*/ var b: array<int>;
/*private*/ var c: array<int>;
/*private*/ var n: int;
/*private*/ ghost var d: seq<int>;
/*private*/ ghost var e: seq<int>;
function Valid(): bool
reads this, a, b, c;
{
a != null && b != null && c != null &&
|a| == |Contents| + 1 && // TODO: remove the "+ 1" hack, which currently serves the purpose of distinguishing 'a' from 'b' and 'c'
|b| == |Contents| &&
|c| == |Contents| &&
b != c &&
0 <= n && n <= |c| &&
(forall i :: 0 <= i && i < |Contents| ==>
Contents[i] == (if 0 <= b[i] && b[i] < n && c[b[i]] == i then a[i] else Zero)) &&
(forall i :: 0 <= i && i < |Contents| ==>
((exists j :: 0 <= j && j < n && c[j] == i)
<==>
0 <= b[i] && b[i] < n && c[b[i]] == i)) &&
// The idea behind d and e is the following:
// * d is a permutation of the first |Contents| natural numbers
// * e describes which permutation d is
// * c[..n] == d[..n]
|d| == |Contents| &&
|e| == |Contents| &&
(forall i :: 0 <= i && i < n ==> c[i] == d[i]) &&
(forall i :: 0 <= i && i < |d| ==> 0 <= d[i] && d[i] < |d|) &&
(forall i :: 0 <= i && i < |e| ==> 0 <= e[i] && e[i] < |e|) &&
(forall i :: 0 <= i && i < |e| ==> d[e[i]] == i)
}
method Init(N: int, zero: T)
requires 0 <= N;
modifies this, a, b, c;
ensures Valid();
ensures |Contents| == N && Zero == zero;
ensures (forall x :: x in Contents ==> x == zero);
{
var aa := new T[N+1]; a := aa;
var ii := new int[N]; b := ii;
ii := new int[N]; c := ii;
n := 0;
// initialize ghost variable Contents to a sequence of length N containing only zero's,
// and ghost variables d and e to be the identity sequences of length N
ghost var s := [];
ghost var id := [];
ghost var k := 0;
while (k < N)
invariant k <= N;
invariant |s| == k && (forall i :: 0 <= i && i < |s| ==> s[i] == zero);
invariant |id| == k && (forall i :: 0 <= i && i < k ==> id[i] == i);
{
s := s + [zero];
id := id + [k];
k := k + 1;
}
d := id;
e := id;
Zero := zero;
Contents := s;
}
method Get(i: int) returns (x: T)
requires Valid();
requires 0 <= i && i < |Contents|;
ensures x == Contents[i];
{
if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
x := a[i];
} else {
x := Zero;
}
}
method Set(i: int, x: T)
requires Valid();
requires 0 <= i && i < |Contents|;
modifies this, a, b, c;
ensures Valid();
ensures |Contents| == |old(Contents)| && Contents == Contents[i := x];
ensures Zero == old(Zero);
{
if (0 <= b[i] && b[i] < n && c[b[i]] == i) {
} else {
assert n <= e[i]; // lemma
b[i] := n;
c[n] := i;
ghost var t := d[n];
ghost var k := e[i];
d := d[n := i][k := t];
e := e[i := n][t := k];
n := n + 1;
}
a[i] := x;
Contents := Contents[i := x];
}
}
|
