blob: 76e4b1d6190afafc524b908d3893770034dc9f34 (
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
|
class PriorityQueue {
var N: int; // capacity
var n: int; // current size
ghost var Repr: set<object>; // set of objects that make up the representation of a PriorityQueue
var a: array<int>; // private implementation of PriorityQueu
function Valid(): bool
reads this, Repr;
{
MostlyValid() &&
(forall j :: 2 <= j && j <= n ==> a[j/2] <= a[j])
}
function MostlyValid(): bool
reads this, Repr;
{
this in Repr && a in Repr &&
a != null && a.Length == N+1 &&
0 <= n && n <= N
}
method Init(capacity: int)
requires 0 <= capacity;
modifies this;
ensures Valid() && fresh(Repr - {this});
ensures N == capacity;
{
N := capacity;
var arr := new int[N+1];
a := arr;
n := 0;
Repr := {this};
Repr := Repr + {a};
}
method Insert(x: int)
requires Valid() && n < N;
modifies this, a;
ensures Valid() && fresh(Repr - old(Repr));
ensures n == old(n) + 1 && N == old(N);
{
n := n + 1;
a[n] := x;
call SiftUp(n);
}
method SiftUp(k: int)
requires 1 <= k && k <= n;
requires MostlyValid();
requires (forall j :: 2 <= j && j <= n && j != k ==> a[j/2] <= a[j]);
requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j != k ==> a[j/2/2] <= a[j]);
modifies a;
ensures Valid();
{
var i := k;
assert MostlyValid();
while (1 < i)
invariant i <= k && MostlyValid();
invariant (forall j :: 2 <= j && j <= n && j != i ==> a[j/2] <= a[j]);
invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j != i ==> a[j/2/2] <= a[j]);
{
if (a[i/2] <= a[i]) {
return;
}
var tmp := a[i]; a[i] := a[i/2]; a[i/2] := tmp;
i := i / 2;
}
}
method RemoveMin() returns (x: int)
requires Valid() && 1 <= n;
modifies this, a;
ensures Valid() && fresh(Repr - old(Repr));
ensures n == old(n) - 1;
{
x := a[1];
a[1] := a[n];
n := n - 1;
call SiftDown(1);
}
method SiftDown(k: int)
requires 1 <= k;
requires MostlyValid();
requires (forall j :: 2 <= j && j <= n && j/2 != k ==> a[j/2] <= a[j]);
requires (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != k ==> a[j/2/2] <= a[j]);
modifies a;
ensures Valid();
{
var i := k;
while (2*i <= n) // while i is not a leaf
invariant 1 <= i && MostlyValid();
invariant (forall j :: 2 <= j && j <= n && j/2 != i ==> a[j/2] <= a[j]);
invariant (forall j :: 2 <= j && j <= n && 1 <= j/2/2 && j/2/2 != i ==> a[j/2/2] <= a[j]);
{
var smallestChild;
if (2*i + 1 <= n && a[2*i + 1] < a[2*i]) {
smallestChild := 2*i + 1;
} else {
smallestChild := 2*i;
}
if (a[i] <= a[smallestChild]) {
return;
}
var tmp := a[i]; a[i] := a[smallestChild]; a[smallestChild] := tmp;
i := smallestChild;
assert 1 <= i/2/2 ==> a[i/2/2] <= a[i];
}
}
}
|
