For a finite acyclic linked list define the node sequence, retaining software object identities, byThen scan without changing any links:
def findMin(first: Node): Node = {
require(first != null)
var best = first
var cursor = first.next
while (cursor != null) {
if (cursor.datum < best.datum) best = cursor
cursor = cursor.next
}
best
}At each while loop head, write . The loop invariant says is nonempty,
best belongs to , and its datum is no larger than that of every node in . Initially contains only first; comparing the next node extends the processed string prefix and preserves minimality. The loop variant strictly decreases. At exit the whole list is processed, so the returned reference identifies a minimum node. Ties retain the earliest minimum. Time is linear in the number of nodes and auxiliary space is constant.A sentinel node supplies a permanent predecessor for the first real node. Inserting or deleting at the front then uses the same
predecessor.next update as an interior operation. Its datum is not a multiset element: the chosen extreme integer is merely unused sentinel data.A representation invariant requires a nonnull fixed header, a finite acyclic chain starting at
bagHeader.next, and exclusion of the header from that chain. Each node identity occurs once, although different nodes may have equal data. Representation links are owned by the implementation, so outside mutation cannot alter them unexpectedly.The abstraction function counts occurrences:This yields nonnegative multiplicities and finite support. Initialization with a null successor gives the empty multiset. Excluding the sentinel is essential even when a real item equals its datum.
The precondition is
n != null and , using node identity rather than datum equality. Search for its predecessor:def delete(n: Node): Unit = {
var previous = bagHeader
while (previous.next ne n) {
previous = previous.next
}
previous.next = n.next
n.next = null
}The loop invariant states that
previous is the header or a preceding real node, and . The loop variant is the number of links from previous to n minus one. The precondition guarantees that this search reaches the predecessor before a null dereference. Replacing its successor by n.next bypasses exactly the requested node; clearing the removed node's link detaches it for later reuse. The order and identities of every other node remain unchanged. In abstract terms, only the multiplicity of n.datum decreases, by one. The worst-case time is linear; the pointer modification itself is constant-time.Check that at least one real node exists, then compose the two helpers:
def deleteMin(): Int = {
require(bagHeader.next != null, "bag is empty")
val smallest = findMin(bagHeader.next)
val answer = smallest.datum
delete(smallest)
answer
}The precondition check makes
findMin applicable. Its result belongs to the real-node sequence, satisfying delete's precondition. Consequently one minimum value is returned and exactly one occurrence is removed; duplicates remain as distinct nodes. Saving the datum before deletion also separates the return value from subsequent link mutation. Two linear traversals still give time for a multiset containing nodes, with constant auxiliary space.Let and describe the entry state. The postcondition is: the multiset is empty; the returned chain is sorted nondecreasingly; its node sequence is a permutation of . 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 in general, from successive scans of lengths , and it uses constant auxiliary space: it relinks original nodes instead of allocating a new node for each item.
Articles by others on the same topic
There are currently no matching articles.