I have been hearing about this term in various contexts.


“An invariant is a formula stating what must be true in every state of the execution.”

The invariant is a formalization of the programmer’s intention for what the loop should accomplish.

Inv is usually an assertion that the intended computation of the loop is correct up to the current step in execution. In general, Inv expresses a relationship between the variables manipulated by the body of the loop.

The variable values may change in each iteration of the loop, but the relationship holds.

If we choose the wrong invariant, we won’t be able to prove the VC’s.