Past exam of the year 1 of the computer science course of the University of Oxford / 2017 / Imperative programming (resit) / 2 / e

Maintain that all positive $h<\mathrm{lo}$ fail $r{h}^2\ge i^2$, while hi satisfies that inequality; its least satisfying integer lies in $[\mathrm{lo},\mathrm{hi}]$. Monotonicity of $r{k}^2$ in positive $k$ validates both updates. At exit the endpoints agree and identify exactly that least integer.

The loop variant hi-lo decreases on every iteration and is at least halved up to rounding. Starting with at most $i$ candidates therefore needs $O(\log (i+1))$ arithmetic operations, conventionally $O(\log i)$ for $i\ge 2$. For $i=1$ the loop is empty. The final upper-bound check proves the returned Boolean is the required membership answer.