Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 3 / d / Solution

Inside the supplied PaymentsHash class, scan until a matching node or the end of the chain. A null return means the user has no record in this bucket.

private def find(user: Int, head: PaymentsHash.Node): PaymentsHash.Node = {
  var p = head
  while (p != null && p.user != user) p = p.next
  p
}

The loop invariant says that every node already passed has a different user identity and p heads the unexamined suffix. Short-circuit evaluation of && prevents dereferencing null. The representation invariant supplies an acyclic finite chain, so each unsuccessful step shortens that suffix and proves algorithm termination. The code changes no node fields.