diff options
Diffstat (limited to 'tests/examplefiles/test.bpl')
-rw-r--r-- | tests/examplefiles/test.bpl | 140 |
1 files changed, 0 insertions, 140 deletions
diff --git a/tests/examplefiles/test.bpl b/tests/examplefiles/test.bpl deleted file mode 100644 index add25e1a..00000000 --- a/tests/examplefiles/test.bpl +++ /dev/null @@ -1,140 +0,0 @@ -/* - * 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); - } -} |