= Solution
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:
``
def recaman(a: Array[Int]): Unit = {
if (a.length == 0) return
a(0) = 0
var i = 1
while (i < a.length) {
val candidate = a(i - 1).toLong - i.toLong
var j = 0
while (candidate > 0L && j < i && a(j).toLong != candidate) {
j += 1
}
val next =
if (candidate > 0L && j == i) candidate
else a(i - 1).toLong + i.toLong
require(next <= Int.MaxValue.toLong, "Sequence value exceeds Int")
a(i) = next.toInt
i += 1
}
}
``
The outer <loop invariant> is $1\leq i\leq a.length$ and $a(t)=r(t)$ for $0\leq t<i$. The inner <loop invariant> says that $0\leq j\leq 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$.
\b[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.
Back to article page
