# 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.