|
|
|
|
|
|
|
sum = sum + count;
count++;
// Invariant:
// sum == 1 + 2 + + count-1
// && 2 <= count <= 11
} while (count <= 10) ;
// Assert:
// sum == 1 + 2 + + 10
// && count == 11 |
|
|
|
|
|
|
|
|
The first time control reaches the position of the loop invariant, sum equals 1 and count equals 2. Therefore, the invariant is true. (Notice that sum equals the sum of the integers from 1 up through 1there's just one number in this sum.) At the end of the second iteration, sum equals 3 (that is, 1+2) and count equals 3, so the invariant is again true. At the end of the tenth iteration, sum contains the sum of 1 through 10 and count equals 11. The invariant is still true. At this time, control exits the loop. Now let's verify that |
|
|
|
|
|
|
|
|
Invariant AND Termination condition(r) Postcondition |
|
|
|
|
|
|
|
|
(Remember that the right arrow, pronounced implies, is the logical implication operator.) We manipulate the assertions as follows. The loop invariant is |
|
|
|
|
|
|
|
|
(sum = 1 + 2 + + count-1) AND (2< count < 11) |
|
|
|
|
|
|
|
|
and the loop termination condition is |
|
|
|
|
|
|
|
|
The following sequence of implications leads us to the loop postcondition: |
|
|
|
|
|
|
|
|
(sum = 1 + 2 + + count-1) AND (2 < count <11) AND (count > 10)(r) |
|
|
|
|
|
|
|
|
(sum = 1 + 2 + + count-1) AND (count = 11)(r) |
|
|
|
|
|
|
|
|
(sum = 1 + 2 + + 10) AND (count = 11) |
|
|
|
|
|
|
|
|
Placing a loop invariant into a While loop (or a For loop) is complicated by the fact that its loop test is at the top, not the bottom. To locate the loop invariant just before the loop test, we need two copies of the invariant, one before the loop starts and one at the end of an iteration: |
|
|
|
|
|
|
|
|
// Invariant:
while ( )
{
.
.
.
// Invariant:
} |
|
|
|
|
|