The abstract data type invariant constrains a total count function on integer keys as follows:The initial state has every count zero, and . These conditions make the abstract state a multiset supported on the allowed finite key range. Since the interface returns an
Int, the implementations below use representable nonnegative multiplicities; equivalently add to the invariant, where . The corresponding add precondition below prevents overflow. An idealized unbounded-integer specification can omit that machine bound.Write for the incoming state and . Use the following explicit contracts.
For
remove(x), the precondition is and . The postcondition is , with every other count unchanged. This convention rejects removal of an absent occurrence rather than silently treating it as a no-op.For
count(x), the precondition is . The result is and the whole abstract state is unchanged. Counts outside the allowed range are zero in the mathematical total function, but this chosen interface requires an in-range query.Implement the count function directly in a private array:The representation invariant is that
class ArrayIntBag(val MAX: Int) extends IntBag {
require(MAX > 0)
private val c = new Array[Int](MAX)
private def inRange(x: Int): Boolean = 0 <= x && x < MAX
def add(x: Int): Unit = {
require(inRange(x))
require(c(x) < Int.MaxValue)
c(x) += 1
}
def remove(x: Int): Unit = {
require(inRange(x))
require(c(x) > 0)
c(x) -= 1
}
def count(x: Int): Int = {
require(inRange(x))
c(x)
}
}c has length MAX and every stored count is nonnegative. The abstraction function gives in range and zero outside it. Zero initialization establishes the invariant. An allowed addition changes exactly one entry without overflow; an allowed removal changes exactly one positive entry without making it negative; querying changes none. Thus each method implements its abstract postcondition as well as preserving the representation invariant. The private array prevents clients from bypassing those guarantees.Store the number of positive buckets, initially zero:Extend the representation invariant byThe abstraction function for the multiset is unchanged. The size operation has no precondition beyond a valid receiver; it returns the cardinality of the multiset support and changes no state. Replace the modifying methods inside the class byOnly transitions from zero to one or from one to zero change the support. Additions to an already positive bucket and removals leaving it positive preserve
private var distinct = 0
def size: Int = distinctdef add(x: Int): Unit = {
require(inRange(x))
require(c(x) < Int.MaxValue)
if (c(x) == 0) distinct += 1
c(x) += 1
}
def remove(x: Int): Unit = {
require(inRange(x))
require(c(x) > 0)
c(x) -= 1
if (c(x) == 0) distinct -= 1
}distinct. Thus size takes time, independently of MAX, and the other operations retain constant-time array access. Initialization still takes time. Articles by others on the same topic
There are currently no matching articles.