Invariant (computer science)
Encyclopedia
In computer science
, a predicate is called an invariant to a sequence of operations
provided that: if the predicate is true before starting the sequence, then it is true at the end of the sequence.
s 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 program
s.
Programmers often make use of assertions
in their code to make invariants explicit. Some object oriented programming language
s have a special syntax for specifying class invariant
s.
is a good example of a logical problem where determining an invariant is useful. The puzzle is as follows:
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 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:
The table above 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 I's 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.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, a predicate is called an invariant to a sequence of operations
Operation (mathematics)
The general operation as explained on this page should not be confused with the more specific operators on vector spaces. For a notion in elementary mathematics, see arithmetic operation....
provided that: if the predicate is true before starting the sequence, then it is true at the end of the sequence.
Use
Although computer programComputer program
A computer program is a sequence of instructions written to perform a specified task with a computer. A computer requires programs to function, typically executing the program's instructions in a central processor. The program has an executable form that the computer can use directly to execute...
s 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
Design by contract
Design by contract , also known as programming by contract and design-by-contract programming, is an approach to designing computer software...
, and formal methods
Formal methods
In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...
for determining program correctness, all pay close attention to invariants in computer program
Computer program
A computer program is a sequence of instructions written to perform a specified task with a computer. A computer requires programs to function, typically executing the program's instructions in a central processor. The program has an executable form that the computer can use directly to execute...
s.
Programmers often make use of assertions
Assertion (computing)
In computer programming, an assertion is a predicate placed in a program to indicate that the developer thinks that the predicate is always true at that place.For example, the following code contains two assertions:...
in their code to make invariants explicit. Some object oriented programming language
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
s have a special syntax for specifying class invariant
Class invariant
In computer programming, specifically object-oriented programming, a class invariant is an invariant used to constrain objects of a class. Methods of the class should preserve the invariant. The class invariant constrains the state stored in the object....
s.
Example
The MU puzzleMU puzzle
The MU puzzle is a puzzle stated by Douglas Hofstadter and found in Gödel, Escher, Bach. As stated, it is an example of a Post canonical system and can be reformulated as a string rewriting system.-The puzzle:...
is a good example of a logical problem where determining an invariant is useful. The puzzle is as follows:
- If a string ends with an I, a U may be appended (xI → xIU)
- Any string after an M may be completely duplicated (Mx → Mxx)
- Any three consecutive I's (III) may be replaced with a single U (xIIIy → xUy)
- Any two consecutive U's may be removed (xUUy → 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 I's is to have three consecutive I's in the string. This makes the following invariant interesting to consider:
- The number of I's 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 I's and U's we can see this actually is the case for all rules:
| Rule | #I's | #U's | Effect on invariant |
|---|---|---|---|
| 1 | +0 | +1 | Number of I's is unchanged. If the invariant held, it still does. |
| 2 | ×2 | ×2 | If n is not a multiple of 3, then 2×n isn't either. The invariant still holds. |
| 3 | −3 | +1 | If n is not a multiple of 3, n−3 isn't either. The invariant still holds. |
| 4 | +0 | −2 | Number of I's is unchanged. If the invariant held, it still does. |
The table above 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 I's 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.