Solution

ID: 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 is disjoint from the source and lies within the array bounds:
PROCEDURE Merge(a, b, c, d: INTEGER);
VAR i, j, k: INTEGER;
BEGIN
  i := a; j := b; k := d;
  WHILE (i < b) & (j < c) DO
    IF u[i] <= u[j] THEN
      u[k] := u[i]; i := i+1
    ELSE
      u[k] := u[j]; j := j+1
    END;
    k := k+1
  END;
  WHILE i < b DO
    u[k] := u[i]; i := i+1; k := k+1
  END;
  WHILE j < c DO
    u[k] := u[j]; j := j+1; k := k+1
  END
END Merge;
Let denote the original two runs. The first loop invariant says and is the sorted merge of and ; 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 .
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 and . At exit both source runs are exhausted:
The destination's multiset is the sum of the two source multisets.

New to topics? Read the docs here!