= Solution
Represent the characteristic values of a bounded universe by one Boolean slot per possible member, a Boolean-<array> form of a <bitset>:
``
class BitMapSet(val MAXVALUE: Int) extends IntSet {
require(MAXVALUE >= 0)
private val bits = Array.fill(MAXVALUE)(false)
private var count = 0
def contains(elem: Int): Boolean =
0 <= elem && elem < MAXVALUE && bits(elem)
def add(elem: Int): Boolean = {
require(0 <= elem && elem < MAXVALUE, "Outside bitmap universe")
if (bits(elem)) false
else {
bits(elem) = true
count += 1
true
}
}
def size: Int = count
}
``
The <abstraction function> is $\alpha(bits,count)=\{x:0\leq x<MAXVALUE,\ bits(x)\}$. The <representation invariant> is that `bits.length==MAXVALUE`, its entries are Boolean, and `count` equals the number of true entries. Initialization gives the empty <set>; changing a false entry to true adds exactly its index and increments the count once. A repeated addition preserves both. All three operations have $O(1)$ <time complexity> after initialization; storage and explicit <array> initialization are $\Theta(MAXVALUE)$.
\b[The constructor requires $MAXVALUE\geq0$, and `add` requires $0\leq elem<MAXVALUE$.] `contains` remains total by returning false outside the representable universe; <short-circuit evaluation> protects the index. This finite representation cannot implement unrestricted addition of every `Int` while preserving the abstract contract. Its strengthened `add` <precondition> therefore makes it a restricted implementation, not a behaviorally substitutable implementation of the unrestricted trait for arbitrary clients. The <sequence> client below proves that it stays within the restricted universe.
Back to article page
