Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Imperative programming (resit) / 1 / a / i

Use a Double base so that the reciprocal is not truncated by integer division. Repeated multiplication gives the requested linear-work approximation to Euler's number.

def eaLinear(n: Int): Double = {
  require(n > 0)
  val base = 1.0 + 1.0 / n.toDouble
  var i = 0
  var result = 1.0
  while (i < n) {
    result *= base
    i += 1
  }
  result
}

In exact arithmetic over the real numbers, the loop invariant is $0\le i\le n$ and $result=bas{e}^i$. It holds initially, one multiplication establishes the next exponent, and at exit $i=n$ gives the specified power. The nonnegative loop variant is $n-i$. There are exactly $n$ loop multiplications, hence $\Theta (n)$ in asymptotic analysis, and one division to form the base. With floating-point arithmetic, the invariant describes the intended exact result; the actual output has the corresponding rounding errors.