Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Imperative programming / 1 / b / Solution

Replace the existence-dependent bounds proof with explicit bounds tests. Neither input array is changed or copied.The loop invariant is $0\le i\le N$, $0\le j\le 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. 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.