= Solution
Set aside the selected pivot at the end, <array partitioning> the other entries, then move the pivot to the separation index:
``
def partition(l: Int, r: Int): Int = {
require(0 <= l && l < r && r <= a.length)
def swap(i: Int, j: Int): Unit = {
val t = a(i); a(i) = a(j); a(j) = t
}
val chosen = bestIndex(l, r)
val x = a(chosen)
swap(chosen, r - 1)
var p = l
var j = l
while (j < r - 1) {
if (a(j) < x) {
swap(p, j)
p += 1
}
j += 1
}
swap(p, r - 1)
p
}
``
The <loop invariant> is $l\leq p\leq j\leq r-1$, $a[l,p)<x$, $a[p,j)\geq x$, and $a(r-1)=x$. The segment's <multiset> is unchanged and all entries outside it are unchanged. A low entry is swapped into the low segment; a high entry simply extends the high segment. The <loop variant> is $r-1-j$. At exit, exchanging the reserved pivot with `a(p)` gives \b[$a[l,p)<x$, $a(p)=x$, and $a[p+1,r)\geq x$]. The displaced value at the old pivot position was already at least $x$. Length one is handled by self-swaps and an empty loop. Duplicate pivot values belong to the high side. This costs $\Theta(r-l)$ time and $O(1)$ auxiliary space.
Back to article page
