= Solution
Represent zero by one digit. Since `int_part` is nonnegative, a logical right shift is exactly <integer division> by two:
``
var digits = 1
var scratch = int_part
while (scratch >= 2) {
scratch = scratch >>> 1
digits += 1
}
``
The <loop invariant> is $digits\geq1$ and $scratch=\lfloor int\_part/2^{digits-1}\rfloor$; for positive `int_part`, also $scratch\geq1$. The <loop variant> is `scratch`, strictly decreased whenever the guard holds. On exit, a positive input has $scratch=1$, yielding $2^{digits-1}\leq int\_part<2^{digits}$. Therefore \b[`digits` is the required width], including width one for zero. Shifting avoids an explicit multiplication or division in the code. This uses the supplied assumption that `dec.toInt` really is the mathematical floor; saturating or invalid conversions are not covered by that assumption.
Back to article page
