= Solution
Start with a private permanent header whose `next` is null. Its two <string> fields are ignored. For a concrete state satisfying the <representation invariant>, define the <abstraction function>
$$
\alpha(header)=\{v.name\mapsto v.number:\ v\text{ is a real node reachable from }header.next\}.
$$
The <representation invariant> says that the header exists, the reachable real <linked list> is finite and acyclic, the header is not a real reachable <linked list node>, all real name/number fields are non-null <strings>, and real names are pairwise distinct. The real <linked list nodes> are owned by the book, so clients cannot mutate their fields through exposed references. Distinct names ensure that the displayed relation is a <partial function>. The initial empty <linked list> has abstraction $\varnothing$. Reordering real <linked list nodes> changes the representation but not the abstract book.
Back to article page
