Let be a saved mathematical copy of the original array. A precise postcondition for sorting isThe precondition is that
a is a non-null array of length . Its length and every unrelated object remain unchanged. The second clause preserves the array multiset, including all multiplicities; ordering alone would also permit overwriting the entire array with zeros. The saved is a specification device and need not be allocated by the implementation.Use three-way quicksort. Fix the pivot value before moving any entries, and group equal entries together so that none needs a recursive call. These helpers and the sorter belong inside an enclosing scope containing The array partitioning loop invariant iswith unclassified. Swaps preserve the segment's array multiset and leave all entries outside it unchanged. The loop variant decreases in every branch. When swapping an entry from the right into
a.def swap(i: Int, j: Int): Unit = {
val t = a(i); a(i) = a(j); a(j) = t
}
def split(l: Int, r: Int): (Int, Int) = {
// Pre: 0 <= l < r <= a.length.
val p = a(l)
var lt = l
var i = l
var gt = r
while (i < gt) {
if (a(i) < p) {
swap(lt, i)
lt += 1
i += 1
} else if (a(i) > p) {
gt -= 1
swap(i, gt)
} else {
i += 1
}
}
(lt, gt)
}
def quicksort(l: Int, r: Int): Unit = {
require(0 <= l && l <= r && r <= a.length)
if (r - l > 1) {
val (lt, gt) = split(l, r)
quicksort(l, lt)
quicksort(gt, r)
}
}
// Sort the whole array with quicksort(0, a.length).i, do not increment i, since the incoming entry still needs classification. At termination,Here the middle segment is nonempty because the original pivot occurs somewhere in the preserved array multiset. Both recursive segments therefore have length strictly smaller than . Mathematical induction on segment length proves that the two recursive calls sort their segments, and their ordering relative to the middle segment proves the complete sorting postcondition.There is no additional array. The call stack and returned boundary pairs still use auxiliary space. An all-equal input takes one linear scan and no nontrivial recursive calls, so its time complexity is for . Balanced partitions give time complexity; a fixed first pivot can still give on adversarial distinct inputs. The worst-case call stack has entries.
Reuse A useful loop invariant is that the pending segments are pairwise disjoint valid array segments of length at least two; the whole array multiset equals its original value; and every inverted pair of positions lies in a single pending segment. Explicitly, if and , some queued contains both and . Thus all ordering obligations are localized to queued segments.
split and swap, but replace recursive calls with a FIFO queue of unresolved segments. Enqueue only segments of length at least two.def quicksortLoop(): Unit = {
val work = scala.collection.mutable.Queue[(Int, Int)]()
if (a.length > 1) work.enqueue((0, a.length))
while (!work.isEmpty) {
val (l, r) = work.dequeue()
val (lt, gt) = split(l, r)
if (lt - l > 1) work.enqueue((l, lt))
if (r - gt > 1) work.enqueue((gt, r))
}
}Initially the only possible pending segment is the whole array. One array partitioning confines all its remaining inversions to its two child segments. Its equal middle segment is ordered, the left/middle/right boundaries have the correct ordering, and segments of length at most one cannot contain an inversion. Because array partitioning only permutes the selected segment's entries, it cannot create an inversion across a boundary that previously had no inversions. This proves preservation of the loop invariant.
The loop variant is the total pending lengthProcessing one segment removes from and adds at most , strictly less because . Thus is a nonnegative integer and decreases. At exit no pending segment exists, so no inversion exists:The FIFO queue itself can grow to pairs. The time complexity is that of the corresponding recursive quicksort, including linear behavior on equal input. Removing recursion does not make the worst-case time complexity linear or eliminate the work storage.
Articles by others on the same topic
There are currently no matching articles.