The rap against "while True:" loops

[Tim Rowe]

2009/10/12 RDrewD <drewlist at gmail.com>:
> I was a bit surprised that nobody in this discussion so far bantered
> around the phrase "loop invariant", but then I looked in
> http://en.wikipedia.org/wiki/Loop_invariant and found it was draped in
> so much formalism that it's sure to put off all but the most dedicated
> of Computer Science fans.

I think in this case the loop variant is more use than the loop variant.

Basically, the loop variant is what is true on every pass of the loop.
If you're being formal, you have to show that it's true on entry to
the loop and remains true on every pass of the loop. That means that
on exit from the loop you can guarantee the loop invariant and the
exit condition.

The loop variant is a finite natural number (positive or zero integer)
that is guaranteed to decrease on every pass of the loop. Because a
finite natural number cannot decrease indefinitely, if you can define
a loop variant then you gurantee that the loop will terminate.

Even if you are not being formal, just considering what the loop
variants and invariants can save no end of trouble with tricky loops.

-- 
Tim Rowe