Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Imperative programming / 4 / c / Solution

The precondition is n != null and $n\in L(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(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.