blob: 01afdafdbf2544362b15d114ebdc829ef4a0d81d (
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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
class {:autocontracts} ExtensibleArray<T> {
ghost var Contents: seq<T>
var elements: array<T>
var more: ExtensibleArray<array<T>>
var length: int
var M: int // shorthand for: if more == null then 0 else 256 * |more.Contents|
predicate Valid()
{
// shape of data structure
elements != null && elements.Length == 256 &&
(more != null ==>
elements !in more.Repr &&
more.Valid() &&
|more.Contents| != 0 &&
forall j :: 0 <= j < |more.Contents| ==>
more.Contents[j] != null && more.Contents[j].Length == 256 &&
more.Contents[j] in Repr && more.Contents[j] !in more.Repr &&
more.Contents[j] != elements &&
forall k :: 0 <= k < |more.Contents| && k != j ==> more.Contents[j] != more.Contents[k]) &&
// length
M == (if more == null then 0 else 256 * |more.Contents|) &&
0 <= length <= M + 256 &&
(more != null ==> M < length) &&
// Contents
length == |Contents| &&
(forall i :: 0 <= i < M ==> Contents[i] == more.Contents[i / 256][i % 256]) &&
(forall i :: M <= i < length ==> Contents[i] == elements[i - M])
}
constructor Init()
ensures Contents == []
{
elements := new T[256];
more := null;
length := 0;
M := 0;
Contents := [];
}
method Get(i: int) returns (t: T)
requires 0 <= i < |Contents|
ensures t == Contents[i]
decreases Repr
{
if M <= i {
t := elements[i - M];
} else {
var arr := more.Get(i / 256);
t := arr[i % 256];
}
}
method Set(i: int, t: T)
requires 0 <= i < |Contents|
ensures Contents == old(Contents)[i := t]
{
if M <= i {
elements[i - M] := t;
} else {
var arr := more.Get(i / 256);
arr[i % 256] := t;
}
Contents := Contents[i := t];
}
method Append(t: T)
ensures Contents == old(Contents) + [t]
decreases |Contents|
{
if length == 0 || length % 256 != 0 {
// there is room in "elements"
elements[length - M] := t;
} else {
if more == null {
more := new ExtensibleArray<array<T>>.Init();
Repr := Repr + {more} + more.Repr;
}
// "elements" is full, so move it into "more" and allocate a new array
more.Append(elements);
Repr := Repr + more.Repr;
M := M + 256;
elements := new T[256];
Repr := Repr + {elements};
elements[0] := t;
}
length := length + 1;
Contents := Contents + [t];
}
}
method Main() {
var a := new ExtensibleArray<int>.Init();
var n := 0;
while n < 256*256+600
invariant a.Valid() && fresh(a.Repr);
invariant |a.Contents| == n;
{
a.Append(n);
n := n + 1;
}
var k := a.Get(570); print k, "\n";
k := a.Get(0); print k, "\n";
k := a.Get(1000); print k, "\n";
a.Set(1000, 23);
k := a.Get(0); print k, "\n";
k := a.Get(1000); print k, "\n";
k := a.Get(66000); print k, "\n";
}
|
