Invariant (computer science)

An invariant is a statement that applies to the execution of certain program instructions. So it is true before and after these commands, so it is not changeable, i.e. invariant. Invariants can be used to prove the correctness of algorithms and play a major role in design by contract . The preconditions and postconditions for a method of an interface and all invariants in their sequence are described. This concept can be implemented using so-called assertions , provided it supports the programming language or API used .

See also

• Loop invariant
• Invariance in Java
• Invariant specification in UML

Web links

• Program for automatic verification (a version ported to Java is also linked on the page)