4.2. Merge Sort¶
- File:
MergeSort.ml
Merge sort is an algorithm that applies the divide-and-conquer idea to sorting.
4.2.1. Merging two sorted arrays¶
The heart of merge sort heart is the procedure merge
that merges
two already sorted arrays, from1
and from2
, into a dedicated
subarray ranging from lo
to hi
of an initial “destination”
array dest
:
let merge from1 from2 dest lo hi =
let len1 = Array.length from1 in
let len2 = Array.length from2 in
let i = ref 0 in
let j = ref 0 in
for k = lo to hi - 1 do
if !i >= len1
(* from1 is exhausted, copy everythin from from2 *)
then (dest.(k) <- from2.(!j); j := !j + 1)
else if !j >= len2
(* from2 is exhausted, copy everythin from from1 *)
then (dest.(k) <- from1.(!i); i := !i + 1)
else if from1.(!i) <= from2.(!j)
(* from1 has a smaller element, copy it, advance its index *)
then (dest.(k) <- from1.(!i); i := !i + 1)
(* from2 has a smaller element, copy it, advance its index *)
else (dest.(k) <- from2.(!j); j := !j + 1)
done
4.2.2. Main sorting procedure and its invariants¶
The main merge sort procedure preforms sorting recursively by (a) by splitting the given array range into two new smaller arrays repeatedly until reaching the primitive arrays (of size of 0 or 1, which are already sorted) and (b) merging the small arrays bottom-up into the larger arrays, until the top range is reached:
let copy_array arr lo hi =
let len = hi - lo in
assert (len >= 0);
if len = 0 then [||]
else
let res = Array.make len arr.(lo) in
for i = 0 to len - 1 do
res.(i) <- arr.(i + lo)
done;
res
let rec merge_sort arr =
let rec sort a =
let lo = 0 in
let hi = Array.length a in
if hi - lo <= 1 then ()
else
let mid = lo + (hi - lo) / 2 in
let from1 = copy_array a lo mid in
let from2 = copy_array a mid hi in
sort from1; sort from2;
merge from1 from2 a lo hi
in
sort arr
This style of merge sort is known as a top-down merge sort.
We can supplement this procedure with standard randomised tests:
let%test _ =
generate_int_array 10 |>
generic_array_sort_tester merge_sort
let%test _ =
generate_string_array 10 |>
generic_array_sort_tester merge_sort
let%test _ =
generate_key_value_array 10 |>
generic_array_sort_tester merge_sort
The correctness of merge sort relies on the correctness of the
merge
procedure, which generates a sorted array out of two smaller
sorted arrays by copying them in the correct interleaving order. We
can check that merge
indeed does so, by employing the familiar
auxiliary functions for testing. The pre- and post-condition of
merge
the can be stated as follows:
(* The two small arrays are sorted *)
let merge_pre from1 from2 =
array_sorted from1 && array_sorted from2
(* The merging is correct *)
let merge_post from1 from2 arr lo hi =
array_sorted arr &&
(let l1 = array_to_list from1 in
let l2 = array_to_list from2 in
let l = subarray_to_list lo hi arr in
same_elems (l1 @ l2) l)
Having checked the invariants for merge
it’s almost trivial to
annotate merge_sort
with invariants:
let rec merge_sort_inv arr =
let rec sort a =
let hi = Array.length a in
let lo = 0 in
if hi - lo <= 1 then ()
else
let mid = lo + (hi - lo) / 2 in
let from1 = copy_array a lo mid in
let from2 = copy_array a mid hi in
sort from1; sort from2;
assert (merge_pre from1 from2);
merge from1 from2 a lo hi;
assert (merge_post from1 from2 a lo hi)
in
sort arr