Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Imperative programming / 2 / a

Use three-way array partitioning around a saved pivot value:

procedure Partition(var a; l, r; var m, n)
    x := a[Pivot(a,l,r)]
    m := l
    k := l
    n := r
    while k < n do
        if a[k] < x then
            swap(a[k], a[m])
            m := m+1
            k := k+1
        else if a[k] > x then
            n := n-1
            swap(a[k], a[n])
        else
            k := k+1

Assume a total ordering on the element keys. The loop invariant partitions the original segment intowith $l\le m\le k\le n\le r$ and the segment's multiset unchanged. A smaller entry exchanges with the first equality position; the displaced equal entry is accounted for when both indices advance. A greater entry exchanges with the last unclassified position, so k must stay to inspect the incoming entry. The loop variant $n-k$ decreases by one in every branch.

At termination the equality interval is $[m,n)$. It is nonempty because the pivot value came from the segment and swaps preserve the bag. The stronger strict outer-region conditions therefore imply the requested overlapping inequalities $a[l..n)\le x\le a[m..r)$ and $l\le m<n\le r$. Storing the pivot value avoids following an array position whose contents may move.