= Solution
The <precondition> is \b[`n != null` and $n\in L(\mathrm{bagHeader.next})$], using node identity rather than datum equality. Search for its predecessor:
``
def delete(n: Node): Unit = {
var previous = bagHeader
while (previous.next ne n) {
previous = previous.next
}
previous.next = n.next
n.next = null
}
``
The <loop invariant> states that `previous` is the header or a preceding real node, and $n\in L(\mathrm{previous.next})$. The <loop variant> is the number of links from `previous` to `n` minus one. The <precondition> guarantees that this search reaches the predecessor before a null dereference. Replacing its successor by `n.next` bypasses exactly the requested node; clearing the removed node's link detaches it for later reuse. The order and identities of every other node remain unchanged. In abstract terms, only the multiplicity of `n.datum` decreases, by one. The worst-case time is linear; the pointer modification itself is constant-time.
Back to article page
