Merge sort

Proof of correctness

We consider the following loop invariants (during the merge step):

• During iteration $l$ of the loop, the output array $C[\mathrm{1..}l-1]$ contains the $l-1$ smallest values of $A_1\cup A_2$.
• The $l$th smallest element of $C$ is either in $A_1[i]$ or $A_2[j]$, where $i$ and $j$ point to the current indices.

Perform induction on size of $A$.

• Base case: $|A|=1$, trivially true. Sorted.
• IH: note that this is strong induction. We assume merge sort returns a sorted array $A$ for $|A|<n$.
• IS: for an array $A$ such that $|A|=n$, we split into two subarrays $A_1$ and $A_2$, and by IH we know that divide-and-conquer will return two sorted arrays. By loop invariant, we know merging $A_1$ and $A_2$ returns an output array $C$ that is sorted. Since $A=C$, the algorithm works.