Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Imperative programming / 4 / e

Let $B_0$ and $R_0=L(bagHeader.next)$ describe the entry state. The postcondition is: the multiset is empty; the returned chain is sorted nondecreasingly; its node sequence is a permutation of $R_0$. Thus it has exactly the original multiset of data and preserves all duplicates. Strict increase is impossible when the multiset contains repeated values.

def getAllSorted(): Node = {
  var head: Node = null
  var tail: Node = null
  while (bagHeader.next != null) {
    val nextSmallest = findMin(bagHeader.next)
    delete(nextSmallest)
    nextSmallest.next = null
    if (head == null) head = nextSmallest
    else tail.next = nextSmallest
    tail = nextSmallest
  }
  head
}

The loop invariant partitions the original node identities into the remaining multiset and the returned-prefix chain. The latter is sorted, its last node is tail, and every datum in it is no larger than every remaining datum. Selecting a minimum and appending that detached node preserves all these facts. The loop variant is the number of real nodes remaining in the multiset, decreasing by one. When it reaches zero the string prefix contains the entire original node set, proving the postcondition. An initially empty multiset returns null.

This is linked-list selection sort. Its time is $\Theta (m^2)$ in general, from successive scans of lengths $m,m-1,\dots ,1$, and it uses constant auxiliary space: it relinks original nodes instead of allocating a new node for each item.