= 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 function>
$$
book=\{\,p.name\mapsto p.number\mid p\in L(list)\,\}.
$$
Name uniqueness makes this a <function>, rather than a relation assigning multiple numbers to one name. Initially `list == null`, so $L(list)=\varnothing$ and \b[the abstract book is empty]. Unreachable allocated nodes are outside this abstract state.
Back to article page
