Unit 4.4 Doing Things a Certain Number of Times,
Counting Negative

PROG

Print the word "something" three times.

PED

Another way to do something a certain number of times.

CONCEPT

countvariable:=limit;
while(countvariable <> 0) do begin
do the thing
countvariable:=countvariable - 1;
end;

DO LOOP INVARIANT

countempty is a count of the number of times "something" still needs to be printed.


Unit 4.4 - Doing Things a Certain Number of Times,
Counting Negative

Click here to view Unit 4.4 Pascal program.

We will learn a different plan for doing the important task of doing something a specific number of times. We will have a count go backwards. We should think of the count as counting the number of empty spaces where the thing still needs to be done.

Again, our sample program simply prints out the word "something" three times.

In our plan template, "limit" becomes the value three. The countvariable is "countempty" 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=3. There are three "somethings" that still haven't appeared on our output.

The next time through, countprinted=2. With one "something" on the output, there are still two to go.

Next time we hit that "w" in the while, countprinted=1. With two "somethings" on the output, there is still one to go.

And lastly, with countprinted=0, and one more "something" we have three "something"'s on the output. The condition is no longer true and we leave the loop, having successfully gotten precisely three "somethings"'s on the output.

As indicated above, our do-loop invariant is that
countempty is a count of the number of times "something" still needs to be printed.

We now do our checks to make sure our program works.
Check 1) The do loop invariant and the condition being true implies that executing the statements leaves the do-loop invariant true.

If we have a certain number of times, we need to do something and we do it one more time, the count in actuality of the number of times we need that done goes down by one. So does our variable with countempty:=countempty-1;

Check 2) The do loop invariant and the condition not being true implies the POSTCONDITION for the loop.

If countempty=0, that means there are no more times that the items needs to be printed.

Check 3) That the do loop invariant is initially true.

Initially, there are three places where "something" belongs but there is nothing yet on the output. This corresponds to setting countempty to three.

Check 4) that executing the statements once makes progress toward the goal

If we keep doing something, in this case printing "something", the number of times we still need to do it goes down.