Proof of correctness
We consider the following loop invariants (during the merge step):
- During iteration of the loop, the output array contains the smallest values of .
- The th smallest element of is either in or , where and point to the current indices.
Perform induction on size of .
- Base case: , trivially true. Sorted.
- IH: note that this is strong induction. We assume merge sort returns a sorted array for .
- IS: for an array such that , we split into two subarrays and , and by IH we know that divide-and-conquer will return two sorted arrays. By loop invariant, we know merging and returns an output array that is sorted. Since , the algorithm works.