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

Treat removal of the first node separately; otherwise find its predecessor:

procedure Remove(x: List; var xs: List)
    require x is a node reachable from xs
    if xs = x then
        xs := x.next
    else
        p := xs
        while p.next != x do
            p := p.next
        p.next := x.next
    x.next := nil

In the search branch the loop invariant says that p is before x in the original linked list, x is reachable from p.next, and no links have yet changed. The remaining link distance to x decreases at every advance, so membership of x guarantees a predecessor is found. Bypassing it removes exactly that cell, rather than an arbitrary equal-valued cell. Detaching x.next leaves a standalone removed node and preserves the relative order and object identities of all retained nodes.