= Solution
The <loop invariant> in <binary long division> says exactly where the true <integer> quotient $Q=\lfloor x/y\rfloor$ lies:
$$
x=qy+r,\quad0\leq r<y2^j
\quad\Longrightarrow\quad
\boxed{q\leq Q<q+2^j.}
$$
Halving `p` proposes the midpoint `q+p` of this candidate interval. The comparison `r >= y*p` is equivalent to `(q+p)*y <= x`, so it decides whether the quotient is in the upper or lower half. Adding `p` chooses the upper half; leaving `q` unchanged chooses the lower half. Thus <binary long division> is <binary search> for the last <integer> satisfying $qy\leq x$, deciding the quotient's <binary numeral system> digits from most significant to least significant. The doubling loop first finds a power-of-two interval containing that quotient.
Back to article page
