2.3. Selection Sort¶
- File:
SelectSortArray.ml
Selection sort is another sorting algorithm based on finding a minimum in an array. Unlike insertion sort, which locates each new element in an already sorted prefix, selection sort obtains the sorted prefix by “extending” it, at each iteration, with a minimum of a not-yet sorted suffix of the array:
let select_sort arr =
let len = Array.length arr in
for i = 0 to len - 1 do
for j = i + 1 to len - 1 do
if arr.(j) < arr.(i)
then swap arr i j
else ()
done
done
2.3.1. Tracing Selection Sort¶
Let us print intermediate stages of the selection sort as follows:
let select_sort_print arr =
let len = Array.length arr in
for i = 0 to len - 1 do
print_int_sub_array 0 i arr;
print_int_sub_array i len arr;
print_newline ();
for j = i to len - 1 do
print_offset ();
Printf.printf "j = %d, a[j] = %d, a[i] = %d: " j arr.(j) arr.(i);
print_int_sub_array 0 i arr;
print_int_sub_array i len arr;
print_newline ();
if arr.(j) < arr.(i)
then swap arr i j
else ()
done;
print_int_sub_array 0 (i + 1) arr;
print_int_sub_array (i + 1) len arr;
print_newline (); print_newline ();
done
This results in the following output:
# select_sort_print a1;;
[| |] [| 6; 8; 5; 2; 3; 7; 0 |]
j = 0, a[j] = 6, a[i] = 6: [| |] [| 6; 8; 5; 2; 3; 7; 0 |]
j = 1, a[j] = 8, a[i] = 6: [| |] [| 6; 8; 5; 2; 3; 7; 0 |]
j = 2, a[j] = 5, a[i] = 6: [| |] [| 6; 8; 5; 2; 3; 7; 0 |]
j = 3, a[j] = 2, a[i] = 5: [| |] [| 5; 8; 6; 2; 3; 7; 0 |]
j = 4, a[j] = 3, a[i] = 2: [| |] [| 2; 8; 6; 5; 3; 7; 0 |]
j = 5, a[j] = 7, a[i] = 2: [| |] [| 2; 8; 6; 5; 3; 7; 0 |]
j = 6, a[j] = 0, a[i] = 2: [| |] [| 2; 8; 6; 5; 3; 7; 0 |]
[| 0 |] [| 8; 6; 5; 3; 7; 2 |]
[| 0 |] [| 8; 6; 5; 3; 7; 2 |]
j = 1, a[j] = 8, a[i] = 8: [| 0 |] [| 8; 6; 5; 3; 7; 2 |]
j = 2, a[j] = 6, a[i] = 8: [| 0 |] [| 8; 6; 5; 3; 7; 2 |]
j = 3, a[j] = 5, a[i] = 6: [| 0 |] [| 6; 8; 5; 3; 7; 2 |]
j = 4, a[j] = 3, a[i] = 5: [| 0 |] [| 5; 8; 6; 3; 7; 2 |]
j = 5, a[j] = 7, a[i] = 3: [| 0 |] [| 3; 8; 6; 5; 7; 2 |]
j = 6, a[j] = 2, a[i] = 3: [| 0 |] [| 3; 8; 6; 5; 7; 2 |]
[| 0; 2 |] [| 8; 6; 5; 7; 3 |]
[| 0; 2 |] [| 8; 6; 5; 7; 3 |]
j = 2, a[j] = 8, a[i] = 8: [| 0; 2 |] [| 8; 6; 5; 7; 3 |]
j = 3, a[j] = 6, a[i] = 8: [| 0; 2 |] [| 8; 6; 5; 7; 3 |]
j = 4, a[j] = 5, a[i] = 6: [| 0; 2 |] [| 6; 8; 5; 7; 3 |]
j = 5, a[j] = 7, a[i] = 5: [| 0; 2 |] [| 5; 8; 6; 7; 3 |]
j = 6, a[j] = 3, a[i] = 5: [| 0; 2 |] [| 5; 8; 6; 7; 3 |]
[| 0; 2; 3 |] [| 8; 6; 7; 5 |]
[| 0; 2; 3 |] [| 8; 6; 7; 5 |]
j = 3, a[j] = 8, a[i] = 8: [| 0; 2; 3 |] [| 8; 6; 7; 5 |]
j = 4, a[j] = 6, a[i] = 8: [| 0; 2; 3 |] [| 8; 6; 7; 5 |]
j = 5, a[j] = 7, a[i] = 6: [| 0; 2; 3 |] [| 6; 8; 7; 5 |]
j = 6, a[j] = 5, a[i] = 6: [| 0; 2; 3 |] [| 6; 8; 7; 5 |]
[| 0; 2; 3; 5 |] [| 8; 7; 6 |]
[| 0; 2; 3; 5 |] [| 8; 7; 6 |]
j = 4, a[j] = 8, a[i] = 8: [| 0; 2; 3; 5 |] [| 8; 7; 6 |]
j = 5, a[j] = 7, a[i] = 8: [| 0; 2; 3; 5 |] [| 8; 7; 6 |]
j = 6, a[j] = 6, a[i] = 7: [| 0; 2; 3; 5 |] [| 7; 8; 6 |]
[| 0; 2; 3; 5; 6 |] [| 8; 7 |]
[| 0; 2; 3; 5; 6 |] [| 8; 7 |]
j = 5, a[j] = 8, a[i] = 8: [| 0; 2; 3; 5; 6 |] [| 8; 7 |]
j = 6, a[j] = 7, a[i] = 8: [| 0; 2; 3; 5; 6 |] [| 8; 7 |]
[| 0; 2; 3; 5; 6; 7 |] [| 8 |]
[| 0; 2; 3; 5; 6; 7 |] [| 8 |]
j = 6, a[j] = 8, a[i] = 8: [| 0; 2; 3; 5; 6; 7 |] [| 8 |]
[| 0; 2; 3; 5; 6; 7; 8 |] [| |]
- : unit = ()
Notice that at each iteration of the inner loop, a new minimum of the
remaining suffix is identified and at the end this is what becomes and
“extension” of the currently growing prefix: 0
, 2
, 3
,
5
, etc. During the inner iteration, we look for minimum in the
same way we were looking for a minimum in a list. All elements in the
non-sorted suffix are larger or equal than elements in the prefix. The
current element arr.(i)
is, thus a minimum of the
prefix-of-the-suffix of the array, yet it’s larger than any element in
the prefix.
2.3.2. Invariants of Selection Sort¶
The observed above intuition can be captured by the following invariants:
let suffix_larger_than_prefix i arr =
let len = Array.length arr in
let prefix = sub_array_to_list 0 i arr in
let suffix = sub_array_to_list i len arr in
List.for_all (fun e ->
List.for_all (fun f -> e <= f) suffix
) prefix
let select_sort_outer_inv i arr =
sub_array_sorted 0 i arr &&
suffix_larger_than_prefix i arr
let select_sort_inner_inv j i arr =
is_min_sub_array i j arr arr.(i) &&
sub_array_sorted 0 i arr &&
suffix_larger_than_prefix i arr
leading to the following annotated version:
let select_sort_inv arr =
let len = Array.length arr in
for i = 0 to len - 1 do
assert (select_sort_outer_inv i arr);
for j = i to len - 1 do
assert (select_sort_inner_inv j i arr);
if arr.(j) < arr.(i)
then swap arr i j
else ();
assert (select_sort_inner_inv (j + 1) i arr);
done;
assert (select_sort_outer_inv (i + 1) arr);
done
Notice that the inner invariant, when j
becomes len
(i.e.,
right before the end of the last iteration), implies that the found
element arr.(i)
is the global minimum of the suffix (which is all
larger than prefix), and, hence the sorted prefix can be extended with
this element, while remaining sorted.
2.3.3. Termination of Selection Sort¶
The algorithm terminates, as both loops in it, inner and outer are bounded and iterate over finite sub-arrays of a given array.