Loop Invariants with Breaks

Question

I am trying to understand how loop invariants interact with breaks. CLRS 3e (pg19) describes a loop invariant as requiring that

If it is true before an iteration of the loop, it remains true before the next iteration.

So given the following trivial loop

for i = 1 to 5
    if i == 3 then break

Would it be fair to say that i < 4 is an invariant property of the loop? The argument being that, since the loop terminates at the break statement, there is no iteration after that property is violated.

Answer 1

Yes, that would be an invariant, for precisely the reason you’ve mentioned. Whether it’s a useful invariant is a separate question that depends on what you’re trying to prove.