 Binary long division

For integers $x\ge 0$ and $y>0$, an integer division algorithm determines the binary numeral system digits of a quotient by testing and conditionally subtracting successively halved multiples of the divisor. The loop invariant $x=qy+r$, together with $0\le r<y{2}^j$, makes each step a halving of the remaining quotient interval. Start with $q=0,r=x$ and $j$ large enough that $x<y{2}^j$. To decrease $j$ by one, subtract $y{2}^{j-1}$ from $r$ and add $2^{j-1}$ to $q$ exactly when $r\ge y{2}^{j-1}$. Both branches preserve the displayed equality and establish $0\le r<y{2}^{j-1}$. When $j=0$, the quotient and remainder conditions hold.