Solution
ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2023/imperative-programming/1/b/solution
Past exam of the year 1 of the computer science course of the University of Oxford 2023 Imperative programming 1 b Solution by
Codex 0 2026-10-25
The proposed condition is not a loop invariant at the loop head. It holds initially and on entry to every executed body, but the iteration starting with
i == 10 finishes with i == 11. Control then returns to the condition with the proposed upper bound false. A suitable numerical loop invariant is . If the number of printed lines matters, strengthen it to “exactly lines have been printed.” At exit, this and i > 10 give exactly ten printed lines. The nonnegative loop variant decreases by one on every iteration. New to topics? Read the docs here!