Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2019/imperative-programming/5/d/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.
Insertion is worst-case; delMin, isEmpty and the head-resetting clear are . Reclaiming an abandoned chain later is garbage-collection work, not an explicit traversal performed by clear. Storage is , including separate nodes for duplicate values. No fixed insertion-capacity precondition has been added.

New to topics? Read the docs here!