= Solution
Append entries in increasing index order, keeping a tail reference so that repeated searches do not make construction quadratic:
``
def makeVector(elems: Array[Double]): Node = {
require(elems != null)
val h = makeZeroVector(elems.length)
var tail = h
var i = 0
while (i < elems.length) {
val v = elems(i)
require(!java.lang.Double.isNaN(v) &&
!java.lang.Double.isInfinite(v))
if (v != 0.0) {
val fresh = new Node(v, i, tail, h)
tail.next = fresh
h.prev = fresh
tail = fresh
}
i += 1
}
h
}
``
The <loop invariant> is $0\leq i\leq elems.length$, a valid circular representation of the nonzero entries in `elems[0..i)`, a fixed header dimension `elems.length`, and `tail eq h.prev`. The next nonzero index is greater than every stored index; appending the fresh <linked list node> preserves reciprocal links, including `tail.next eq h`. The <loop variant> is `elems.length-i`. At exit \b[the <abstraction function> yields exactly the input <array> as a <vector>]. There is one pass and constant work per entry: $\Theta(n)$ <time complexity> for $n>0$, $O(n+1)$ including emptiness, and $O(k+1)$ output storage for $k$ nonzero entries. Both signs of floating-point zero are represented by absence.
Back to article page
