Invariant (computer science)

In computer science, an invariant is a condition that can be relied upon to be true during execution of a program, or during some portion of it. It is a logical assertion that is held to always be true during a certain phase of execution. For example, a loop invariant is a condition that is true at the beginning and end of every execution of a loop.

Invariants are especially useful when reasoning about whether a computer program is correct. The theory of optimizing compilers, the methodology of design by contract, and formal methods for determining program correctness, all rely heavily on invariants.

Programmers often use assertions in their code to make invariants explicit. Some object oriented programming languages have a special syntax for specifying class invariants.

The MU puzzle is a good example of a logical problem where determining an invariant is useful. The puzzle asks one to start with the word MI and transform it into the word MU using in each step one of the following transformation rules:

An example derivation (superscripts indicating the applied rules) is

Is it possible to convert MI into MU using these four transformation rules only?

One could spend many hours applying these transformation rules to strings. However, it might be quicker to find a property that is invariant to all rules (i.e. that isn't changed by any of them), and demonstrates that getting to MU is impossible. Logically looking at the puzzle, the only way to get rid of any I's is to have three consecutive I's in the string. This makes the following invariant interesting to consider:

This is an invariant to the problem if for each of the transformation rules the following holds: if the invariant held before applying the rule, it will also hold after applying it. If we look at the net effect of applying the rules on the number of I's and U's we can see this actually is the case for all rules:

...
Wikipedia