= Solution
Inside `LinkedListBook`, traverse without modifying the head or any node:
``
def printBook(): Unit = {
var p = list
while (p != null) {
println(p.name + ":" + p.number)
p = p.next
}
}
``
The <loop invariant> is that precisely the prefix before `p` has been printed, once per node, in list order; `p` heads the remaining suffix. The <null-terminated linked list> invariant proves termination and prevents duplicate output through cycles. An empty list prints nothing. The <abstraction function> is unchanged, and the traversal takes $O(K)$ node visits for $K$ entries.
Back to article page
