|
|
|
|
|
|
|
Testing a program can be as challenging as writing it. To test a program, you have to step back, take a fresh look at what you've written, and then attack it in every way possible to make it fail. This isn't always easy to do, but it's necessary if your programs are going to be reliable. (A reliable program is one that works consistently and without errors regardless of whether the input data is valid or invalid.) |
|
|
|
|
|
|
|
|
To verify an algorithm, we use the loop invariant as a bridge between the statements that precede and follow the loop. We have to show that the invariant is true before entering the loop. If the loop is designed correctly, the invariant should still be true when the termination condition is reached. |
|
|
|
|
|
|
|
|
To show that the invariant is true before loop entry, we compare the current set of conditions (the postconditions from the preceding statements) with the invariant. If the invariant is a subset of the current conditions, then the loop is ready to start. If the invariant contains an assertion that has not been established, then something is missing in our preparations for executing the loop. Most often, the missing item is an initialization such as assigning a beginning value to a loop control variable or performing a priming read. |
|
|
|
|
|
|
|
|
Once we know that the invariant is true at loop entry, we must show that the invariant is true at the start of each iteration. We do this by walking through the body of the loop and determining the postcondition of each statement. Then we compare the postcondition of the last statement in the loop to the invariant. If any part of the invariant is not satisfied by these conditions, there is something wrong with the loop. Otherwise, we know that the invariant is true at the beginning of the next iteration. |
|
|
|
|
|
|
|
|
When the loop exits, its termination condition is true (that is, the While condition is false). The postcondition of the loop is, in part, the conjunction (logical AND) of the termination condition and the invariant. The postcondition also includes any conditions that existed before the loop that have not changed. |
|
|
|
|
|
|
|
|
Let's tie all this together with an example: summing the integers 1 through 10. |
|
|
|
|
|
|
|
|
// SumUp program
int main()
{
int sum;
int number;
sum = 0;
number = 1;
|
|
|
|
|
|