= Solution
For $N$ result entries the largest required index is $N-1$, so the bound in part (a)(iii) permits universe size $M=N(N-1)/2+1$. Check that the chosen universe can itself be expressed as an <array> length:
``
def recamanBitmap(a: Array[Int]): Unit = {
val n = a.length
if (n == 0) return
val capacity = n.toLong * (n.toLong - 1L) / 2L + 1L
require(capacity <= Int.MaxValue.toLong, "Bitmap universe too large")
val seen = new BitMapSet(capacity.toInt)
a(0) = 0
seen.add(0)
var i = 1
while (i < n) {
val candidate = a(i - 1).toLong - i.toLong
val next =
if (candidate > 0L && !seen.contains(candidate.toInt)) candidate
else a(i - 1).toLong + i.toLong
a(i) = next.toInt
seen.add(a(i))
i += 1
}
}
``
The <loop invariant> is that the result prefix contains exactly $r(0),\ldots,r(i-1)$ and the <abstraction function> of `seen` is their <set> of values. The universe bound ensures that each positive candidate being queried and each actual next value is less than `capacity`; values are nonnegative. Thus the conversions and the restricted `add` <precondition> are justified, rather than merely hoped to succeed. At a repeated addition, `add` returning false is harmless: the set of previously seen values is still updated correctly. The <loop variant> is $n-i$. \b[At return every result entry agrees with the original recurrence.]
Back to article page
