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
|
include "arrays.why"
(** Selection sort *)
parameter t : int array
let selection () =
{ array_length(t) >= 1 }
begin
init:
let i = ref 0 in
while !i < (array_length_ t)-1 do
(* t[0..i-1] is already sorted *)
{ invariant 0 <= i <= array_length(t)-1 and
sorted_array(t, 0, i-1) and permutation(t, t@init) and
forall k,l:int. 0 <= k < i ->
i <= l < array_length(t) -> t[k] <= t[l]
variant array_length(t) - i }
(* we look for the minimum of t[i..n-1] *)
let min = ref !i in
let j = ref !i + 1 in
begin
while !j < (array_length_ t) do
{ invariant i+1 <= j <= array_length(t) and
i <= min < array_length(t) and
forall k:int. i <= k < j -> t[min] <= t[k]
variant array_length(t) - j }
if t[!j] < t[!min] then min := !j;
j := !j + 1
done;
(* we swap t[i] and t[min] *)
let w = t[!min] in begin t[!min] := t[!i]; t[!i] := w end
end;
i := !i + 1
done
end
{ sorted_array(t, 0, array_length(t)-1) and permutation(t, t@) }
(*
Local Variables:
compile-command: "gwhy-bin -split-user-conj selection.mlw"
End:
*)
|
