= Solution
Inside the supplied `PaymentsHash` class, scan until a matching node or the end of the chain. \b[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.
Back to article page
