blob: e9280a9a6212aa16bb3a907eb8d8d46364a549e1 (
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
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class SparseArray<T> {
ghost var Contents: seq<T>;
var zero: T;
/*private*/ var a: seq<T>; // should really be an array
/*private*/ var b: seq<int>; // should really be an array
/*private*/ var c: seq<int>; // should really be an array
/*private*/ var n: int;
/*private*/ ghost var d: seq<int>; // would be better as an array
/*private*/ ghost var e: seq<int>; // would be better as an array
function Valid(): bool
reads this;
{
|a| == |Contents| &&
|b| == |Contents| &&
|c| == |Contents| &&
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| ==>
(i in c[..n] <==> 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;
ensures Valid();
ensures |Contents| == N && this.zero == zero;
ensures (forall x :: x in Contents ==> x == zero);
{
var aa : seq<T> := AllocateArray(N); this.a := aa;
var bb : seq<int> := AllocateArray(N); this.b := bb;
bb := AllocateArray(N); this.c := bb;
this.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;
// TODO: why doesn't this work instead of the next line? invariant (forall x :: x in s ==> x == zero);
invariant (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;
}
this.zero := zero;
this.Contents := s;
this.d := id;
this.e := id;
}
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;
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 := b[i := n];
c := 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 := a[i := x];
Contents := Contents[i := x];
}
}
/* The following method is here only to simulate support of arrays in Dafny */
/*private*/ method AllocateArray<G>(n: int) returns (arr: seq<G>)
requires 0 <= n;
ensures |arr| == n;
{
arr := [];
var i := 0;
while (i < n)
invariant i <= n && |arr| == i;
{
var g: G;
arr := arr + [g];
i := i + 1;
}
}
|
