Let denote the non-null nodes reachable from the head. The representation invariant requires a finite acyclic null-terminated linked list and pairwise distinct names among its reachable nodes. Names and numbers retain the interface's string data type interpretation; no ordering of names is required.
The abstraction function is the finite partial functionName uniqueness makes this a function, rather than a relation assigning multiple numbers to one name. Initially
list == null, so and the abstract book is empty. Unreachable allocated nodes are outside this abstract state.Inside
LinkedListBook, traverse without modifying the head or any node:def printBook(): Unit = {
var p = list
while (p != null) {
println(p.name + ":" + p.number)
p = p.next
}
}The loop invariant is that precisely the prefix before
p has been printed, once per node, in list order; p heads the remaining suffix. The null-terminated linked list invariant proves termination and prevents duplicate output through cycles. An empty list prints nothing. The abstraction function is unchanged, and the traversal takes node visits for entries.Save the next pointer before redirecting it, then advance the two working heads. No node is allocated and the name/number fields are untouched.
def reverseBook(): Unit = {
var prev: Node = null
var cur = list
while (cur != null) {
val following = cur.next
cur.next = prev
prev = cur
cur = following
}
list = prev
}Let be the original sequence of node identities, not just their possibly equal field values. Write for the sequence currently headed by
prev and for that headed by cur. A suitable loop invariant for in-place linked-list reversal iswith both working lists finite, acyclic, disjoint, together containing exactly the original nodes, and with every name and number unchanged. Here ++ means concatenation. Initially and . One iteration takes from the front of and replaces by . Since , the equation is preserved. Saving following before changing cur.next retains access to .The loop variant is the length of , decreasing by one. At exit , so ; assigning the head establishes reversal. The empty and singleton cases work without a special branch. The abstraction function of the phone book ignores order, so it still maps every original name to its original number. All original node identities are reused, with running time and auxiliary space.
In-place reversal preserves node identities while moving nodes from an untouched suffix into a reversed prefix
. Details. 
private var last: Node = nullNull represents the empty book. In a nonempty book,
last.next is the first node, and following next makes one finite simple cycle containing last. Names are unique around that cycle. This representation makes appending a new entry constant-time once a failed name search has established absence. The abstraction function collects every name/number pair on one complete turn of the cycle, rather than following pointers until null.Starting at
last.next, visit each node once and stop when the traversal would return to its start. This helper is private so that callers do not receive writable nodes from the representation.private def find(name: String): Node = {
if (last == null) return null
val first = last.next
var p = first
do {
if (p.name == name) return p
p = p.next
} while (p ne first)
null
}Null means no entry has that name. The test
p ne first compares object identity, not the equality of name or number fields. At each iteration all previously visited nodes failed the name test. The finite simple cycle guarantees that either a match is found or the traversal returns to first after exactly one turn. A singleton cycle is inspected exactly once. Stopping at null instead would fail to terminate on this representation.Update an existing node, otherwise append one fresh node while preserving the cycle:
def store(name: String, number: String): Unit = {
val p = find(name)
if (p != null) p.number = number
else {
val fresh = new Node(name, number, null)
if (last == null) {
fresh.next = fresh
last = fresh
} else {
fresh.next = last.next
last.next = fresh
last = fresh
}
}
}For an existing name, changing only its number realizes replacement in the abstract partial function. On an empty book, the new node points to itself, establishing a singleton cycle. On a nonempty book, its successor becomes the old first node and the old last points to it; advancing
last leaves the first node unchanged and closes the enlarged cycle. Since a full search established absence, name uniqueness is preserved. Thus the postcondition is exactly the old book with this name mapped to the supplied number, and all other entries unchanged. A store takes running time for the name search and additional pointer work. Articles by others on the same topic
There are currently no matching articles.