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

Let $L(list)$ denote the non-null nodes reachable from the head. The representation invariant requires a finite acyclic null-terminated linked list and pairwise distinct names among its reachable nodes. Names and numbers retain the interface's string data type interpretation; no ordering of names is required.

The abstraction function is the finite partial functionName uniqueness makes this a function, rather than a relation assigning multiple numbers to one name. Initially list == null, so $L(list)=\varnothing$ and the abstract book is empty. Unreachable allocated nodes are outside this abstract state.