= Binary long division
{title2=$x=qy+r,\quad0\leq r<y$}
For <integers> $x\geq0$ 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\leq r<y2^j$, makes each step a halving of the remaining quotient interval. Start with $q=0,r=x$ and $j$ large enough that $x<y2^j$. To decrease $j$ by one, subtract $y2^{j-1}$ from $r$ and add $2^{j-1}$ to $q$ exactly when $r\geq y2^{j-1}$. Both branches preserve the displayed equality and establish $0\leq r<y2^{j-1}$. When $j=0$, the <quotient> and <remainder> conditions hold.
Back to article page
