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

The algorithmic intention is exponentiation by squaring to compute $x^n$ for $n\ge 0$. With exact arithmetic, its loop invariant isInitially result = 1, y = x, and i = n. For an even integer $i=2q$, squaring y and replacing i by $q$ preserves the product. For an odd integer $i=2q+1$, first multiply result by y; then $(resulty)(y^2{)}^q=result{y}^{2q+1}$. The nonnegative loop variant i decreases by halving whenever positive. At exit $i=0$, so the loop invariant yields result = x^n. There are $O(\log (n+1))$ multiplication steps.

Two qualifications are essential for the actual source. There is no requirement that n be nonnegative: for every n <= 0 the printed function simply returns 1.0. Also, var y = x infers Int, so y *= y uses wrapping integer arithmetic, while the accumulator uses floating-point arithmetic. For example, anotherfunc(50000, 2L) returns -1794967296.0, rather than 2500000000.0. An exact-power loop invariant cannot prove a false claim about that execution.

More precisely, for positive n, after $k$ iterations the remaining exponent is $\lfloor n/2^k\rfloor$, and the Int base is the signed 32-bit representative of $x^{2^k}$ modulo $2^{32}$. The accumulator multiplies those signed representatives for the set bits of n, in increasing bit order, with a floating-point rounding after each multiplication. This describes the actual code even when the intended power law fails. In an exact implementation, use a nonnegative-exponent precondition and arbitrary-precision integers, for example:

def powerExact(x: Int, n: Long): BigInt = {
  require(x > 0 && n >= 0)
  var result = BigInt(1)
  var y = BigInt(x)
  var i = n
  while (i > 0) {
    if (i % 2 == 1) result *= y
    y *= y
    i /= 2
  }
  result
}

The displayed loop invariant applies exactly to this version. It performs logarithmically many arbitrary-precision multiplications; their bit cost grows with operand size, so that statement is not an $O(\log n)$ bit-complexity bound. Merely making the accumulator a Double does not widen the separate Int base variable.