From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/textbook/DutchFlag.bpl | 142 ++++++++++++++++++++++---------------------- 1 file changed, 71 insertions(+), 71 deletions(-) (limited to 'Test/textbook/DutchFlag.bpl') diff --git a/Test/textbook/DutchFlag.bpl b/Test/textbook/DutchFlag.bpl index 8bac6aec..f5ee73bb 100644 --- a/Test/textbook/DutchFlag.bpl +++ b/Test/textbook/DutchFlag.bpl @@ -1,71 +1,71 @@ -// RUN: %boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// The partition step of Quick Sort picks a 'pivot' element from a specified subsection -// of a given integer array. It then partially sorts the elements of the array so that -// elements smaller than the pivot end up to the left of the pivot and elements larger -// than the pivot end up to the right of the pivot. Finally, the index of the pivot is -// returned. -// The procedure below always picks the first element of the subregion as the pivot. -// The specification of the procedure talks about the ordering of the elements, but -// does not say anything about keeping the multiset of elements the same. - -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, i, j, tmp: int; - - 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; - - // The following loop iterates while 'i < j'. In each iteration, - // one of the three alternatives (A, B, or C) is chosen in such - // a way that the assume statements will evaluate to true. - LoopHead: - // The following the assert statements give the loop invariant - 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; -} +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// The partition step of Quick Sort picks a 'pivot' element from a specified subsection +// of a given integer array. It then partially sorts the elements of the array so that +// elements smaller than the pivot end up to the left of the pivot and elements larger +// than the pivot end up to the right of the pivot. Finally, the index of the pivot is +// returned. +// The procedure below always picks the first element of the subregion as the pivot. +// The specification of the procedure talks about the ordering of the elements, but +// does not say anything about keeping the multiset of elements the same. + +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, i, j, tmp: int; + + 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; + + // The following loop iterates while 'i < j'. In each iteration, + // one of the three alternatives (A, B, or C) is chosen in such + // a way that the assume statements will evaluate to true. + LoopHead: + // The following the assert statements give the loop invariant + 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; +} -- cgit v1.2.3