2.2. Insertion Sort on Arrays

• File: InsertSortArray.ml

Previously, we have studied insertion sort and its invariants on lists. Let us now use the same idea to sort an array. Since adding an element into an array prefix is more difficult than it would be for lists, we are going to implement the sorting a bit differently: namely, swapping, right-to-left, the elements of each prefix (taken from the beginning of the array increasingly), until it becomes sorted:

let insert_sort arr =
  let len = Array.length arr in
  for i = 0 to len - 1 do
    let j = ref i in
    while !j > 0 && arr.(!j) < arr.(!j - 1) do
      swap arr !j (!j - 1);
      j := !j - 1
    done
  done

We can now sort our array (notice that the operation does not return a new array, but rather modifies an old one):

# a1;;
- : int array = [|6; 8; 5; 2; 3; 7; 0|]
# insert_sort a1;;
- : unit = ()
# a1;;
- : int array = [|0; 2; 3; 5; 6; 7; 8|]

2.2.1. Tracing Insertion Sort

Why does insertion sort implemented this way works? An answer to that could be obtained via suitable invariants. But before we discover them, it might be a good idea to study what does the algorithm do, step by step. We are going to do that by instrumenting the code as follows:

(* A function unit -> unit that prints two spaces *)
let print_offset _ = Printf.printf "  "

let insert_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 ();

   let j = ref i in
    while !j > 0 && arr.(!j) < arr.(!j - 1) do
      print_offset ();
      print_int_sub_array 0 (i + 1) arr;
      print_int_sub_array (i + 1) len arr;
      print_newline ();

      swap arr !j (!j - 1);
      j := !j - 1;
    done;

    print_int_sub_array 0 (i + 1) arr;
    print_int_sub_array (i + 1) len arr;
    print_newline (); print_newline ()
done

That is, we print the array, divided via the current index i, at the beginning and at the end of each top-level iteration (at the end, the index is incremented, as it would be at the beginning of the next iteration or after the loop). In the inner loop, we pring the intermediate arrays. Notice that print_int_sub_array l u arr does not print the element arr.(u):

# insert_sort_print a1;;
[|  |] [| 6; 8; 5; 2; 3; 7; 0 |]
[| 6 |] [| 8; 5; 2; 3; 7; 0 |]

[| 6 |] [| 8; 5; 2; 3; 7; 0 |]
[| 6; 8 |] [| 5; 2; 3; 7; 0 |]

[| 6; 8 |] [| 5; 2; 3; 7; 0 |]
  [| 6; 8; 5 |] [| 2; 3; 7; 0 |]
  [| 6; 5; 8 |] [| 2; 3; 7; 0 |]
[| 5; 6; 8 |] [| 2; 3; 7; 0 |]

[| 5; 6; 8 |] [| 2; 3; 7; 0 |]
  [| 5; 6; 8; 2 |] [| 3; 7; 0 |]
  [| 5; 6; 2; 8 |] [| 3; 7; 0 |]
  [| 5; 2; 6; 8 |] [| 3; 7; 0 |]
[| 2; 5; 6; 8 |] [| 3; 7; 0 |]

[| 2; 5; 6; 8 |] [| 3; 7; 0 |]
  [| 2; 5; 6; 8; 3 |] [| 7; 0 |]
  [| 2; 5; 6; 3; 8 |] [| 7; 0 |]
  [| 2; 5; 3; 6; 8 |] [| 7; 0 |]
[| 2; 3; 5; 6; 8 |] [| 7; 0 |]

[| 2; 3; 5; 6; 8 |] [| 7; 0 |]
  [| 2; 3; 5; 6; 8; 7 |] [| 0 |]
[| 2; 3; 5; 6; 7; 8 |] [| 0 |]

[| 2; 3; 5; 6; 7; 8 |] [| 0 |]
  [| 2; 3; 5; 6; 7; 8; 0 |] [|  |]
  [| 2; 3; 5; 6; 7; 0; 8 |] [|  |]
  [| 2; 3; 5; 6; 0; 7; 8 |] [|  |]
  [| 2; 3; 5; 0; 6; 7; 8 |] [|  |]
  [| 2; 3; 0; 5; 6; 7; 8 |] [|  |]
  [| 2; 0; 3; 5; 6; 7; 8 |] [|  |]
[| 0; 2; 3; 5; 6; 7; 8 |] [|  |]

- : unit = ()

2.2.2. Insertion Sort Invariants

From the trace above, we can see that at the beginning and the end of each top-level iteration, the prefix arr.(0) .. arr.(i) is sorted. Furthermore, from the intermediate steps of the inner loop, we can see that in each iteration the new element “crawls” from the end towards the beginning, until it finds its position in the sorted prefix.

Importantly, at each iteration of the inner loop, the element at the position j is the smallest element of the prefix’s suffix, i.e., arr.(!j) .. arr.(i). We can capture that via the following definitions, which check that a sub-array of array is indeed sorted:

let sub_array_to_list l u arr =
  assert (l <= u);
  let res = ref [] in
  let i = ref (u - 1) in
  while l <= !i do
    res := arr.(!i) :: !res;
    i := !i - 1
  done;
  !res

let array_to_list arr =
  subarray_to_list 0 (Array.length arr) arr

let rec sorted ls =
  match ls with
  | [] -> true
  | h :: t ->
    List.for_all (fun e -> e >= h) t && sorted t

let sub_array_sorted l u arr =
  let ls = sub_array_to_list l u arr in
  sorted ls

let array_sorted arr =
  sub_array_sorted 0 (Array.length  arr) arr

The following functions check that an elemen min is a minimum with resepct to a particular sub-array:

let is_min ls min =
  List.for_all (fun e -> min <= e) ls

let is_min_sub_array l u arr min =
  let ls = sub_array_to_list l u arr in
  is_min ls min

We can now state the invariants:

let insert_sort_inner_loop_inv j i arr =
  is_min_sub_array !j (i + 1) arr arr.(!j) &&
  sub_array_sorted 0 !j arr &&
  sub_array_sorted (!j + 1) (i + 1) arr

let insert_sort_outer_loop_inv i arr =
  sub_array_sorted 0 i arr

and write the invariant-annotated version of the sorting:

let insert_sort_inv arr =
  let len = Array.length arr in
  for i = 0 to len - 1 do
    assert (insert_sort_outer_loop_inv i arr);
    let j = ref i in
    while !j > 0 && arr.(!j) < arr.(!j - 1) do
      assert (insert_sort_inner_loop_inv j i arr);
      swap arr !j (!j - 1);
      j := !j - 1;
      assert (insert_sort_inner_loop_inv j i arr);
    done;
    assert (insert_sort_outer_loop_inv (i + 1) arr)
  done

Notice that at the end of the inner loop, the three conjuncts of insert_sort_inner_loop_inv together imply that the entire prefix arr.(0) ... arr.(i) is sorted, i.e., the new element is correctly positioned within it.

2.2.3. Termination of Insertion Sort

It is not difficult to prove that insertion sort terminates: its outer loop is an iteration, bounded by len - 1. Its inner loop’s termination measure (variant) is j, so the loop terminates when j reaches 0.