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
}The linked list node needs mutable fields for changing a stored number and rearranging links:The implementation will keep its real linked list nodes private to the
class Node(var name: String, var number: String, var next: Node)Book object and will not return linked list node references to clients.A permanent dummy header node gives even the first real linked list node a predecessor. Insertion into an empty linked list and deletion or movement of its first real linked list node then use the same link updates as internal cases. The header itself represents no contact, so it also removes the need to use a real name as a special end marker. A search still needs a null-end check.
Start with a private permanent header whose
next is null. Its two string fields are ignored. For a concrete state satisfying the representation invariant, define the abstraction functionThe representation invariant says that the header exists, the reachable real linked list is finite and acyclic, the header is not a real reachable linked list node, all real name/number fields are non-null strings, and real names are pairwise distinct. The real linked list nodes are owned by the book, so clients cannot mutate their fields through exposed references. Distinct names ensure that the displayed relation is a partial function. The initial empty linked list has abstraction . Reordering real linked list nodes changes the representation but not the abstract book.Search for the predecessor of the matching linked list node, or for the last linked list node if there is no match. This helper makes deletion uniform:The search loop invariant says that
class LinkedBook extends Book {
private val header = new Node("", "", null)
// Pre: name != null.
// Post: result is header or a real node.
// All real nodes through result have names different from name.
// result.next is null or has name equal to name.
// No state is changed.
private def findPrev(name: String): Node = {
require(name != null)
var p = header
while (p.next != null && p.next.name != name) {
p = p.next
}
p
}
def store(name: String, number: String): Unit = {
require(name != null && number != null)
val p = findPrev(name)
if (p.next == null)
p.next = new Node(name, number, null)
else
p.next.number = number
}
def recall(name: String): String = {
require(name != null)
val p = findPrev(name)
require(p.next != null, "Name is not in the book")
p.next.number
}
def isInBook(name: String): Boolean = {
require(name != null)
findPrev(name).next != null
}
def delete(name: String): Boolean = {
require(name != null)
val p = findPrev(name)
if (p.next == null) false
else {
p.next = p.next.next
true
}
}
}p is the header or a reachable real linked list node, and every real linked list node from the start through p has a name different from the requested name. The linked list has not been changed. Short-circuit evaluation protects p.next.name when the end is reached. The loop variant is the number of real linked list nodes strictly after p; finiteness and acyclicity make it a nonnegative decreasing integer. Consequently the helper's stated postcondition holds.For
store, a found name changes only its number; an absent name adds exactly one fresh binding at the end, maintaining uniqueness. For delete, unlinking the found linked list node removes exactly the requested binding; absence returns false without mutation. Both query operations preserve the abstraction function. Non-null preconditions are checked at entry; recall additionally checks membership using the one completed search, avoiding a redundant whole-list membership scan. The helper is the only additional operation and its complete behavioral contract is stated above.Let be the number of real contacts, and suppose the requested name is at position , counting from one. The implementation above makes exactly name-equality comparisons, including the successful comparison; null checks are not string comparisons. Thus the minimum is one, when the first real contact is requested, and the maximum is , when the last is requested. The precondition excludes unsuccessful recalls and recalls on an empty book. This counts calls to string equality, not individual character inspections within each call.
Use the move-to-front heuristic. Replace only The search has the same loop invariant and loop variant as before. Detach the existing linked list node before inserting it immediately after the dummy header node. The branch for an already-first linked list node avoids linking it to itself. Every real contact still occurs exactly once with the same name/number binding, so the representation invariant and abstraction function are preserved at return. No new linked list node is allocated, and an immediate repeated recall needs one name comparison. The present recall still pays its original search cost; the gain is for later repeated access.
recall in LinkedBook by:def recall(name: String): String = {
require(name != null)
val p = findPrev(name)
require(p.next != null, "Name is not in the book")
val found = p.next
if (p ne header) {
p.next = found.next
found.next = header.next
header.next = found
}
found.number
} Articles by others on the same topic
There are currently no matching articles.