 Solution

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

For finite acyclic chains, define the abstraction function recursively by

α (NIL) = [], α (p) = [p] + + α (p . tail) (p \neq = NIL) .

Here the list contains linked list nodes themselves. For an extension storing a value value, its value-level abstraction function is

α_{v} (p) = [p . value] + + α_{v} (p . tail)

. Finiteness and absence of a graph cycle ensure that these recursive definitions terminate. A dummy header node is excluded by applying

α

to its tail.

 New to topics? Read the docs here!