 Solution

The abstract data type invariant constrains a total count function on integer keys as follows:The initial state has every count zero, and $MAX>0$. 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 $bag(x)\le M$ to the invariant, where $M=Int.MaxValue$. The corresponding add precondition below prevents overflow. An idealized unbounded-integer specification can omit that machine bound.