Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 2 / c

Under exact integer arithmetic, the intended result is $\lceil {\log }_{2}x\rceil$, using the ceiling function. A sufficient loop invariant isInitially $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\ge x$. If $i=0$, positivity of $x$ forces $x=1$; otherwise $2^{i-1}<x\le 2^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.

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\le x\le 2^{30}$. Scala documents Int as a signed 32-bit value equivalent to Java's primitive int.^[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\le 2^{31}$, safely within Long. The same loop invariant proves total correctness without the overflow gap.