WHILE (we are not on 99th Street) do begin
move one block east
end;

SF

while (condition) do begin
statements
end;

Do-Loop Invariants

DEFINITION: something that is true at the W in the while

Purpose: to think about a program and see if it is correct

check

1) that the do loop invariant and the condition being true implies that the executing the statements leaves the do loop invariant true

2) that the do loop invariant and the condition not being true implies the POSTCONDITION for the loop

3) that the do loop invariant is initially true

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

Do Loop Invariant

We are at an intersection that is not East of 99th street

We are going to learn about looping. By having repetition of a set of statements--until a condition is reached, one can write programs that compute and print logarithm tables, reports and collections of invoices or continually monitor sensors in a chemical plant.

The while statement in pascal performs that repetition. It is of the form:

while (condition) do begin
statements to be executed
end;

The condition is written in the same form as the condition in an if is, and can even include "and" and "or." The condition is checked upon initial entry. If the condition is true, then the statements are executed in order from first to last. Then the condition is checked again If true, the statements are again executed. When and if the condition is found to be false, the while statement will stop executing the statements. Whatever statements follow the "end;" will be executed.

As we did with simple sequences and the if statements, we will illustrate the control structure on a street example. The next unit, will cover a program in real PASCAL.

We have a map with the streets numbered from to 1st Street to 100th street. Crossing these are regular avenues going down from First Avenue down to 100th Avenue. If one wanted a program that would get us from a location on First Street to 99th Street would take a long number of move one block east commands. Even harder would be a program that would take us from any street West of 99th Street to 99th Street. It would take a large number if if's and move one block east.

However, using a loop as seen above, will give us the ability to write programs to do these tasks in a few lines of code. There are two examples. The first will continue "while we are not on 99th Street." If we are not on the given location, we move one block East. The second example is similar. If we are west of 99th Street, we move one block East. The difference is in the "condition." They both will work as long as we start at some location West of 99th Street. But, what if we started at 100th Street. The first program will go off into parts unknown. The second program will simply leave the person at their starting location and not send them off on a wild-good chased. Question for thought: How would you write a program that will get our person to say 50th street, no matter where they started from?

A lot of times we can write and get correct without debugging, a program with loops by simple inspection. However, there is a technique called do loop invariants which helps us think about the programs we write and prove informally that our program is correct. (There are techniques that enbable one to prove formally that programs are correct in the same manner that one might prove two trigonometric identities equal or a theorem from geometry. The ofrmalization is beyond the scope of this course. See Dijkstra's Discipline of Programming for the best explication of these techniques.) With these techniques, we can ensure our programs are correct, first time, every time.

A do-loop invariant is some statement about the state of the world at the "w" in the "while" statement before either the condition is checked or the statements or executed. We call it a do-loop "invariant" because it is always true--if our program is working correctly. We must ensure that going through the loop one time, if both the condition and the invariant is true, will keep the invariant true. In our example, the do loop invariant is that we are west of 99th street on some intersection. If that is true, we can move one block east and not become East of 99th Street. (We might end up on 99th Street or some block that is still West of it. We won't end up West of 99th Street.

There are three other things to check on our list, the first being to verify that our do-loop really is invariant. Item number 2) is that the do loop invariant and the condition not being false implies that the do loop does whatever the do loop is supposed to do--the Postcondition for the do loop. In our case, our do loop invariant is that the program is not East of 99th Street and is on an intersection. If we know that it is not West from the condition being false, then by elimination, we must be on 99th Street, what our program is supposed to do.

Item number 3) is that the do loop invariant is initially true. We do that by checkoing the precondition, the program is only designed to work if initially, we are west of 99th Street.

Item number 4) is that executing the statements once gets us closer to the goal. If we are West of 99th Street and we move East, we are going to get closer to 99th Street.