Solution (source code)

= Solution

Implement the count <function> directly in a private <array>:
``
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)
  }
}
``
The <representation invariant> is that `c` has length `MAX` and every stored count is nonnegative. The <abstraction function> gives $bag(x)=c(x)$ 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.