Editing Invariant (mathematics) (section)

===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 interpretation#Examples of abstract domains|abstract domains]] used. Typical example properties are single integer variable ranges like <code>0<=x<1024</code>, relations between several variables like <code>0<=i-j<2*n-1</code>, and modulus information like <code>y%4==0</code>. Academic research prototypes also consider simple properties of pointer structures.<ref>{{cite conference|first1=A.|last1=Bouajjani|first2=C.|last2=Drǎgoi|first3=C.|last3=Enea|first4=A.|last4=Rezine|first5=M.|last5=Sighireanu|author5-link= Mihaela Sighireanu |title=Invariant Synthesis for Programs Manipulating Lists with Unbounded Data|book-title=Proc. CAV|year=2010|doi=10.1007/978-3-642-14295-6_8|url=https://link.springer.com/content/pdf/10.1007/978-3-642-14295-6_8.pdf|doi-access=free}}</ref>

More sophisticated invariants generally have to be provided manually.
In particular, when verifying an imperative program using [[Hoare logic|the Hoare calculus]],<ref>{{Cite journal
 |last1=Hoare 
 |first1=C. A. R. 
 |author-link1=C.A.R. Hoare 
 |title=An axiomatic basis for computer programming 
 |doi=10.1145/363235.363259 
 |journal=[[Communications of the ACM]] 
 |volume=12 
 |issue=10 
 |pages=576&ndash;580 
 |date=October 1969 
 |s2cid=207726175 
 |url=http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf 
 |url-status=dead 
 |archive-url=https://web.archive.org/web/20160304013345/http://www.spatial.maine.edu/~worboys/processes/hoare%20axiomatic.pdf 
 |archive-date=2016-03-04 
}}</ref> a loop invariant has to be provided manually for each loop in the program, which is one of the reasons that this approach is generally impractical for most programs.

In the context of the above [[MU puzzle]] example, there is currently no general automated tool that can detect that a derivation from MI to MU is impossible using only the rules 1–4. However, once the abstraction from the string to the number of its "I"s has been made by hand, leading, for example, to the following C program, an abstract interpretation tool will be able to detect that <code>ICount%3</code> cannot be 0, and hence the "while"-loop will never terminate.

<syntaxhighlight lang="C">
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
}
</syntaxhighlight>