Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2023/imperative-programming/4/a/solution

Let 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
Name uniqueness makes this a function, rather than a relation assigning multiple numbers to one name. Initially list == null, so and the abstract book is empty. Unreachable allocated nodes are outside this abstract state.

New to topics? Read the docs here!