= 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 \b[$0\leq\mathrm{lo}<\mathrm{hi}\leq X$ and $p(\mathrm{lo})\leq0<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> \b[$p(\mathrm{lo})\leq0<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_2X\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.
Back to article page
