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

Maintain the reciprocal factorial term rather than calculating large factorials separately:

def eb(n: Int): Double = {
  require(n > 0)
  var i = 0
  var term = 1.0
  var sum = 1.0
  while (i < n) {
    i += 1
    term /= i.toDouble
    sum += term
  }
  sum
}

The exact-arithmetic loop invariant is $0\le i\le n$, $term=1/i!$, and $sum={\sum }_{k=0}^{i}1/k!$. It holds for $i=0$ because $0!=1$. Dividing by the new index produces the next reciprocal factorial; adding it extends the partial sum. The loop variant is $n-i$. At exit the sum includes all terms from $0$ through $n$, using exactly $n$ divisions and no multiplications in the loop. In particular, the initial 1.0 accounts for the zero-index term. The work bound is $O(n)$, with constant auxiliary space.