= Solution
Maintain the required boundary between entries strictly above the target and entries at most the target:
``
def search(u: Array[Int], z: Int): Boolean = {
var a = 0
var b = u.length
while (a < b) {
val middle = a + (b - a) / 2
if (u(middle) > z) a = middle + 1
else b = middle
}
a < u.length && u(a) == z
}
``
The full <invariant> is $0\leq a\leq b\leq n$, every entry before $a$ is greater than $z$, and every entry at or after $b$ is at most $z$. The <array> remains unchanged. Descending order justifies each update: if the middle value is greater, all earlier values are greater too; otherwise all values from the middle onward are at most the target.
The nonnegative <loop variant> $b-a$ strictly decreases, with each update retaining at most half the old candidate length. On termination $a=b$, which is the first index whose value could be at most $z$. Equality at that index is therefore necessary and sufficient for presence. <Short-circuit evaluation> makes the final test safe when $a=n$, including the empty-<array> case. The time is \b[$O(\log(n+1))$], using constant <auxiliary space>.
Back to article page
