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

First find a sign bracket by exponential search, then bisect that bracket without evaluating its endpoints again:

def floorRoot(): Int = {
  require(eval(0.0) < 0.0)
  var lo = 0
  var hi = 1
  while (eval(hi.toDouble) <= 0.0) {
    lo = hi
    require(hi <= Int.MaxValue / 2, "doubling bound exceeds Int range")
    hi *= 2
  }
  while (hi - lo > 1) {
    val mid = lo + (hi - lo) / 2
    if (eval(mid.toDouble) <= 0.0) lo = mid
    else hi = mid
  }
  lo
}

For the first while loop the loop invariant is $p(\mathrm{lo})\le 0$, with hi a positive power of two, and either $(\mathrm{lo},\mathrm{hi})=(0,1)$ or $\mathrm{hi}=2\mathrm{lo}$. Every previously tested power of two has nonpositive value. Let $t$ be the least nonnegative integer for which $p(2^t)>0$. It exists by the positive leading coefficient. If the current upper endpoint is $2^k$, a mathematical loop variant is $t-k$ while the guard holds; the next doubling decreases it by one. The first while loop's postcondition is $p(\mathrm{lo})\le 0<p(\mathrm{hi})$. The second while loop has exactly the invariant, variant and adjacent-integer postcondition established in part c.

There are $t+1$ evaluations at powers of two. If $t\ge 1$, the final bracket has width $2^{t-1}$ and takes exactly $t-1$ midpoint evaluations. Including the initial sign check, the total is $2t+1$ evaluations for $t\ge 1$, and two for $t=0$. Thus evaluation cost is $O(\log U)$ for the first positive dyadic bound $U=2^t$; it is not a claim about the first positive root of a polynomial when the polynomial is nonmonotone.

The mathematical argument uses unbounded integer endpoints and reliable signs. The guarded Int implementation requires the successful dyadic bound to fit in Int; otherwise it explicitly fails rather than wrapping to a negative bound. The coefficient assumptions alone cannot guarantee that a requested integer result fits a fixed-width type. Floating-point overflow or unreliable signs likewise need a wider or certified evaluator for a fully general implementation.