blob: 7ef36ce27935a0055cb6b10ad08b68d42ab14f5a (
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
|
class ExtensibleArray[T] {
var Contents: seq[T]
constructor Init()
Contents := []
method Get(i) returns (t)
requires 0 <= i && i < |Contents|
t := Contents[i]
method Set(i, t)
requires 0 <= i && i < |Contents|
Contents := Contents[i := t]
method Append(t)
Contents := Contents + [t]
}
model ExtensibleArray[T] {
var elements: array[T]
var more: ExtensibleArray[array[T]]
var length: int
var M: int
frame
elements * more * more.Contents[*]
invariant
elements != null
elements.Length = 256
more = null ==> M = 0
more != null ==> |more.Contents| != 0 && M = 256 * |more.Contents|
0 <= length && length <= M + 256
more != null ==> M < length
length = |Contents|
more != null ==> forall i :: 0 <= i && i < |more.Contents| ==> more.Contents[i] != null && more.Contents[i].Length = 256
more != null ==> forall i :: 0 <= i && i < M ==> Contents[i] = more.Contents[i div 256][i mod 256]
forall i :: M <= i && i < length ==> Contents[i] = elements[i - M]
}
|
