Use the already-filled prefix itself for membership tests. The outer loop invariant is and for . The inner loop invariant says that and no processed entry before
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
}
}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 . This establishes exactly the choice required by the recurrence, so the outer loop invariant is preserved. The outer loop variant is .Extra storage is beyond the supplied result array. Membership scans give an upper bound for output entries. Addition, unlike the subtraction branch, is not required to avoid repeats: at indices and the value 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. Articles by others on the same topic
There are currently no matching articles.