Invariant (computer science)

In computer science, a predicate that, if true, will remain true throughout a specific sequence of operations, is called (an) invariant to that sequence.

Use

Although computer programs are typically mainly specified in terms of what they change, it's equally important to know or specify the invariants of a program. This is especially useful when reasoning about the program. The theory of optimizing compilers, the methodology of design by contract, and formal methods for determining program correctness, all pay close attention to invariants in computer programs.

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

Example

The MU puzzle is a good example of a logical problem where determining an invariant is useful. The puzzle:
# If a string ends with an I, a U may be appended ("x"I → "x"IU)
# Any string after an M may be completely duplicated (M"x" → M"xx")
# Any three consecutive Is (III) may be replaced with a single U ("x"III"y" → "x"U"y")
# And two consecutive Us may be removed ("x"UU"y" → "xy")

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 predicate that's invariant to all rules, and makes getting to "MU" impossible. Logically looking at the puzzle, the only way to get rid of any Is is to have three consecutive Is in the string. The only way to get rid of all Is is when there are exactly three consecutive Is. This makes the following invariant interesting to consider:

:"The number of Is in the string is not a multiple of 3".

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 Is and Us we can see this actually is the case for all rules:

:

Above table shows clearly that the invariant holds for each of the possible transformation rules. Which basically means that whichever rule we pick, at whatever state, if the number of Is was not a multiple of three before applying the rule, it won't be afterwards either.

Given that there is a single I in the starting string MI, and one is not a multiple of three, it's impossible to go from MI to MU as zero is a multiple of three.

References

* C. A. R. Hoare. "An axiomatic basis for computer programming". "Communications of the ACM", 12(10):576–585, October 1969. doi|10.1145/363235.363259 [http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf | Download PDF ]
* J.D. Fokker, H. Zantema, S.D. Swierstra (1991). "Iteratie en invariatie", Programmeren en Correctheid. Academic Service. ISBN 90-6233-681-7.

ee also

* Hoare logic
* Loop invariant
* Object invariant
* Const correctness

External links

* [http://www.samdurak.com/software/VisualInvariants/ Applet: Visual Invariants in Sorting Algorithms ]