= Solution
Insert before the first entry that is at least the new value; equal values remain separate occurrences:
``
class ListPriorityQueue extends PriorityQueue[Int] {
private var first: Node = null
def clear(): Unit = { first = null }
def isEmpty(): Boolean = first == null
def insert(x: Int): Unit = {
if (first == null || x <= first.value) {
first = new Node(x, first)
} else {
var p = first
while (p.next != null && p.next.value < x) {
p = p.next
}
p.next = new Node(x, p.next)
}
}
def delMin(): Int = {
require(first != null, "Empty priority queue")
val result = first.value
first = first.next
result
}
}
``
In the scanning branch, the <loop invariant> says that `p` is reachable and all values from `first` through `p` are strictly smaller than `x`. The rest of the chain is unchanged and remains sorted. The <loop variant> is the number of nodes after `p`. At exit either the next value is at least `x` or there is no next node, so inserting between `p` and `p.next` preserves the <representation invariant> and adds exactly one occurrence under the <abstraction function>. The head branch covers an empty chain, a new minimum and equality with the old minimum. `delMin` returns the head's minimum value and removes exactly that occurrence.
\b[Insertion is $O(n)$ worst-case; `delMin`, `isEmpty` and the head-resetting `clear` are $O(1)$]. Reclaiming an abandoned chain later is garbage-collection work, not an explicit traversal performed by `clear`. Storage is $\Theta(n)$, including separate nodes for duplicate values. No fixed insertion-capacity <precondition> has been added.
Back to article page
