Represent the characteristic values of a bounded universe by one Boolean slot per possible member, a Boolean-array form of a bitset:The abstraction function is . The representation invariant is that
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
}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 time complexity after initialization; storage and explicit array initialization are .The constructor requires , and
add requires . 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. Articles by others on the same topic
There are currently no matching articles.