= Solution
Write $bag_0$ for the incoming state and $M=\operatorname{Int.MaxValue}$. Use the following explicit contracts.
For `add(x)`, the <precondition> is $0\leq x<MAX$ and $bag_0(x)<M$. The <postcondition> is $bag(x)=bag_0(x)+1$ and $bag(y)=bag_0(y)$ for every $y\neq x$.
For `remove(x)`, the <precondition> is $0\leq x<MAX$ and $bag_0(x)>0$. The <postcondition> is $bag(x)=bag_0(x)-1$, 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 $0\leq x<MAX$. The result is $bag_0(x)$ 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.
Back to article page
