Remember the minimum node while scanning the remaining suffix:
function FindMin(xs: List): List
require xs != nil
best := xs
p := xs.next
while p != nil do
if p.x < best.x then best := p
p := p.next
return bestThe loop invariant says that the processed prefix is nonempty,
best is a node of that prefix, and its key is no greater than any other processed key. The links are unchanged. Advancing p extends the prefix by one; the number of unprocessed nodes decreases. When it reaches nil, best is the minimum of the whole finite singly linked list. Strict comparison retains the first minimum among ties.Treat removal of the first node separately; otherwise find its predecessor:
procedure Remove(x: List; var xs: List)
require x is a node reachable from xs
if xs = x then
xs := x.next
else
p := xs
while p.next != x do
p := p.next
p.next := x.next
x.next := nilIn the search branch the loop invariant says that
p is before x in the original linked list, x is reachable from p.next, and no links have yet changed. The remaining link distance to x decreases at every advance, so membership of x guarantees a predecessor is found. Bypassing it removes exactly that cell, rather than an arbitrary equal-valued cell. Detaching x.next leaves a standalone removed node and preserves the relative order and object identities of all retained nodes.A sentinel node is a permanent header whose key is ignored and whose
next field holds the first data node. Every data node then has a predecessor, including the first, so unlinking always updates a predecessor's next field.function DelMin(hd: List): List
require hd != nil and hd.next != nil
bestPrev := hd
p := hd.next
while p.next != nil do
if p.next.x < bestPrev.next.x then
bestPrev := p
p := p.next
result := bestPrev.next
bestPrev.next := result.next
result.next := nil
return resultThe processed data prefix ends at
p. Its minimum is bestPrev.next, and bestPrev remains that node's actual predecessor. This loop invariant is initialized by the first node and preserved when a strictly smaller next node is found. The unprocessed suffix length is a loop variant. At exit, the final splice removes the first minimum in one uniform case. This is linked-list minimum extraction; it requires at least one data node, rather than treating the dummy header as an element.Repeatedly detach the minimum and append that very node to a separate output chain:
function Sort(xs: List): List
allocate dummy headers remaining and output
remaining.next := xs
output.next := nil
tail := output
while remaining.next != nil do
p := DelMin(remaining)
tail.next := p
tail := p
return output.nextThe loop invariant says that the output and remaining chains contain disjoint subsets of the original data nodes, together containing every original node exactly once. The output is nondecreasing, its final key is no larger than any remaining key, and
tail points to its final node, or to the dummy header when empty. Its outgoing link is nil because DelMin detaches the returned node. Appending the remaining minimum preserves all these properties; the remaining node count decreases by one.At exit the output is the complete sorted bag. This iterative selection sort preserves duplicate occurrences and, with first-minimum tie handling, their original relative order. It uses time and auxiliary nodes. “Increasing” here means nondecreasing when equal keys occur.
Articles by others on the same topic
There are currently no matching articles.