|
|
|
|
|
|
|
where the symbol (r) is the logical implication operator and is pronounced implies. In other words, we want to ensure that if the invariant is true and the While condition is false, then the loop postcondition is true. |
|
|
|
|
|
|
|
|
The loop invariant usually consists of other conditions as well as those related to the While condition. For example, it typically includes the ranges of all the variables used in the loop and the status of any files. |
|
|
|
|
|
|
|
|
To create the invariant, we begin with the loop postconditionour answer to the last question on the loop design checklist (What is the state of the program on exiting the loop?)because it forces us to determine the final condition of the variables and files. Then we work backward, answering the other questions on the checklist. |
|
|
|
|
|
|
|
|
Let's write the invariant for the outer loop in the Invoice program. We begin with the part of the invariant associated with totalAmount. We know that on loop exit, totalAmount contains the sum of all the individual item amounts. Then we look at how the process is initialized and updated. Here's the related invariant condition: |
|
|
|
 |
|
|
|
|
totalAmount >= 0 AND
At the start of each iteration, totalAmount equals the total of all the values of amount that have been computed. |
|
|
|
|
|
|
|
|
In the same way, we look at the termination condition, initialization, and update of totalUnits to determine the portion of the invariant that relates to it: |
|
|
|
|
|
|
|
|
totalUnits >= 0 AND
At the start of each iteration, totalUnits equals the sum of all the values of quantity that have been input so far. |
|
|
|
|
|
|
|
|
Here are the invariant conditions for the other variables and the input file: |
|
|
|
|
|
|
|
|
price either is undefined or contains a floating point value AND
price contains the item price input in the most recently completed iteration. |
|
|
|
|
|
|
|
|
amount either is undefined or contains a floating point value AND
amount contains the product quantity * price calculated in the most recently completed iteration. |
|
|
|
|
|
|
|
|
quantity contains the most recently input quantity ordered of an item. |
|
|
|
|
|
|
|
|
counter either is undefined or contains the value 31. |
|
|
|
|
|
|
|
|
inputChar either is undefined or contains the last character of the item description input in the previous iteration. |
|
|
|
|
|
|
|
|
blank either is undefined or contains the character between the quantity and the item description input in the previous iteration. |
|
|
|
|
|
|
|
|
The reading marker in inFile is positioned just after the most recent quantity input. |
|
|
|
|
|
|
|
|
In addition to the status of variables and files, most programs contain some general invariant conditions. For example: |
|
|
|
|
|