Assume The search loop invariant says that the structure is unchanged and every ordinary linked list node passed has index smaller than
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
}
}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. Exactly the requested coordinate changes. With stored entries, the search costs and the splice costs constant time; checking the whole input structure is a caller obligation, rather than an unmentioned scan inside each call. Articles by others on the same topic
There are currently no matching articles.