Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Imperative programming / 4 / b / Solution

A sentinel node supplies a permanent predecessor for the first real node. Inserting or deleting at the front then uses the same predecessor.next update as an interior operation. Its datum is not a multiset element: the chosen extreme integer is merely unused sentinel data.

A representation invariant requires a nonnull fixed header, a finite acyclic chain starting at bagHeader.next, and exclusion of the header from that chain. Each node identity occurs once, although different nodes may have equal data. Representation links are owned by the implementation, so outside mutation cannot alter them unexpectedly.

The abstraction function counts occurrences:This yields nonnegative multiplicities and finite support. Initialization with a null successor gives the empty multiset. Excluding the sentinel is essential even when a real item equals its datum.