Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Imperative programming / 3 / a

Remember the minimum node while scanning the remaining suffix:

function FindMin(xs: List): List
    require xs != nil
    best := xs
    p := xs.next
    while p != nil do
        if p.x < best.x then best := p
        p := p.next
    return best

The loop invariant says that the processed prefix is nonempty, best is a node of that prefix, and its key is no greater than any other processed key. The links are unchanged. Advancing p extends the prefix by one; the number of unprocessed nodes decreases. When it reaches nil, best is the minimum of the whole finite singly linked list. Strict comparison retains the first minimum among ties.