= Solution
Under exact <integer arithmetic>, the intended result is \b[$\lceil\log_2 x\rceil$], using the <ceiling function>. A sufficient <loop invariant> is
$$
i\geq0,\qquad y=2^i,\qquad i=0\ \lor\ 2^{i-1}<x.
$$
Initially $i=0,y=1$, and the final disjunction is true. If the guard holds, the old value $y=2^i$ is below $x$. Incrementing `i` and doubling `y` therefore preserves $y=2^i$ and makes the new lower bound $2^{i-1}<x$ true. At exit $y\geq x$. If $i=0$, positivity of $x$ forces $x=1$; otherwise $2^{i-1}<x\leq2^i$. Both cases establish the claimed <postcondition>. Doubling eventually reaches or exceeds any fixed positive $x$, proving <algorithm termination> in this arithmetic model. This is the <doubling-loop ceiling logarithm> argument.
\b[The printed Scala implementation is not correct for its entire stated `Int` domain.] Its `y` is an `Int`. For $x>2^{30}$, it reaches $y=2^{30}$, wraps to $-2^{31}$ on the next doubling, then becomes zero and stays zero. The guard remains true forever. The <loop invariant> above is valid for the printed code only when $1\leq x\leq2^{30}$. Scala documents `Int` as a signed 32-bit value equivalent to Java's primitive `int`.<Scala Int API documentation>[Scala 2.13.16, class Int: signed 32-bit representation]{ref}
A corrected implementation for every positive `Int` input widens the doubling variable before any multiplication:
``
def ceilingLog2(x: Int): Int = {
require(x > 0)
var i = 0
var y = 1L
while (y < x.toLong) {
i += 1
y *= 2L
}
i
}
``
Now at most 31 iterations are needed and $y\leq2^{31}$, safely within `Long`. The same <loop invariant> proves <total correctness> without the overflow gap.
Back to article page
