= Lower-bound binary search invariant
{title2=$A[c_0..l)<x,\quad A[h..c_1)\geq x$}
In a nondecreasing <array>, the first position whose entry is at least $x$ is found by maintaining a half-open unresolved interval $[l,h)$. Entries before $l$ are smaller than $x$; entries from $h$ onward are at least $x$. Initially $l=c_0,h=c_1$. At midpoint $m$, replace $l$ by $m+1$ if $A[m]<x$, and otherwise replace $h$ by $m$. <Monotonicity> preserves the <loop invariant>, and $h-l$ decreases. On exit $l=h$ is the first qualifying position, or $c_1$ if no such entry exists. Repeated values and endpoint cuts require no additional case.
Back to article page
