The abstract state is a finite partial function from strings to strings, initially empty. Names and numbers below are non-null mathematical strings. 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.
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
} Articles by others on the same topic
There are currently no matching articles.