Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 4 / c

Save the next pointer before redirecting it, then advance the two working heads. No node is allocated and the name/number fields are untouched.

def reverseBook(): Unit = {
  var prev: Node = null
  var cur = list
  while (cur != null) {
    val following = cur.next
    cur.next = prev
    prev = cur
    cur = following
  }
  list = prev
}

Let $S$ be the original sequence of node identities, not just their possibly equal field values. Write $P$ for the sequence currently headed by prev and $Q$ for that headed by cur. A suitable loop invariant for in-place linked-list reversal iswith both working lists finite, acyclic, disjoint, together containing exactly the original nodes, and with every name and number unchanged. Here ++ means concatenation. Initially $P=[]$ and $Q=S$. One iteration takes $q$ from the front of $Q=q:Q^{\prime }$ and replaces $(P,Q)$ by $(q:P,Q^{\prime })$. Since $\mathrm{reverse}(q:P)=\mathrm{reverse}(P)++[q]$, the equation is preserved. Saving following before changing cur.next retains access to $Q^{\prime }$.

The loop variant is the length of $Q$, decreasing by one. At exit $Q=[]$, so $P=\mathrm{reverse}(S)$; assigning the head establishes reversal. The empty and singleton cases work without a special branch. The abstraction function of the phone book ignores order, so it still maps every original name to its original number. All original node identities are reused, with $O(K)$ running time and $O(1)$ auxiliary space.