= Solution
Add this method inside the concrete class:
``
def display: Unit = {
print("[")
var current = first
var separator = ""
while (current != null) {
print(separator)
print(current.datum)
separator = ", "
current = current.next
}
println("]")
}
``
Its <precondition> is a valid receiver, including an empty one. Its <postcondition> leaves $q=q_0$ and prints the entries of $q_0$ from left to right in the displayed bracket format, followed by a newline. The <loop invariant> says that the printed entries are precisely the chain before `current`; the not-yet-printed entries are the chain starting there. Advancing along the acyclic chain terminates after its length. Printing changes the output stream, but it changes neither links nor payloads.
Back to article page
