= Solution
The abstract state is a finite <partial function> $B$ from <strings> to <strings>, initially empty. Names and numbers below are non-null mathematical <strings>. `store` replaces an old binding if present; `delete` reports whether a binding existed.
``
trait Book {
// Abstract state B: finite partial map String -> String; initially empty.
// Pre: name != null && number != null.
// Post: B' = B updated at name with number.
def store(name: String, number: String): Unit
// Pre: name != null && name is in dom(B).
// Post: result = B(name), and B' = B.
def recall(name: String): String
// Pre: name != null.
// Post: result iff name is in dom(B), and B' = B.
def isInBook(name: String): Boolean
// Pre: name != null.
// Post: result iff name was in dom(B); B' = B with name removed.
def delete(name: String): Boolean
}
``
These <preconditions> and <postconditions> specify an <abstract data type>, independently of any <linked list>. In particular, a failed deletion leaves the abstract state unchanged, and recalling a missing name is outside the operation's specified domain.
Back to article page
