Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2019/imperative-programming-resit/3/a/solution

The abstract state is a finite partial function 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.

New to topics? Read the docs here!