The rap against "while True:" loops

Mon Oct 12 04:28:00 EDT 2009

RDrewD wrote:

> my_prissy_little_indicator_variable = true
> while (my_prissy_little_indicator_variable){
>     <body>
> }
> isn't satisfying because it doesn't guard the <body> with any
> assurance that the loop invariant will be true before you enter into
> that block of code.

The loop invariant and the exit condition are different things.

The loop invariant is supposed to be true every time the loop
invariant is tested, including on the last iteration, so that
when the loop exits, you can assert that the loop invariant
*and* the exit condition are both true. The trick is to choose
them so that together they ensure whatever it is the loop is
meant to accomplish.

If the exit test is half way through the loop, then the loop
invariant doesn't have to be true before the loop is entered --
it only has to be true by the time the exit test is encountered
for the first time. In other words, the first execution of the
part of the loop before the exit test is really part of the
initialization, and has to be treated as such in the analysis.

> I don't mind while(true) for the case of "do forever" like those
> launcher requirements Peter Billam wrote about up above in this
> thread.   It essentially says the loop invariant is that the system
> hasn't crashed yet.

I think it's more accurate to say that, because there is no exit
test, there is no point in the loop at which a loop invariant
has to be true, so there is no need for a loop invariant, at least
in the sense the term is used in the formal theory of correctness
proofs for loops.

It may be desirable to impose invariants on the state of the
system at various points in the loop for other reasons, although
those might better be described as parts of the contracts between
the loop and the functions it calls.

(BTW, "the system hasn't crashed yet" can't be the loop invariant,
because if the loop ever exits then it means the system must have
crashed, so the loop invariant is no longer true!)

-- 
Greg