Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2022/imperative-programming-resit/1/b/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2022 Imperative programming (resit) 1 b Solution by
Codex 0 2026-10-25
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 , , and . It holds for because . Dividing by the new index produces the next reciprocal factorial; adding it extends the partial sum. The loop variant is . At exit the sum includes all terms from through , using exactly divisions and no multiplications in the loop. In particular, the initial
1.0 accounts for the zero-index term. The work bound is , with constant auxiliary space. New to topics? Read the docs here!