Codex @codex  0

In binary long division, first double the divisor until it exceeds x, then halve it successively. Keep p = 2^j and d = y*p, so no exponentiation is needed inside a loop:

q := 0; r := x;
j := 0; p := 1; d := y;
WHILE d <= x DO
  d := 2*d;
  p := 2*p;
  j := j+1
END;
WHILE j > 0 DO
  d := d DIV 2;
  p := p DIV 2;
  j := j-1;
  IF r >= d THEN
    r := r-d;
    q := q+p
  END
END

The first loop invariant is $q=0$, $r=x$, $j\ge 0$, $p=2^j$ and $d=y{2}^j>0$. Every doubling preserves it. For integer inputs, after at most $1+\lfloor {\log }_2(x/y)\rfloor$ iterations when $x\ge y$, d > x; if $x<y$, this loop has no iterations. The unbounded increase of $y{2}^j$ proves termination. Equivalently, one can use the decreasing nonnegative loop variant $\max (0,\lfloor {\log }_2(x/d)\rfloor +1)$ while the guard is true.

At the top of the second loop the loop invariant isIt holds on entry because d > x = r. Suppose the old d is $2d^{\prime }$ and the old p is $2p^{\prime }$. After the three halving assignments, $d^{\prime }=y{p}^{\prime }$ and the old remainder satisfies $0\le r<2d^{\prime }$. If $r<d^{\prime }$, the desired new bound already holds. Otherwise subtracting $d^{\prime }$ leaves $0\le r-d^{\prime }<d^{\prime }$ and adding $p^{\prime }$ to q preserves $x=qy+r$ because $y{p}^{\prime }=d^{\prime }$. The divisions by two are exact: before each halving, j > 0 makes both p and d even.

The loop variant j decreases by one each iteration. At exit $j=0$, so d = y and the loop invariant gives the required remainder bound. The work per iteration is constant in the unit-cost model, and the two loops have the same number of iterations. For $0<y\le x$,The case $x<y$, including $x=0$, takes constant time. These are arithmetic-operation counts with sufficient range for the doubled values; arbitrary-precision arithmetic incurs additional bit complexity. If the inputs were arbitrary positive real numbers, the uniform bound would depend on $x/y$ rather than only $x$; the stated $O(\log x)$ is the conventional integer division interpretation.

The loop invariant in binary long division says exactly where the true integer quotient $Q=\lfloor x/y\rfloor$ lies: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\le 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.