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