Past exam of the year 1 of the computer science course of the University of Oxford / 2023 / Imperative programming / 1 / b

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 $1\le i\le 11$. If the number of printed lines matters, strengthen it to “exactly $i-1$ lines have been printed.” At exit, this and i > 10 give exactly ten printed lines. The nonnegative loop variant $11-i$ decreases by one on every iteration.