For result entries the largest required index is , so the bound in part (a)(iii) permits universe size . Check that the chosen universe can itself be expressed as an array length:The loop invariant is that the result prefix contains exactly and the abstraction function of
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
}
}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 . At return every result entry agrees with the original recurrence. Articles by others on the same topic
There are currently no matching articles.