blob: 34065b7d9f0da7c93c41b222350009cbc445f6ea (
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
|
var A: [int]int;
const N: int;
procedure Partition(l: int, r: int) returns (result: int)
requires 0 <= l && l+2 <= r && r <= N;
modifies A;
ensures l <= result && result < r;
ensures (forall k: int, j: int :: l <= k && k < result && result <= j && j < r ==> A[k] <= A[j]);
ensures (forall k: int :: l <= k && k < result ==> A[k] <= old(A)[l]);
ensures (forall k: int :: result <= k && k < r ==> old(A)[l] <= A[k]);
{
var pv: int;
var i: int;
var j: int;
var tmp: int;
start:
pv := A[l];
i := l;
j := r-1;
// swap A[l] and A[j]
tmp := A[l];
A[l] := A[j];
A[j] := tmp;
goto LoopHead;
LoopHead:
assert (forall k: int :: l <= k && k < i ==> A[k] <= pv);
assert (forall k: int :: j <= k && k < r ==> pv <= A[k]);
assert l <= i && i <= j && j < r;
goto A, B, C, exit;
A:
assume i < j;
assume A[i] <= pv;
i := i + 1;
goto LoopHead;
B:
assume i < j;
assume pv <= A[j-1];
j := j - 1;
goto LoopHead;
C:
assume i < j;
assume A[j-1] < pv && pv < A[i];
// swap A[j-1] and A[i]
tmp := A[i];
A[i] := A[j-1];
A[j-1] := tmp;
assert A[i] < pv && pv < A[j-1];
i := i + 1;
j := j - 1;
goto LoopHead;
exit:
assume i == j;
result := i;
return;
}
|
