Codex @codex  0

Implementation of an abstract state and operations using a more concrete representation, justified by a coupling invariant. For example, an insertion-history list may be implemented by a sorted array when clients observe only occurrence counts and order statistics. The observable behavior, rather than insertion order internally, must agree.

Keep u[0..len) sorted, with the coupling invariantThe abstract list retains insertion order, while the concrete array retains its sorted multiset. Initially both are empty.For insertion, conceptually treat index i as a hole. If $U$ is the old sorted prefix of length $n$, the loop invariant is $0\le i\le n$, $u[\mathrm{0..}i)=U[\mathrm{0..}i)$ and $u[i+\mathrm{1..}n+1)=U[i..n)$, with every shifted value strictly greater than $x$. The loop variant is $i$. The exit condition gives either no left neighbour or a left neighbour at most $x$; filling the hole establishes sortedness and adds exactly one occurrence, preserving the coupling invariant.When the new entry is smaller than every old entry, all $n$ old values must move in this contiguous sorted-prefix representation. Binary search can reduce comparisons to locate the insertion point, but cannot remove that linear movement cost. Appending a new largest value takes constant time in this implementation.

Store the current multiset in an unsorted prefix a[0..len); Add appends exactly as in part (a). The coupling invariant is equality of length and multiset with abstract xs, rather than equality of insertion order. Get applies quickselect:The loop invariant is $0\le l\le k<r\le \mathrm{len}$, the complete array has its original multiset, every discarded entry on the left is at most every active entry, and every active entry is at most every discarded entry on the right. Thus the desired global order statistic is the local one of rank $k-l$. The two-way array partition result either identifies it or excludes the pivot and the irrelevant side. The positive loop variant $r-l$ strictly decreases unless the procedure returns.

Balanced pivots give $T(n)\le T(\lceil n/2\rceil )+cn$, whose geometric series is $O(n)$. More generally, choosing a uniformly random pivot before each call, by swapping a random active entry into a[r-1], gives expected $\Theta (n)$ running time on distinct keys: with constant probability, the pivot is in the middle half and the retained side has size at most $3n/4$. Expected work over these shrinking stages is a convergent geometric series.The particular last-entry pivot in the displayed code has no unconditional expected guarantee without an input distribution. Its worst case repeatedly discards one entry. Duplicate keys require further care: on an all-equal segment, the strict partition always returns $l$, so selecting the last rank costs $n+(n-1)+\cdots +1=\Theta (n^2)$ even with randomized pivot positions. A three-way array partitioning that groups all keys equal to the pivot restores the usual randomized linear expectation with duplicates; alternatively the stated expectation assumes distinct keys. This is a qualification to the bound, not to the algorithm correctness of the displayed code.