Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming / 3 / a

The first three subtractions are negative or return the already-seen zero, so addition is used. The fourth subtraction gives a new positive two; the next subtraction is negative. Thus $r(1),\dots ,r(5)=1,3,6,2,7$. These are the initial terms of Recamán's sequence.^[ref]

Use the already-filled prefix itself for membership tests. Long intermediates avoid overflow in the candidate calculations, while a checked conversion respects the required output type:The outer loop invariant is $1\le i\le a.length$ and $a(t)=r(t)$ for $0\le t<i$. The inner loop invariant says that $0\le j\le i$ and no processed entry before j equals the positive candidate. Its guard either reaches the end of the prefix, finds the candidate, or immediately rejects a nonpositive candidate. Its loop variant is $i-j$. This establishes exactly the choice required by the recurrence, so the outer loop invariant is preserved. The outer loop variant is $a.length-i$.

Extra storage is $O(1)$ beyond the supplied result array. Membership scans give an $O(N^2)$ upper bound for $N$ output entries. Addition, unlike the subtraction branch, is not required to avoid repeats: at indices $20$ and $24$ the value $42$ occurs twice. The code therefore does not try to enforce global distinctness. If an exact value eventually exceeds Int, the output interface cannot hold it; the check reports that limitation rather than wrapping the recurrence.

Regardless of which branch is taken, $r(n)\le r(n-1)+n$. Starting from zero and applying induction givesFor the inductive step, add $n$ to the bound $(n-1)n/2$ for the previous value. The subtraction branch gives an even smaller result, and positivity is checked there. This bound need not describe the actual growth sharply; it is sufficient to size a finite membership representation for a requested prefix.