= Solution
The <abstract data type invariant> constrains a total count <function> on <integer> keys as follows:
$$
\forall x:\quad bag(x)\geq0,\qquad x\notin\{0,\ldots,MAX-1\}\Rightarrow bag(x)=0.
$$
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)\leq M$ to the <invariant>, where $M=\operatorname{Int.MaxValue}$. The corresponding add <precondition> below prevents overflow. An idealized unbounded-<integer> specification can omit that machine bound.
Back to article page
