-
Notifications
You must be signed in to change notification settings - Fork 0
/
AvlNode.dfy
82 lines (76 loc) · 2.25 KB
/
AvlNode.dfy
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
class AvlNode {
ghost var Contents: set<int>
ghost var Repr: set<AvlNode>
//Height of the subtree
var height: int
var data: int
var left: AvlNode?
var right: AvlNode?
predicate Height_Valid()
reads this, Repr
{
Valid() &&
(left == null && right == null) ==> height == -1 &&
(left != null && right == null) ==> height == left.height + 1 &&
(left == null && right != null) ==> height == right.height + 1 &&
(left != null && right != null) ==> height == max(left.height, right.height) + 1 &&
(right != null) ==> right.Height_Valid() &&
(left != null) ==> left.Height_Valid()
}
predicate Balanced()
reads this, Repr
{
Valid() &&
Height_Valid() &&
(left != null && right == null) ==> left.height + 1 <= 1 &&
(left == null && right != null) ==> right.height + 1 <= 1 &&
(left != null && right != null) ==> (right.height - left.height <= 1 && left.height - right.height <= 1) &&
(right != null) ==> right.Balanced() &&
(left != null) ==> left.Balanced()
}
function method max(a: int, b: int) : int
{
if (a > b) then
a
else
b
}
predicate Valid()
reads this, Repr
{
this in Repr &&
(left != null ==>
left in Repr &&
left.Repr <= Repr && this !in left.Repr &&
left.Valid() &&
(forall y :: y in left.Contents ==> y < data)) &&
(right != null ==>
right in Repr &&
right.Repr <= Repr && this !in right.Repr &&
right.Valid() &&
(forall y :: y in right.Contents ==> data < y)) &&
(left == null && right == null ==>
Contents == {data}) &&
(left != null && right == null ==>
Contents == left.Contents + {data}) &&
(left == null && right != null ==>
Contents == {data} + right.Contents) &&
(left != null && right != null ==>
left.Repr !! right.Repr &&
Contents == left.Contents + {data} + right.Contents)
}
constructor Init(x: int)
ensures Valid() && fresh(Repr - {this})
ensures Height_Valid()
ensures Balanced()
ensures Contents == {x}
ensures Repr == {this};
{
height := 0;
data := x;
left := null;
right := null;
Contents := {x};
Repr := {this};
}
}