= Solution
Let $B_0$ and $R_0=L(\mathrm{bagHeader.next})$ describe the entry state. The <postcondition> is: \b[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,\ldots,1$, and it uses constant auxiliary space: it relinks original nodes instead of allocating a new node for each item.
Back to article page
