Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Imperative programming resit / 3 / d

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 functionThe 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.