|
|
|
|
|
|
|
is trivially true because there are no integers in this range. The second part of the invariant is also truenamely, that i is in the range 1 through 51, inclusive. The first loop iteration prints the value 1 and increments i to 2. Prior to the loop test, the invariant is true; the value 1 has been output, and i is in the stated range. On the final iteration, the value 50 is printed and i becomes 51. Prior to the loop test, you can see that the invariant is true. After the loop test, control exits the loop and the invariant is still true. |
|
|
|
|
|
|
|
|
When loops don't use counters, loop invariants are harder to write. For example, what is the invariant for the following loop? |
|
|
|
|
|
|
|
|
do
{
cout << Enter your age: ;
cin >> age;
} while (age <= 0) ; |
|
|
|
|
|
|
|
|
This loop continues to iterate as long as age < 0. We might be tempted to write the invariant this way: |
|
|
|
|
|
|
|
|
do
{
cout << Enter your age: ;
cin >> age;
// Invariant (WRONG) :
// age has been input
// && age <= 0
} while (age <= 0); |
|
|
|
|
|
|
|
|
This invariant is true for every iteration except the final iteration, which occurs when the user finally types a positive number. Suppose that the user types 5 as the input value. Immediately after the input statement and before the loop test, the invariant is false. This is not the correct invariant. |
|
|
|
|
|
|
|
|
With loops that input data and immediately test the data in the loop condition, there are two keys to expressing a loop invariant correctly. The first is to think about the history of the loopwhat has happened so far since the loop began. The second is to exclude the current input value from any claim about its value. In the above loop, we can't claim that age is negative or 0 or positive immediately after reading it inthat's for the loop test to determine. Here is a reasonable way to write the invariant for the above loop: |
|
|
|
|
|
|
|
|
do
{
cout << Enter your age: ;
|
|
|
|
|
|