|
|
|
|
|
|
|
while (number <= 10)
{
sum = sum + number;
number++;
}
} |
|
|
|
|
|
|
|
|
To verify this program, we begin by determining the loop postcondition. When the loop finishes executing, here's what should be true: |
|
|
|
|
|
|
|
|
sum contains the sum of the integers from 0 through 10 AND
number equals 11 AND
The number of loop iterations executed equals 10. |
|
|
|
|
|
|
|
|
Now we have to do the following: |
|
|
|
|
|
|
|
|
1. Define the loop invariant. |
|
|
|
|
|
|
|
|
2. Show that the invariant is true before loop entry. |
|
|
|
|
|
|
|
|
3. Show that the invariant is true at the start of each iteration. |
|
|
|
|
|
|
|
|
4. Show that at loop exit the invariant is still true, the termination condition is true, and the AND of these two conditions implies that the postcondition is true. |
|
|
|
|
|
|
|
|
This is the loop invariant: |
|
|
|
|
|
|
|
|
sum contains the sum of the integers from 0 through number - 1 AND
1 <= number <= 11 AND
The number of loop iterations executed equals number - 1. |
|
|
|
|
|
|
|
|
At loop entry, the following conditions have been established: sum is equal to 0, and number is equal to 1. Comparing these conditions to the invariant, we see that sum is equal to number - 1; number is in the range 1 through 11; and the number of iterations executed is 0, which equals number - 1. |
|
|
|
|
|
|
|
|
Next, we walk through the loop body. The first statement adds the value of number to sum, so sum now contains the sum of the integers from 0 through number. The next statement increments number, which means that sum now contains the sum of the integers from 0 through number - 1. At the end of this iteration, number - 1 also equals the number of iterations. Because number cannot be greater than 10 at the start of an iteration, we also know that number cannot be greater than 11 at this point. So the invariant is true for the start of the next iteration. |
|
|
|
|
|
|
|
|
We can tell that the loop terminates correctly from the fact that number is initially less than 10 and is incremented in each loop iteration. So number eventually becomes greater than 10, and the loop will terminate. |
|
|
|
|
|
|
|
|
Finally, let's form the logical AND of the loop invariant and the termination condition: |
|
|
|
|
|