Loop Invariant Positioning
l
The loop invariant always goes right before the
test for continuing to the next iteration.
l
In particular, it is ÒtestedÓ:
l
Before the first iteration, if any.
l
Before each additional iteration.
l
Before exit.
l