= Solution
\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 \b[$1\leq i\leq11$]. 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.
Back to article page
