Solution

ID: 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.

New to topics? Read the docs here!