Array multiset

A multiset of keys in a fixed finite integer range represented by one nonnegative count per key. The abstraction function extends the stored array counts by zero outside the range. Single-key additions, removals and queries use constant array work, provided overflow and operation preconditions are handled. Encapsulation of the count array is necessary to preserve its representation invariant.

Maintain a counter equal to the number of positive count-array entries. Increment it only when an addition changes zero to one; decrement it only when a removal changes one to zero. Other count changes leave the support unchanged. Initialization at zero and these cases prove the representation invariant by induction over completed operations, giving a constant-time distinct-size query.