|
|
|
|
|
|
|
cin >> age;
// Invariant:
// age has been input
// && For all values of age prior to
// current value, age <= 0
} while (age <= 0); |
|
|
|
|
|
|
|
|
After the loop terminates, the conjunction of the termination condition and the invariant yields the postcondition |
|
|
|
|
|
|
|
|
(age > 0) AND (For all values of age prior to the current value, age < 0) |
|
|
|
|
|
|
|
|
Writing loop invariants as program comments is not always easy to do. Sometimes an invariant consists of 15 or 20 separate assertions. Although these assertions may all be important when you design and verify the loop, it's not practical to include them all as comments. For documentation purposes, what is important is to summarize concisely the task accomplished by the loop, mentioning values of key variables such as counters, summing variables, and input or output variables. Using mathematical notation wherever possible helps keep the comments brief and precise. And remember to express an invariant as an assertion, not as a general informational comment. Assertions don't look like This loop will do such-and-such or This loop does so-and-so. An assertion is a truth-valued statementone that is either true or false (true, one hopes). |
|
|
|
|
|
|
|
|
One final remark about loop invariants: If you write an infinite loop with break statements to allow multiple exits from the loop, you need a different loop invariant for each of the exit points. The loop invariants are all bound to be different because the state of the program changes between any two exit points. The prospect of creating four or five different invariants for a given loop may keep you from becoming too casual about using break statements! |
|
|
|
|
|
|
|
|
Problem-Solving Case Study The Rich Uncle |
|
|
|
|
|
|
|
|
Problem: Your rich uncle has just died, and in his desk you find two wills. One of them, dated several months ago, leaves you and your relatives a substantial part of his fortune; the other, dated last week, gives it all to his next-door neighbor. Being suspicious that the second will is a forgery, you decide to write a program to analyze writing style in order to compare the wills. The program reads and prints alphanumeric characters from a file |
|
|
|
|
|
