|
|
|
|
|
|
|
To avoid duplicating the invariant this way, we include only one copy at the top of the loop body, along with the remark prior to test. This remark is a reminder that the invariant is logically, if not physically, located just before the loop test. Here is a While loop to sum the integers 1 through 10: |
|
|
|
|
|
|
|
|
sum = 0;
count = 1;
while (count <= 10)
{
// Invariant (prior to test):
// sum == 1 + 2 + + count-1
// && 1 <= count <= 11
sum = sum + count;
count++;
} |
|
|
|
|
|
|
|
|
In comparing this example to the Do-While version, there are two things to notice. First, the two versions use different invariants for count. In the Do-While loop, the lower limit is 2 because count has already been incremented by the time the invariant is reached. In the While loop version, the invariant is first encountered before the loop begins. At that moment, count equals 1. |
|
|
|
|
|
|
|
|
The second thing to notice is that the invariant for sum seems to be wrong the first time the invariant is encountered. Before the loop begins, the assertion is |
|
|
|
|
|
|
|
|
Is this a true assertion? The answer is yes, and here's why. The assertion, if written out in full, is actually this: For all integers in the range 1 through 0 in increasing order, sum is the sum of these integers. Because there aren't any integers that satisfy the For all part, the assertion is trivially true. Here's another example of a loop invariant that is trivially true before the first execution of the loop body: |
|
|
|
|
|
|
|
|
for (i = 1; i <= 50; i++)
// Invariant (prior to test) :
// The values 1, 2, , il have been output
// && 1 <= i <= 51
cout << i << endl; |
|
|
|
|
|
|
|
|
After i has been initialized to 1 but before the loop test occurs, the assertion |
|
|
|
|
|
|
|
|
The values 1,2, , 0 have been output |
|
|
|
|
|