= Solution
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:
``
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
}
}
}
``
The search <loop invariant> says that `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; \b[`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.
Back to article page
