invariant initialization

Before you can trust that something stays true throughout a loop, you have to check it is true at the very start — before the loop body has run even once. This first check is initialization. It is the foot of the ladder: if the tray is not level before you take your first step, no amount of careful stepping will save you. So initialization asks: given how the variables were set up just above the loop, does the invariant already hold?

Concretely, you evaluate the invariant at the loop's entry, using the initial values of the loop variables. Often this case is almost trivial because the loop has done nothing yet, so the invariant talks about an empty range. For insertion sort, the invariant 'A[1..i-1] is sorted' is checked at i=1, where A[1..0] is the empty prefix — and an empty (or one-element) list is trivially sorted, so it holds. For a running sum with invariant 's = sum of A[1..i-1]', initialization sets s=0 and i=1, and the sum of the empty range A[1..0] is indeed 0. The point is to verify, not to wave it away.

Initialization is the base case of the induction hiding inside every loop proof: maintenance will be the inductive step. People often skip it because it 'obviously' holds, but skipping it is exactly where off-by-one and uninitialized-variable bugs hide. If your invariant cannot be made true at entry, that is a signal the invariant is wrong or the setup before the loop is missing a step.