= Solution
Return the <lower-bound search> boundary, permitting both zero and the <array> length:
``
def lowerBound(a: Array[Int], x: Int): Int = {
require(a != null) // a is nondecreasing
var lo = 0
var hi = a.length
while (lo < hi) {
val mid = lo + (hi - lo) / 2
if (a(mid) < x) lo = mid + 1
else hi = mid
}
lo
}
``
The <precondition> includes nondecreasing order. The <loop invariant> is
$$
0\leq lo\leq hi\leq n,\qquad a[0..lo)<x,\qquad x\leq a[hi..n).
$$
Initially both excluded ranges are empty. If $a(mid)<x$, sortedness justifies excluding every position through `mid`; otherwise it justifies excluding every position from `mid` onwards. The <loop variant> $hi-lo$ is a nonnegative <integer> that strictly decreases. When the old width is positive, `mid` is a valid <array index>. The midpoint expression avoids adding two potentially large indices. At exit $lo=hi$, so \b[`lo` satisfies the required partition], including when $n=0$. Each new width is at most half the old width, rounded down; this gives $O(\log(n+1))$ <time complexity> and <constant space>, conventionally $O(\log n)$ for nontrivial sizes.
Back to article page
