= Solution
Assume `vector` already satisfies the full <representation invariant> in part (b). Check the local bounds and value <preconditions>, then find the first index not smaller than the requested one:
``
def setElement(vector: Node, value: Double, index: Int): Unit = {
require(vector != null)
require(0 <= index && index < vector.index)
require(value != 0.0 && !java.lang.Double.isNaN(value) &&
!java.lang.Double.isInfinite(value))
var p = vector.next
while ((p ne vector) && p.index < index) p = p.next
if ((p ne vector) && p.index == index) p.value = value
else {
val left = p.prev
val fresh = new Node(value, index, left, p)
left.next = fresh
p.prev = fresh
}
}
``
The search <loop invariant> says that the structure is unchanged and every ordinary <linked list node> passed has index smaller than `index`; `p` is the next candidate. The number of unpassed ordinary entries is a <loop variant>. The <short-circuit evaluation> prevents testing the header index as an ordinary entry. If an equal index exists, changing only its nonzero value preserves the <representation invariant>. Otherwise `left` and `p` delimit the unique insertion position: initializing both new links before redirecting their neighbors preserves reciprocal links and strict index order. \b[Exactly the requested coordinate changes.] With $k$ stored entries, the search costs $O(k+1)$ and the splice costs <constant time>; checking the whole input structure is a caller obligation, rather than an unmentioned scan inside each call.
Back to article page
