1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
(* Selection sort. *)
module SelectionSort
use int.Int
use ref.Ref
use array.Array
use array.IntArraySorted
use array.ArraySwap
use array.ArrayPermut
use array.ArrayEq
let selection_sort (a: array int)
ensures { sorted a /\ permut_all (old a) a } =
let min = ref 0 in
for i = 0 to length a - 1 do
(* a[0..i[ is sorted; now find minimum of a[i..n[ *)
invariant { sorted_sub a 0 i /\ permut_all (old a) a /\
forall k1 k2: int. 0 <= k1 < i <= k2 < length a -> a[k1] <= a[k2] }
(* let min = ref i in *) min := i;
for j = i + 1 to length a - 1 do
invariant {
i <= !min < j && forall k: int. i <= k < j -> a[!min] <= a[k] }
if a[j] < a[!min] then min := j
done;
label L in
if !min <> i then swap a !min i;
assert { permut_all (a at L) a }
done
let test1 () =
let a = make 3 0 in
a[0] <- 7; a[1] <- 3; a[2] <- 1;
selection_sort a;
a
let test2 () ensures { result.length = 8 } =
let a = make 8 0 in
a[0] <- 53; a[1] <- 91; a[2] <- 17; a[3] <- -5;
a[4] <- 413; a[5] <- 42; a[6] <- 69; a[7] <- 6;
selection_sort a;
a
exception BenchFailure
let bench () raises { BenchFailure -> true } =
let a = test2 () in
if a[0] <> -5 then raise BenchFailure;
if a[1] <> 6 then raise BenchFailure;
if a[2] <> 17 then raise BenchFailure;
if a[3] <> 42 then raise BenchFailure;
if a[4] <> 53 then raise BenchFailure;
if a[5] <> 69 then raise BenchFailure;
if a[6] <> 91 then raise BenchFailure;
if a[7] <> 413 then raise BenchFailure;
a
end
|
