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
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
/*
* Test Boogie rendering
*/
const N: int;
axiom 0 <= N;
procedure foo() {
break;
}
// array to sort as global array, because partition & quicksort have to
var a: [int] int;
var original: [int] int;
var perm: [int] int;
// Is array a of length N sorted?
function is_sorted(a: [int] int, l: int, r: int): bool
{
(forall j, k: int :: l <= j && j < k && k <= r ==> a[j] <= a[k])
}
// is range a[l:r] unchanged?
function is_unchanged(a: [int] int, b: [int] int, l: int, r: int): bool {
(forall i: int :: l <= i && i <= r ==> a[i] == b[i])
}
function is_permutation(a: [int] int, original: [int] int, perm: [int] int, N: int): bool
{
(forall k: int :: 0 <= k && k < N ==> 0 <= perm[k] && perm[k] < N) &&
(forall k, j: int :: 0 <= k && k < j && j < N ==> perm[k] != perm[j]) &&
(forall k: int :: 0 <= k && k < N ==> a[k] == original[perm[k]])
}
function count(a: [int] int, x: int, N: int) returns (int)
{ if N == 0 then 0 else if a[N-1] == x then count(a, x, N - 1) + 1 else count(a, x, N-1) }
/*
function count(a: [int] int, x: int, N: int) returns (int)
{ if N == 0 then 0 else if a[N-1] == x then count(a, x, N - 1) + 1 else count(a, x, N-1) }
function is_permutation(a: [int] int, b: [int] int, l: int, r: int): bool {
(forall i: int :: l <= i && i <= r ==> count(a, a[i], r+1) == count(b, a[i], r+1))
}
*/
procedure partition(l: int, r: int, N: int) returns (p: int)
modifies a, perm;
requires N > 0;
requires l >= 0 && l < r && r < N;
requires ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
requires ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
/* a is a permutation of the original array original */
requires is_permutation(a, original, perm, N);
ensures (forall k: int :: (k >= l && k <= p ) ==> a[k] <= a[p]);
ensures (forall k: int :: (k > p && k <= r ) ==> a[k] > a[p]);
ensures p >= l && p <= r;
ensures is_unchanged(a, old(a), 0, l-1);
ensures is_unchanged(a, old(a), r+1, N);
ensures ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
ensures ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
/* a is a permutation of the original array original */
ensures is_permutation(a, original, perm, N);
{
var i: int;
var sv: int;
var pivot: int;
var tmp: int;
i := l;
sv := l;
pivot := a[r];
while (i < r)
invariant i <= r && i >= l;
invariant sv <= i && sv >= l;
invariant pivot == a[r];
invariant (forall k: int :: (k >= l && k < sv) ==> a[k] <= old(a[r]));
invariant (forall k: int :: (k >= sv && k < i) ==> a[k] > old(a[r]));
/* a is a permutation of the original array original */
invariant is_permutation(a, original, perm, N);
invariant is_unchanged(a, old(a), 0, l-1);
invariant is_unchanged(a, old(a), r+1, N);
invariant ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
invariant ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
{
if ( a[i] <= pivot) {
tmp := a[i]; a[i] := a[sv]; a[sv] := tmp;
tmp := perm[i]; perm[i] := perm[sv]; perm[sv] := tmp;
sv := sv +1;
}
i := i + 1;
}
//swap
tmp := a[i]; a[i] := a[sv]; a[sv] := tmp;
tmp := perm[i]; perm[i] := perm[sv]; perm[sv] := tmp;
p := sv;
}
procedure quicksort(l: int, r: int, N: int)
modifies a, perm;
requires N > 0;
requires l >= 0 && l < r && r < N;
requires ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
requires ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
/* a is a permutation of the original array original */
requires is_permutation(a, original, perm, N);
ensures ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
ensures ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
ensures is_unchanged(a, old(a), 0, l-1);
ensures is_unchanged(a, old(a), r+1, N);
ensures is_sorted(a, l, r);
/* a is a permutation of the original array original */
ensures is_permutation(a, original, perm, N);
{
var p: int;
call p := partition(l, r, N);
if ((p-1) > l) {
call quicksort(l, p-1, N);
}
if ((p+1) < r) {
call quicksort(p+1, r, N);
}
}
|
