invariant maintenance

Maintenance is the heart of a loop proof: it shows that one trip through the loop body keeps the invariant true. You assume the invariant holds at the top of an iteration (this assumption is the induction hypothesis), trace what the body does, and verify the invariant holds again at the top of the next iteration. Back to the ladder: assuming the tray is level on the current rung, you check that the way you take one step keeps it level on the next rung.

The careful part is that you only get to assume the invariant for the current iteration, not for the final answer you are hoping for. You walk through the body's effect on the variables and re-establish the invariant with the updated values. For insertion sort, assume 'A[1..i-1] is sorted'; the body slides A[i] leftward past larger elements and drops it into place, after which 'A[1..i] is sorted', and since i then becomes i+1 the invariant 'A[1..i-1] is sorted' holds again. Notice the invariant is restated for the new i. The whole argument is just one iteration; you never reason about 'all iterations at once' directly — induction does that for you.

Maintenance is where almost all real bugs surface, because it forces you to confront every line of the body and every edge of the data. If you cannot prove maintenance, either the body has a bug, or your invariant is too strong (claims more than the body preserves) or too weak (does not carry enough information forward). It pairs with initialization (the base case) to give, by induction, that the invariant holds before every iteration.