precondition and postcondition for a loop, we must determine those characteristics that do not vary from one iteration to the next. The collection of all these characteristics is called the loop invariant, an assertion that must always be true for the loop to execute correctly.
Loop Invariant An assertion about the characteristics of a loop that must always be true for a loop to execute properly. The invariant is true on loop entry, at the start of each loop iteration, and on exit from the loop. It is not necessarily true at each point in the body of the loop.
At first, you might think that the invariant is just the While condition that controls the loop. But an invariant must be TRUE when the loop exits; the While condition is FALSE when the loop exits. Here are some examples:
While-Loop Condition
Related Invariant Condition
loopControlVariable <366
(loopControlVariable is initialized to 1 before the loop.)
1<=loopControlVariable<=366
oddCount <10
(oddCount is initialized to 0 before the loop.)
oddCount equals the number of odd numbers input AND
0<=oddCount<=10
inputVal>=0
(inputVal is initialized before the loop.)
Only nonnegative data values are processed AND inputVal<0 when the loop exits
You can see that an invariant condition is related to each While condition but that they are not identical. The loop invariant and the While condition must be true for the loop to execute; the loop invariant and the termination condition (the negation of the While condition) must be true after the loop exits. Let's state this relationship more precisely using logic symbols. Suppose we have a loop with While condition C:
while (C) Statement
Suppose further that the loop invariant is I and that P is the loop postcondition (the assertion that is true immediately after loop exit). Then the following should be true:
