28 lines
741 B
Text
28 lines
741 B
Text
|
module SelectionSort
|
||
|
|
use int.Int
|
||
|
|
use array.Array
|
||
|
|
use array.IntArraySorted
|
||
|
|
use array.ArraySwap
|
||
|
|
use array.ArrayPermut
|
||
|
|
|
||
|
|
let selection_sort (xs: array int)
|
||
|
|
ensures { sorted xs }
|
||
|
|
ensures { permut_all (old xs) xs } =
|
||
|
|
|
||
|
|
let ref min = 0 in
|
||
|
|
for i = 0 to length xs - 1 do
|
||
|
|
invariant { sorted_sub xs 0 i }
|
||
|
|
invariant { permut_all (old xs) xs }
|
||
|
|
invariant { forall k1 k2: int. 0 <= k1 < i <= k2 < length xs -> xs[k1] <= xs[k2] }
|
||
|
|
|
||
|
|
min <- i;
|
||
|
|
for j = i + 1 to length xs - 1 do
|
||
|
|
invariant { i <= min < j }
|
||
|
|
invariant { forall k:int . i <= k < j -> xs[min] <= xs[k] }
|
||
|
|
|
||
|
|
if xs[j] < xs[min] then min <- j
|
||
|
|
done;
|
||
|
|
swap xs min i;
|
||
|
|
done
|
||
|
|
end
|