blob: 01532f96cb153e313391fd2ec64867de84d7fa91 (
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
|
interface Set {
var elems: set[int]
constructor Empty()
ensures elems = {}
constructor SingletonZero()
ensures elems = {0}
constructor Singleton(t: int)
ensures elems = {t}
constructor Sum(p: int, q: int)
ensures elems = {p + q}
constructor Double(p: int, q: int)
requires p != q
ensures elems = {p q}
}
datamodel Set {
var root: SetNode
frame
root
invariant
root = null ==> elems = {}
root != null ==> elems = root.elems
}
interface SetNode {
var elems: set[int]
constructor Init(x: int)
ensures elems = {x}
constructor Double(a: int, b: int)
requires a != b
ensures elems = {a b}
constructor DoubleBase(x: int, y: int)
requires x > y
ensures elems = {x y}
constructor Triple(x: int, y: int, z: int)
requires x != y && y != z && z != x
ensures elems = {x y z}
constructor TripleBase(x: int, y: int, z: int)
requires x < y && y < z
ensures elems = {x y z}
method Find(n: int) returns (ret: bool)
ensures ret = (n in elems)
}
datamodel SetNode {
var data: int
var left: SetNode
var right: SetNode
frame
left * right
invariant
elems = {data} + (left != null ? left.elems : {}) + (right != null ? right.elems : {})
left != null ==> forall e :: e in left.elems ==> e < data
right != null ==> forall e :: e in right.elems ==> e > data
}
|
