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.