= Doubling-loop ceiling logarithm
{title2=$i=\lceil\log_2 x\rceil$}
For positive $x$, start at $i=0,y=1$ and repeatedly increment $i$ and double $y$ while $y<x$. In exact <integer arithmetic>, the <loop invariant> $y=2^i$ together with $i=0$ or $2^{i-1}<x$ yields $i=\lceil\log_2x\rceil$ at exit. For fixed-width arithmetic, this proof requires every useful doubling to be representable. A signed 32-bit doubling variable becomes negative at $2^{31}$ and then zero, so the loop need not terminate for inputs above $2^{30}$. Widening the variable to a signed 64-bit type repairs the algorithm for positive 32-bit inputs.
Back to article page
