1/*
2 * Test Boogie rendering
3*/
4
5const N: int;
6axiom 0 <= N;
7
8procedure foo() {
9    break;
10}
11// array to sort as global array, because partition & quicksort have to
12var a: [int] int;
13var original: [int] int;
14var perm: [int] int;
15
16// Is array a of length N sorted?
17function is_sorted(a: [int] int, l: int, r: int): bool
18{
19    (forall j, k: int :: l <= j && j < k && k <= r ==> a[j] <= a[k])
20}
21
22// is range a[l:r] unchanged?
23function is_unchanged(a: [int] int, b: [int] int, l: int, r: int): bool {
24    (forall i: int :: l <= i && i <= r ==> a[i] == b[i])
25}
26
27function is_permutation(a: [int] int, original: [int] int, perm: [int] int, N: int): bool
28{
29    (forall k: int :: 0 <= k && k < N ==> 0 <= perm[k] && perm[k] < N) &&
30    (forall k, j: int :: 0 <= k && k < j && j < N ==> perm[k] != perm[j]) &&
31    (forall k: int :: 0 <= k && k < N ==> a[k] == original[perm[k]])
32}
33
34function count(a: [int] int, x: int, N: int) returns (int)
35{ if N == 0 then 0 else if a[N-1] == x then count(a, x, N - 1) + 1 else count(a, x, N-1) }
36
37
38/*
39function count(a: [int] int, x: int, N: int) returns (int)
40{ if N == 0 then 0 else if a[N-1] == x then count(a, x, N - 1) + 1 else count(a, x, N-1) }
41
42function is_permutation(a: [int] int, b: [int] int, l: int, r: int): bool {
43  (forall i: int :: l <= i && i <= r ==> count(a, a[i], r+1) == count(b, a[i], r+1))
44}
45*/
46
47procedure partition(l: int, r: int, N: int) returns (p: int)
48    modifies a, perm;
49    requires N > 0;
50    requires l >= 0 && l < r && r < N;
51    requires ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
52    requires ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
53
54    /* a is a permutation of the original array original */
55    requires is_permutation(a, original, perm, N);
56
57    ensures (forall k: int :: (k >= l &&  k <= p ) ==> a[k] <= a[p]);
58    ensures (forall k: int :: (k > p &&  k <= r ) ==> a[k] > a[p]);
59    ensures p >= l && p <= r;
60    ensures is_unchanged(a, old(a), 0, l-1);
61    ensures is_unchanged(a, old(a), r+1, N);
62    ensures ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
63    ensures ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
64
65    /* a is a permutation of the original array original */
66    ensures is_permutation(a, original, perm, N);
67{
68    var i: int;
69    var sv: int;
70    var pivot: int;
71    var tmp: int;
72
73    i := l;
74    sv := l;
75    pivot := a[r];
76
77    while (i < r)
78        invariant i <= r && i >= l;
79        invariant sv <= i && sv >= l;
80        invariant pivot == a[r];
81        invariant (forall k: int :: (k >= l &&  k < sv) ==> a[k] <= old(a[r]));
82        invariant (forall k: int :: (k >= sv &&  k < i) ==> a[k] > old(a[r]));
83
84        /* a is a permutation of the original array original */
85        invariant is_permutation(a, original, perm, N);
86
87        invariant is_unchanged(a, old(a), 0, l-1);
88        invariant is_unchanged(a, old(a), r+1, N);
89        invariant ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
90        invariant ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
91    {
92        if ( a[i] <= pivot) {
93            tmp := a[i]; a[i] := a[sv]; a[sv] := tmp;
94            tmp := perm[i];  perm[i] := perm[sv];  perm[sv] := tmp;
95            sv := sv +1;
96        }
97        i := i + 1;
98    }
99
100    //swap
101    tmp := a[i]; a[i] := a[sv]; a[sv] := tmp;
102    tmp := perm[i];  perm[i] := perm[sv];  perm[sv] := tmp;
103
104    p := sv;
105}
106
107
108procedure quicksort(l: int, r: int, N: int)
109    modifies a, perm;
110
111    requires N > 0;
112    requires l >= 0 && l < r && r < N;
113    requires ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
114    requires ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
115
116    /* a is a permutation of the original array original */
117    requires is_permutation(a, original, perm, N);
118
119    ensures ((r+1) < N) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] <= a[r+1]);
120    ensures ((l-1) >= 0) ==> (forall k: int :: (k >= l && k <= r) ==> a[k] > a[l-1]);
121
122    ensures is_unchanged(a, old(a), 0, l-1);
123    ensures is_unchanged(a, old(a), r+1, N);
124    ensures is_sorted(a, l, r);
125
126    /* a is a permutation of the original array original */
127    ensures is_permutation(a, original, perm, N);
128{
129    var p: int;
130
131    call p := partition(l, r, N);
132
133    if ((p-1) > l) {
134        call quicksort(l, p-1, N);
135    }
136
137    if ((p+1) < r) {
138        call quicksort(p+1, r, N);
139    }
140}
141