mirror of
https://github.com/kmc7468/cs220.git
synced 2025-12-15 06:28:46 +00:00
59 lines
1.4 KiB
Plaintext
59 lines
1.4 KiB
Plaintext
(* Two Way Sort
|
|
|
|
The following program sorts an array of Boolean values, with False<True.
|
|
|
|
Questions:
|
|
|
|
1. Prove safety i.e. the absence of array access out of bounds.
|
|
|
|
2. Prove termination.
|
|
|
|
3. Prove that array a is sorted after execution of function two_way_sort
|
|
(using the predicate sorted that is provided).
|
|
|
|
4. Show that after execution the array contents is a permutation of its
|
|
initial contents. Use the library predicate "permut_all" to do so
|
|
(the corresponding module ArrayPermut is already imported).
|
|
|
|
You can refer to the contents of array a at the beginning of the
|
|
function with notation "a at Init".
|
|
*)
|
|
|
|
module TwoWaySort
|
|
|
|
use int.Int
|
|
use bool.Bool
|
|
use ref.Refint
|
|
use array.Array
|
|
use array.ArraySwap
|
|
use array.ArrayPermut
|
|
|
|
predicate (<<) (x y: bool) = x = False \/ y = True
|
|
|
|
predicate sorted (a: array bool) =
|
|
forall i1 i2: int. 0 <= i1 <= i2 < a.length -> a[i1] << a[i2]
|
|
|
|
let two_way_sort (a: array bool) : unit
|
|
ensures { true }
|
|
=
|
|
label Init in
|
|
let ref i = 0 in
|
|
let ref j = length a - 1 in
|
|
while i < j do
|
|
invariant { forall i1: int. 0 <= i1 < i -> a[i1] = False }
|
|
invariant { forall i2: int. j < i2 < length a -> a[i2] = True }
|
|
invariant { 0 <= i /\ j < length a }
|
|
variant { j - i }
|
|
if not a[i] then
|
|
incr i
|
|
else if a[j] then
|
|
decr j
|
|
else begin
|
|
swap a i j;
|
|
incr i;
|
|
decr j
|
|
end
|
|
done
|
|
|
|
end
|