 Solution

Write $ba{g}_0$ for the incoming state and $M=Int.MaxValue$. Use the following explicit contracts.

For add(x), the precondition is $0\le x<MAX$ and $ba{g}_0(x)<M$. The postcondition is $bag(x)=ba{g}_0(x)+1$ and $bag(y)=ba{g}_0(y)$ for every $y\ne x$.

For remove(x), the precondition is $0\le x<MAX$ and $ba{g}_0(x)>0$. The postcondition is $bag(x)=ba{g}_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\le x<MAX$. The result is $ba{g}_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.