A property that remains TRUE across some transformation or mapping. In the context of program correctness proofs, an invariant is an assertion that is associated with some program element and remains TRUE despite execution of some part of that element. For example, a loop invariant is an assertion that is attached at some point inside a program loop, and is TRUE whenever the attachment point is reached on each iteration around the loop. Similarly a module invariant is associated with a given module, and each operation provided by the module assumes that the invariant is TRUE whenever the operation is invoked and leaves the invariant TRUE upon completion.

Note that invariants cannot accurately be described as TRUE AT ALL TIMES since individual operations may destroy and subsequently restore the invariant condition. However the invariant is always TRUE between such operations, and therefore provides a static characterization by which the element can be analysed and understood.