Past exam of the year 1 of the computer science course of the University of Oxford / 2015 / Imperative programming (resit) / 3 / b / Solution

Use a merge algorithm with one unread index in each run. Here u is the module's array; the destination $[d,d+c-a)$ is disjoint from the source and lies within the array bounds:Let $A,B$ denote the original two runs. The first loop invariant says $k-d=(i-a)+(j-b)$ and $u[d..k)$ is the sorted merge of $A[\mathrm{0..}i-a)$ and $B[\mathrm{0..}j-b)$; moreover each emitted value is at most every unread value. Choosing the smaller head preserves that condition. Equal heads are taken from the first run, giving stable sorting within this merge. The loop variant is $(b-i)+(c-j)$.

For each copying loop, the output remains the sorted merge of the consumed prefixes, at least one source run is exhausted, and only the indicated suffix remains. The respective loop variants are $b-i$ and $c-j$. At exit both source runs are exhausted:The destination's multiset is the sum of the two source multisets.