PROG
Print the word "something" three times.
PED
How to do something a certain number of times.
CONCEPT
countvariable:=0;
while(countvariable <> limit) do begin
do the thing
countvariable:=countvariable + 1;
end;
DO LOOP INVARIANT
countvariable is a count of the number of times "something" was printed
Click here to view Unit 4.3 Pascal program.
A very important plan is to do some activity a certain number of times. Our computer may need to count out 100 screws in an automated assembly plant or instruct a robot to do a certain number of brush strokes to get a car painted. More prosaically, our computer might have to print out a certain number of blank lines to generate a report in the correct format.As you might suspect, we need a count variable. That count variable will tell us how many times we have done the activity. Each time through the loop, we increment that count variable. Notice that we start the count variable at zero and continue as long as the count variable is not equal to the limit--the number of times we have to do the thing.
Our sample program simply prints out the word "something" three times. In our plan
template, "limit" becomes the value three. The countvariable is "countprinted" The
write and the writeln "do the thing"
Just to go through it by hand, the first time we pass the "w" in the while, we have
countprinted=0 and nothing printed out yet.
The next time through, countprinted=1 and we have one "something" on the output.
The third time we pass that "w", countprinted would be two and we would have two "something" on the output.
The fourth time, countprinted would be three and three "something" would appear. Now countprinted is no longer "<>" 3 so we leave the loop and hit the end of the program.
As indicated above, our do-loop invariant is that
countvariable is a count of the number of times "something" was printed
We now do our checks to make sure our program works. By doing these checks, we can help protect agains the frequent "off by one" errors that often plague programmers, the new and the experienced alike. "Off by one" errors are those where something is done one too many or one too few times.
Check 1) The do loop invariant and the condition being true implies that executing the statements leaves the do-loop invariant true.
We print "something" one more time and we increment countprinted one more time. This adds one both to the variable keeping track of the number of times the thing was printed as well as adding one to the number of times "something" was actually printed.
Check 2) The do loop invariant and the condition not being true implies the POSTCONDITION for the loop.
When the condition is not true, that means countprinted=3. From our do loop invariant, that means there are 3 "something"'s on our output.
Check 3) That the do loop invariant is initially true.
Initially, there are no "somethings" on the output. countprinted=0, reflecting that fact.
Check 4) that executing the statements once makes progress toward the goal
As we keep adding "something"'s to that which already has appeared, we get closer and closer to whatever the limit is.