World Library  
Flag as Inappropriate
Email this Article

Invariant (computer science)

Article Id: WHEBN0001126643
Reproduction Date:

Title: Invariant (computer science)  
Author: World Heritage Encyclopedia
Language: English
Subject: Design by contract, Precondition, Liskov substitution principle, Vienna Development Method, Tree rotation
Collection: Computer Programming, Formal Methods
Publisher: World Heritage Encyclopedia
Publication
Date:
 

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.

Contents

  • Use 1
  • Example 2
  • Automatic invariant detection in imperative programs 3
  • See also 4
  • References 5
  • External links 6

Use

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 "invariant"s in computer programs.

Programmers often use 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 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:

  1. If a string ends with an I, a U may be appended (xI → xIU)
  2. The string after the M may be completely duplicated (Mx → Mxx)
  3. Any three consecutive I's (III) may be replaced with a single U (xIIIyxUy)
  4. Any two consecutive U's may be removed (xUUyxy)

An example derivation (superscripts indicating the applied rules) is

MI →2 MII →2 MIIII →3 MUI →2 MUIUI →1 MUIUIU →2 MUIUIUUIUIU →4 MUIUIIUIU → ...

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.

Automatic invariant detection in imperative programs

Abstract interpretation tools can compute simple invariants of given imperative computer programs. The kind of properties that can be found depend on the abstract domains used. Typical example properties are single integer variable ranges like 0<=x<1024, relations between several variables like 0<=i-j<2*n-1, and modulus information like y%4==0. Academic research prototypes also consider simple properties of pointer structures.[1]

Any more sophisticated invariants still have to be provided manually. In particular, when verifying an imperative program using the Hoare calculus,[2] a loop invariant has to be provided manually for each loop in the program, which is one of the reasons for that task being extremely tedious.

In the above example, no tool will be able to detect from rules 1-4 that a derivation "MI →...→ MU" is impossible. However, once the abstraction from the string to the number of its "I"s has been made by hand, leading e.g. to the following C program, an abstract interpretation tool will be able to detect that ICount%3 can't be 0 and hence the "while"-loop will never terminate.

void MUPuzzle(void) {
    volatile int RandomRule;
    int ICount=1, UCount=0;
    while (ICount%3!=0)                            // non-terminating loop
        switch(RandomRule) {
        case 1:                UCount+=1;   break;
        case 2:   ICount*=2;   UCount*=2;   break;
        case 3:   ICount-=3;   UCount+=1;   break;
        case 4:                UCount-=2;   break;
        }                                          // computed invariant: ICount%3==1||ICount%3==2
}

See also

References

  • J.D. Fokker, H. Zantema, S.D. Swierstra (1991). "Iteratie en invariatie", Programmeren en Correctheid. Academic Service. ISBN 90-6233-681-7.
  1. ^ Bouajjani, A.; Drǎgoi, C.; Enea, C.; Rezine, A.; Sighireanu, M. (2010). "Proc. CAV". 
  2. ^  

External links

  • Applet: Visual Invariants in Sorting Algorithms
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
 
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
 
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.
 



Copyright © World Library Foundation. All rights reserved. eBooks from World eBook Library are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.