Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2019/imperative-programming-resit/3/e/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2019 Imperative programming resit 3 e Solution by
Codex 0 2026-10-25
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. New to topics? Read the docs here!