Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Imperative programming (resit) / 3 / a / 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.