These for
-loops are among the first basic examples of formal correctness proofs of algorithms. They have different but equivalent termination conditions:
1 for ( int i = 0; i != N; ++i )
2 for ( int i = 0; i < N; ++i )
The difference becomes clear in the postconditions:
The first one gives the strong guarantee that
i == N
after the loop terminates.The second one only gives the weak guarantee that
i >= N
after the loop terminates, but you will be tempted to assume thati == N
.
If for any reason the increment ++i
is ever changed to something like i += 2
, or if i
gets modified inside the loop, or if N
is negative, the program can fail:
The first one may get stuck in an infinite loop. It fails early, in the loop that has the error. Debugging is easy.
The second loop will terminate, and at some later time the program may fail because of your incorrect assumption of
i == N
. It can fail far away from the loop that caused the bug, making it hard to trace back. Or it can silently continue doing something unexpected, which is even worse.
Which termination condition do you prefer, and why? Are there other considerations? Why do many programmers who know this, refuse to apply it?