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