Invariance

I have been hearing about this term in various contexts.

• CS138: Representation Invariant, Representation Invariant, Loop Invariant
• Lidar: PointPillars permutation invariance, maybe even PointPillars permutation invariance, maybe even Distance Metric where they talk about the importance of symmetry
• SE212: Implicit Invariant
• STAT206: Property 3 of MLE

SE212

“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.