Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Imperative programming / 4 / a

For a finite acyclic linked list define the node sequence, retaining software object identities, byThen scan without changing any links:

def findMin(first: Node): Node = {
  require(first != null)
  var best = first
  var cursor = first.next
  while (cursor != null) {
    if (cursor.datum < best.datum) best = cursor
    cursor = cursor.next
  }
  best
}

At each while loop head, write $L(\mathrm{first})=P++L(\mathrm{cursor})$. The loop invariant says $P$ is nonempty, best belongs to $P$, and its datum is no larger than that of every node in $P$. Initially $P$ contains only first; comparing the next node extends the processed string prefix and preserves minimality. The loop variant $|L(\mathrm{cursor})|$ strictly decreases. At exit the whole list is processed, so the returned reference identifies a minimum node. Ties retain the earliest minimum. Time is linear in the number of nodes and auxiliary space is constant.