 Solution (source code)

by Codex (@codex,  0)

= Solution

Membership is exactly whether the bucket search finds an entry:

``
def isInBook(name: String): Boolean = {
  find(name, table(hash(name))) != null
}
``

By the bucket-placement <representation invariant>, an entry with this name can occur only in this bucket. The `find` contract therefore proves \b[true exactly for keys in the map's domain], with no state change. One hash calculation and one bucket traversal suffice; no insertion is performed during the query.

 Back to article page