Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Imperative programming / 1 / c / Solution

Maintain opposite signs at the endpoints, rather than assuming that the polynomial is monotone:

def floorRoot(X: Int): Int = {
  require(X > 0 && eval(0.0) <= 0.0 && eval(X.toDouble) > 0.0)
  var lo = 0
  var hi = X
  while (hi - lo > 1) {
    val mid = lo + (hi - lo) / 2
    if (eval(mid.toDouble) <= 0.0) lo = mid
    else hi = mid
  }
  lo
}

The loop invariant is $0\le \mathrm{lo}<\mathrm{hi}\le X$ and $p(\mathrm{lo})\le 0<p(\mathrm{hi})$. Both branches preserve those signs, even when there are other roots of a polynomial or sign reversals elsewhere. When the interval width exceeds one, the midpoint is strictly between its endpoints, so the positive integer loop variant hi - lo strictly decreases. On exit hi == lo + 1, giving the required postcondition $p(\mathrm{lo})\le 0<p(\mathrm{lo}+1)$. Continuity establishes a root of a polynomial between those adjacent integers, possibly at the left endpoint.

The width is at most halved with rounding upwards, so there are at most $\lceil {\log }_{2}X\rceil$ midpoint evaluations, plus two endpoint evaluations in the precondition check. The midpoint expression avoids adding two large endpoints. The explicit positive upper-bound precondition supplies the interval order assumed in the question. For the literal computed-eval contract, the same proof holds provided evaluated midpoints are not NaN; identifying its bracket with the real polynomial additionally requires trustworthy evaluation signs.