= Solution
For a finite acyclic <linked list> define the node <sequence>, retaining <software object> identities, by
$$
L(\mathrm{null})=[],\qquad L(u)=u:L(u.\mathrm{next}).
$$
Then 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\mathbin{++}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 \b[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.
Back to article page
