Many program errors occur within loops, so it is important to verify that loops are correct. One verification method is to trace the loop's execution for a variety of different sets of data, making sure that the loop always terminates and that it produces the correct results, even when zero iterations are performed. To help us verify that a loop works properly, we can use special comments, called assertions and loop invariants, within a loop body. In this section, we introduce some principles of loop verification that will help you in loop design.
A critical part of loop verification is to document the loop using assertions,
which are logical statements that are always true. An assertion should be
placed just before the loop body (after the WHILE statement), and
another one should be placed just after the loop exit.
The assertion that precedes the loop body is called the loop
invariant. Because the loop invariant is an assertion, it must always be
true, even before loop repetition begins. Like the WHILE
condition, the loop invariant is evaluated just before each repetition of the
loop body. The execution of the loop body may change the value of the
WHILE condition from true to false (e.g., just before the loop
exit); however, the value of the loop invariant must remain true. In other
words, the execution of the loop body must not change the value of the loop
invariant.
The loop from Program 6.3 is rewritten below using assertions. Remember that these assertions are inserted to help you or another human reader verify the correctness of the loop. Since assertions are just comments, they are ignored by the Ada compiler.
-- Cut the distance between the worm and the apple by the worm's
-- body length until the worm is close enough to bite the apple
Distance := InitialDist;
WHILE Distance > WormLength LOOP
-- invariant:
-- Distance <= InitialDist and
-- Distance in pass i is Distance in pass i-1
-- less the worm's length (for i > 1)
Ada.Text_IO.Put(Item => "The distance is ");
Ada.Float_Text_IO.Put
(Item => Distance, Fore => 4, Aft => 2, Exp => 0);
Ada.Text_IO.New_Line;
Distance := Distance - WormLength; -- reduce Distance
END LOOP;
-- assert: Distance <= WormLength
The
invariant and the assertion following the loop summarize all we know about the
loop, and they are similar to our earlier observations:
Distance must always be less than or equal to
InitialDist.
Distance is reduced by the
worm's body length.
Distance must be less than or equal to the worm's body length
just after loop exit.
Example 6.10 The sentinel-controlled loop in Example 6.8 is rewritten below using assertions. Compare the loop invariant with the statements below that summarize the loop properties.
Sum is the sum of all scores read so far.
Score is the sentinel just after loop exit.
Sum := 0;
Ada.Text_IO.Put (Item => "When done, enter -1 to stop.");
Ada.Text_IO.New_Line;
Ada.Text_IO.Put (Item => Enter the first score > ");
Ada.Integer_Text_IO.Get (Item => Score);
WHILE Score /= Sentinel LOOP
-- invariant: Sum is the sum of all scores read
-- and no prior score was the sentinel
Sum := Sum + Score;
Ada.Text_IO.Put ("Item => Enter the next score > ");
Ada.Integer_Text_IO.Get (Item => Score);
END LOOP;
-- assert: Score is Sentinel and Sum is the sum of all scores
Some computer scientists use loop invariants for loop design as well as loop
verification. By first writing the loop invariant as a comment inside the loop,
they can discern from the invariant what initialization, testing, and
processing steps are required. In this book, we will generally document our
WHILE and general loops with invariants and end-of-loop assertions.
PROBLEM SPECIFICATION
Your parents have some money to invest in a savings account and they are interested in knowing the best strategy for investment. They would like you to write a program that shows them the value of a certificate of deposit as it increases annually. They would like to use this program for both fixed-rate certificates and variable-rate certificates (in which the interest rate changes at the beginning of each year). Whenever it is run, your program should display a table showing the investment year, the annual interest, and the certificate balance at the end of each year until the balance has passed a target amount.
ANALYSIS
What is needed is a program that computes annual interest and new balance using the formulas
Balance) to
represent the old and new balance where the initial value of
Balance is the deposit amount (Deposit). The data
requirements for the problem follow.
Data Requirements
Problem Inputs
the deposit amount (Deposit : NonNegFloat)
the target balance (TargetBal : NonNegFloat)
the annual interest rate as a fraction (Rate : NonNegFloat)
an indicator of whether the interest rate is fixed or variable (FixedOrVar : Character)
Problem Outputs
the current investment year (Year : Positive)
the annual balance (Balance : NonNegFloat)
the annual interest earned (Interest : NonNegFloat)
The type Character variable FixedOrVar indicates
whether or not the annual interest rate is fixed (value is 'F') or
varying (value is 'V'). The algorithm is shown next.
DESIGN
Initial Algorithm
1. Enter the deposit amount, the value of FixedOrVar, and the
interest rate for a fixed-rate certificate.
2. Display a table showing the year, interest earned, and account balance as long as the balance has not passed the target balance. If the interest rate is variable, read in the new rate at the start of each year before computing the annual interest.
Step 2 requires a loop. Because we don't know how many iterations are needed,
we should use a WHILE loop. The loop has the following properties:
Year is the number of loop iterations performed so far.
Balance is the sum of Deposit plus all prior
values of Interest.
Balance is between TargetBal and
TargetBal + Interest just after loop exit. Step 2 Refinement
2.1. Initialize Year to 0
2.2. Initialize Balance to Deposit
2.3. Initialize Interest to 0
2.4. WHILE Balance < TargetBal LOOP
2.5. Increment Year by 1
2.6. IF the interest rate is variable THEN
2.7. Read this year's rate
END IF;
2.8. Compute the interest for this year
2.9. Compute the new value of Balance
2.10. Display the table line for the current year
END LOOP;
TEST PLAN
We leave the test plan as an exercise.
IMPLEMENTATION
The program is Program 6.6. The sample run uses a fixed interest rate.
Program 6.6
WITH Ada.Text_IO;
WITH Ada.Integer_text_IO;
WITH Ada.Float_Text_IO;
PROCEDURE Grow_Money IS
------------------------------------------------------------------------
--| Displays a table of interest earned and account balance for each
--| investment year for fixed or varying rate certificates.
--| Author: Michael B. Feldman, The George Washington University
--| Last Modified: July 1995
------------------------------------------------------------------------
SUBTYPE NonNegFloat IS Float RANGE 0.0 .. Float'Last;
FixedOrVar : Character; -- input - indicates fixed or varying rate
Deposit : NonNegFloat; -- input - initial amount of deposit
Rate : NonNegFloat; -- input - annual rate of interest
TargetBal : NonNegFloat; -- input - the target certificate amount
Balance : NonNegFloat; -- output - current certificate amount
Interest : NonNegFloat; -- output - amount of annual interest
Year : Natural; -- output - year of investment
BEGIN -- Grow_Money
Ada.Text_IO.Put (Item => "Enter the deposit amount $");
Ada.Float_Text_IO.Get (Item => Deposit);
Ada.Text_IO.Put (Item => "Enter the desired final balance $");
Ada.Float_Text_IO.Get (Item => TargetBal);
Ada.Text_IO.Put
(Item => "Is the interest rate fixed (F) or variable (V)? ");
Ada.Text_IO.Get (Item => FixedOrVar);
IF FixedOrVar = 'F' THEN
Ada.Text_IO.Put
(Item => "Enter the interest rate as a decimal fraction > ");
Ada.Float_Text_IO.Get (Item => Rate);
END IF;
-- Display table heading
Ada.Text_IO.New_Line;
Ada.Text_IO.Put (Item => "Year Interest Balance");
Ada.Text_IO.New_Line;
-- Display the certificate balance for each year.
Year := 0;
Balance := Deposit;
Interest := 0.0;
WHILE Balance < TargetBal LOOP
-- invariant:
-- Balance < TargetBal + Interest and
-- Balance is the sum of Deposit and all values of Interest
Year := Year + 1;
IF FixedOrVar = 'V' THEN
Ada.Text_IO.Put (Item => "Enter rate for year ");
Ada.Integer_text_IO.Put (Item => Year, Width => 0);
Ada.Text_IO.Put (Item => " > ");
Ada.Float_Text_IO.Get (Item => Rate);
END IF;
Interest := Balance * Rate;
Balance := Balance + Interest;
Ada.Integer_Text_IO.Put (Item => Year, Width => 4);
Ada.Float_Text_IO.Put (Item => Interest, Fore=>12, Aft=>2, Exp=>0);
Ada.Float_Text_IO.Put (Item => Balance, Fore=>12, Aft=>2, Exp=>0);
Ada.Text_IO.New_Line;
END LOOP;
-- assert: Balance >= TargetBal and
-- Balance is the sum of Deposit and all values of Interest
Ada.Text_IO.New_Line;
Ada.Text_IO.Put (Item => "Certificate amount reaches target after ");
Ada.Integer_Text_IO.Put (Item => Year, Width => 2);
Ada.Text_IO.Put (Item => " years");
Ada.Text_IO.New_Line;
Ada.Text_IO.Put (Item => "Final balance is $");
Ada.Float_Text_IO.Put (Item => Balance, Fore=>1, Aft=>2, Exp=>0);
Ada.Text_IO.New_Line;
END Grow_Money;
Sample
RunEnter the deposit amount $100.00 Enter the desired final balance $200.00 Is the interest rate fixed (F) or variable (V)? F Enter the interest rate as a decimal fraction > 0.035 Year Interest Balance 1 3.50 103.50 2 3.62 107.12 3 3.75 110.87 4 3.88 114.75 5 4.02 118.77 6 4.16 122.93 7 4.30 127.23 8 4.45 131.68 9 4.61 136.29 10 4.77 141.06 11 4.94 146.00 12 5.11 151.11 13 5.29 156.40 14 5.47 161.87 15 5.67 167.53 16 5.86 173.40 17 6.07 179.47 18 6.28 185.75 19 6.50 192.25 20 6.73 198.98 21 6.96 205.94 Certificate amount reaches target after 21 years Final balance is $205.94
Copyright © 1996 by Addison-Wesley Publishing Company, Inc.