[Python-ideas] Re: RFC: For Loop Invariants

On Sat, Apr 11, 2020 at 03:19:06PM +1200, Greg Ewing wrote:

Also it doesn't quite do a complete job, because it doesn't check the invariant after the last iteration,

I'm not sure whether loop invariants should be checked at the beginning of the loop, the end of the loop, or both. Anyone know what Eiffel does?

and doesn't check it at all if the iterable is empty.

That is surely okay though. If the loop is never entered at all, by the principle of vacuous truth the condition inside the loop is true.

For what it's worth, I agree that loop invariants should look like assertions, not ordinary conditionals.