= Solution
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.
Back to article page
