= Solution
For each table index $b$, let $C_b=L(table(b))$ be the <set> of non-null nodes reachable by following `next`. A sufficient <representation invariant> is:
* The <array> has exactly $N>0$ buckets, and every bucket heads a finite acyclic <linked list>.
* The sets $C_b$ are pairwise disjoint, so one physical node cannot belong to two buckets.
* Every reachable node has a valid user identity, lies in bucket `hash(node.user)`, and has both counters between zero and `Int.MaxValue`.
* User identities are unique among all reachable nodes, not merely within a single chain.
The <abstraction function> maps these nodes to the total <functions> of part (a): if the unique node for $u$ exists, $I(u)$ and $O(u)$ are its fields; otherwise both are zero. A stored record with two zero counters is harmless and has the same observable meaning as an absent record. This intentionally permits multiple concrete representations of the same abstract <program state>.
Initially every bucket is null, so the <representation invariant> holds and the <abstraction function> yields all zeros. The successful-update branch preserves every structural condition; the insertion branch creates a fresh node with a previously absent identity in its correct bucket. Both branches realize exactly the incoming-increment <postcondition>, demonstrating <correct operations through an abstraction function>.
Back to article page
