= Solution
Replace the existence-dependent bounds proof with explicit bounds tests. Neither input <array> is changed or copied.
``
PROCEDURE commonOrNone(a, N, b, M);
VAR i, j: INTEGER;
BEGIN
i := 0; j := 0;
WHILE (i < N) AND (j < M) DO
IF a[i] = b[j] THEN RETURN Some(a[i])
ELSIF a[i] < b[j] THEN i := i + 1
ELSE j := j + 1
END
END;
RETURN None
END commonOrNone;
``
The <loop invariant> is $0\leq i\leq N$, $0\leq j\leq M$, and every common value of the original <arrays> lies in both remaining suffixes $a[i..N)$ and $b[j..M)$. Equivalently neither discarded prefix contains a common value. Advancing the smaller current value preserves this for the same ordering reason as in part (a).
Both <array bounds> are checked before any element is read. If the remaining heads are equal, all later entries are larger, so the returned value is the smallest. If either suffix becomes empty, the <loop invariant> proves there is no common value. The <loop variant> $(N-i)+(M-j)$ decreases on each unsuccessful comparison. \b[The result is `Some(smallest common value)` or `None`, with $O(N+M)$ time and $O(1)$ auxiliary space], including empty-input cases. A language without short-circuit operators can use nested tests; the guard here itself contains no array reads.
Back to article page
