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. Articles by others on the same topic
There are currently no matching articles.