Editing Loop invariant

{{Short description|Invariants used to prove properties of loops}}
{{for|the computer programming  optimization technique|Loop-invariant code motion}}

In [[computer science]], a '''loop invariant''' is a property of a [[Computer program|program]] [[Control flow#Loops|loop]] that is true before (and after) each iteration. It is a [[logical assertion]], sometimes checked with a code [[Assertion (software development)|assertion]]. Knowing its invariant(s) is essential in understanding the effect of a loop.

In [[formal verification|formal program verification]], particularly the [[Hoare logic|Floyd-Hoare approach]], loop invariants are expressed by formal [[predicate logic]] and used to prove properties of loops and by extension [[algorithm]]s that employ loops (usually [[Correctness (computer science)|correctness]] properties).
The loop invariants will be true on entry into a loop and following each iteration, so that on exit from the loop both the loop invariants and the loop termination condition can be guaranteed.

From a programming methodology viewpoint, the loop invariant can be viewed as a more abstract specification of the loop, which characterizes the deeper purpose of the loop beyond the details of this implementation. A survey article <ref>Carlo A. Furia, [[Bertrand Meyer]] and Sergey Velder. "Loop invariants: analysis, classification, and examples."ACM Computing Surveys.  vol. 46, no. 3, February 2014([http://se.ethz.ch/~meyer/publications/methodology/invariants.pdf]</ref> covers fundamental algorithms from many areas of computer science (searching, sorting, optimization, arithmetic etc.), characterizing each of them from the viewpoint of its invariant.

Because of the similarity of loops and [[recursion|recursive]] programs, proving partial correctness of loops with invariants is very similar to proving the correctness of recursive programs via [[structural induction|induction]].  In fact, the loop invariant is often the same as the inductive hypothesis to be proved for a recursive program equivalent to a given loop.

==Informal example==
The following [[C (programming language)|C]] [[subroutine]] <code>max()</code> returns the maximum value in its argument array <code>a[]</code>, provided its length <code>n</code> is at least 1.
Comments are provided at lines 3, 6, 9, 11, and 13. Each comment makes an assertion about the values of one or more variables at that stage of the function.
The highlighted assertions within the loop body, at the beginning and end of the loop (lines 6 and 11), are exactly the same. They thus describe an invariant property of the loop.
When line 13 is reached, this invariant still holds, and it is known that the loop condition <code>i!=n</code> from line 5 has become false. Both properties together imply that <code>m</code> equals the maximum value in <code>a[0...n-1]</code>, that is, that the correct value is returned from line 14.
<!---Usage of (source) tag see http://www.mediawiki.org/wiki/Extension:SyntaxHighlight_GeSHi--->
<syntaxhighlight lang="c" line highlight="6,11">
int max(int n, const int a[]) {
    int m = a[0];
    // m equals the maximum value in a[0...0]
    int i = 1;
    while (i != n) {
        // m equals the maximum value in a[0...i-1]
        if (m < a[i])
            m = a[i];
        // m equals the maximum value in a[0...i]
        ++i;
        // m equals the maximum value in a[0...i-1]
    }
    // m equals the maximum value in a[0...i-1], and i==n
    return m;
}
</syntaxhighlight>
Following a [[defensive programming]] paradigm, the loop condition <code>i!=n</code> in line 5 should better be modified to <code>i<n</code>, in order to avoid endless looping for illegitimate negative values of <code>n</code>. While this change in code intuitively shouldn't make a difference, the reasoning leading to its correctness becomes somewhat more complicated, since then only <code>i>=n</code> is known in line 13. In order to obtain that also <code>i<=n</code> holds, that condition has to be included into the loop invariant. It is easy to see that <code>i<=n</code>, too, is an invariant of the loop, since <code>i<n</code> in line 6 can be obtained from the (modified) loop condition in line 5, and hence <code>i<=n</code> holds in line 11 after <code>i</code> has been incremented in line 10. However, when loop invariants have to be manually provided for formal program verification, such intuitively too obvious properties like <code>i<=n</code> are often overlooked.

==Floyd–Hoare logic==
In [[Hoare logic|Floyd–Hoare logic]],<ref>{{cite book 
 | contribution-url=http://www.cse.chalmers.se/edu/year/2017/course/TDA384_LP1/files/lectures/additional-material/AssigningMeanings1967.pdf
 | author=Robert W. Floyd
 | contribution=Assigning Meanings to Programs
 | editor=J.T. Schwartz
 | title=Proceedings of Symposia in Applied Mathematics
 | publisher=American Mathematical Society
 | location=Providence, RI
 | series=Mathematical Aspects of Computer Science
 | volume=19
 | pages=19–32
 | year=1967 }}</ref><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> the [[partial correctness]] of a [[while loop]] is governed by the following rule of inference:

:<math>\frac{\{C\land I\}\;\mathrm{body}\;\{I\}} {\{I\}\;\mathtt{while}\ (C)\ \mathrm{body}\;\{\lnot C\land I\}}</math>

This means:
* If some property {{mvar|I}} is preserved by the code <math>\mathrm{body}</math> —more precisely, if {{mvar|I}} holds after the execution of <math>\mathrm{body}</math> whenever both {{mvar|C}} and {{mvar|I}} held beforehand— ''(upper line)'' then
* {{mvar|C}} and {{mvar|I}} are guaranteed to be false and true, respectively, after the execution of the whole loop <math>\mathtt{while}\ (C)\ \mathrm{body}</math>, provided {{mvar|I}} was true before the loop ''(lower line)''.

In other words: The rule above is a deductive step that has as its premise the [[Hoare triple]] <math>\{C\land I\}\;\mathrm{body}\;\{I\}</math>.  This triple is actually a [[relation (mathematics)|relation]] on machine states.  It holds whenever starting from a state in which the boolean expression <math>C\land I</math> is true and successfully executing some code called <math>\mathrm{body}</math>, the machine ends up in a state in which {{mvar|I}} is true.  If this relation can be proven, the rule then allows us to conclude that successful execution of the program <math>\mathtt{while}\ (C)\ \mathrm{body}</math> will lead from a state in which {{mvar|I}} is true to a state in which <math>\lnot C\land I</math> holds.  The boolean formula {{mvar|I}} in this rule is called a loop invariant.

With some variations in the notation used, and with the premise that the loop halts, this rule is also known as the '''Invariant Relation Theorem'''.<ref name="conway-gries">{{cite book |last1=Conway |first1=Richard |author-link1=Richard W. Conway |last2=Gries |first2=David |author-link2=David Gries|year=1973 |title=An Introduction to Programming: A Structured Approach using PL/1 and PL/C |publisher=Winthrop |location=Cambridge, Massachusetts | pages=198–200 }}</ref><ref>{{cite book | title=Software Error Detection through Testing and Analysis | author-first=J. C. | author-last= Huang | publisher=John Wiley & Sons |location= Hoboken, New Jersey | year= 2009 | pages=156–157 }}</ref>  As one 1970s textbook presents it in a way meant to be accessible to student programmers:<ref name="conway-gries"/>

Let the notation <code>P { seq } Q</code> mean that if <code>P</code> is true before the sequence of statements <code>seq</code> run, then <code>Q</code> is true after it.  Then the invariant relation theorem holds that

:<code>P & c { seq } P</code>
::implies   
:<code>P { DO WHILE (c); seq END; } P & ¬c</code>

===Example===
The following example illustrates how this rule works.  Consider the program

 while (x < 10)
     x := x+1;

One can then prove the following Hoare triple:

:<math>\{x\leq10\}\; \mathtt{while}\ (x<10)\ x := x+1\;\{x=10\}</math>

The condition ''C'' of the <code>while</code> loop is <math>x<10</math>.  A useful loop invariant {{mvar|I}} has to be guessed; it will turn out that <math>x\leq10</math> is appropriate.  Under these assumptions it is possible to prove the following Hoare triple:

:<math>\{x<10 \land x\leq10\}\; x := x+1 \;\{x\leq10\}</math>

While this triple can be derived formally from the rules of Floyd-Hoare logic governing assignment, it is also intuitively justified: Computation starts in a state where <math>x<10 \land x\leq10</math> is true, which means simply that <math>x<10</math> is true.  The computation adds 1 to {{mvar|x}}, which means that <math>x\leq10</math> is still true (for integer x).

Under this premise, the rule for <code>while</code> loops permits the following conclusion:

:<math>\{x\leq10\}\; \mathtt{while}\ (x<10)\ x := x+1 \;\{\lnot(x<10) \land x\leq10\}</math>

However, the post-condition <math>\lnot(x<10)\land x\leq10</math> ({{mvar|x}} is less than or equal to 10, but it is not less than 10) is [[Logical equivalence|logically equivalent]] to <math>x=10</math>, which is what we wanted to show.

The property <math>0 \leq x</math> is another invariant of the example loop, and the trivial property <math>\mathrm{true}</math> is another one.
Applying the above inference rule to the former invariant yields <math>\{0 \leq x\}\; \mathtt{while}\ (x<10)\ x := x+1\;\{10 \leq x\}</math>.
Applying it to invariant <math>\mathrm{true}</math> yields <math>\{\mathrm{true}\}\; \mathtt{while}\ (x<10)\ x := x+1\;\{10 \leq x\}</math>, which is slightly more expressive.

==Programming language support==

===Eiffel===
The [[Eiffel (programming language)|Eiffel]] programming language provides native support for loop invariants.<ref>[[Bertrand Meyer|Meyer, Bertrand]], ''Eiffel: The Language,'' [[Prentice Hall]], 1991, pp. 129–131.</ref> A loop invariant is expressed with the same syntax used for a [[class invariant]]. In the sample below, the loop invariant expression <code>x&nbsp;<=&nbsp;10</code> must be true following the loop initialization, and after each execution of the loop body; this is checked at runtime.

<syntaxhighlight lang="eiffel">    from
        x := 0
    invariant
        x <= 10
    until
        x > 10
    loop
        x := x + 1
    end</syntaxhighlight>

===Whiley===
The [[Whiley (programming language)|Whiley]] programming language also provides first-class support for loop invariants.<ref>{{cite journal|title=Designing a Verifying Compiler: Lessons Learned from Developing Whiley | doi=10.1016/j.scico.2015.09.006 | volume=113 | journal=Science of Computer Programming | pages=191–220| year=2015 | last1=Pearce | first1=David J. | last2=Groves | first2=Lindsay | doi-access= }}</ref> Loop invariants are expressed using one or more <code>where</code> clauses, as the following illustrates:

<syntaxhighlight lang="whiley">
function max(int[] items) -> (int r)
// Requires at least one element to compute max
requires |items| > 0
// (1) Result is not smaller than any element
ensures all { i in 0..|items| | items[i] <= r }
// (2) Result matches at least one element
ensures some { i in 0..|items| | items[i] == r }:
    //
    nat i = 1
    int m = items[0]
    //
    while i < |items|
    // (1) No item seen so far is larger than m
    where all { k in 0..i | items[k] <= m }
    // (2) One or more items seen so far matches m
    where some { k in 0..i | items[k] == m }:
        if items[i] > m:
            m = items[i]
        i = i + 1
    //
    return m
</syntaxhighlight>

The <code>max()</code> function determines the largest element in an integer array.  For this to be defined, the array must contain at least one element.  The [[postconditions]] of <code>max()</code> require that the returned value is: (1) not smaller than any element; and, (2) that it matches at least one element.  The loop invariant is defined inductively through two <code>where</code> clauses, each of which corresponds to a clause in the postcondition.  The fundamental difference is that each clause of the loop invariant identifies the result as being correct up to the current element <code>i</code>, whilst the postconditions identify the result as being correct for all elements.

==Use of loop invariants==

A loop invariant can serve one of the following purposes:
# purely documentary 
# to be checked within in the code, e.g. by an assertion call
# to be verified based on the [[Hoare logic|Floyd–Hoare approach]]

For 1., a natural language comment (like <code>// m equals the maximum value in a[0...i-1]</code> in the [[#Informal example|above]] example) is sufficient.

For 2., programming language support is required, such as the [[C (programming language)|C]] library [[assert.h]], or the [[#Eiffel|above]]-shown <code>invariant</code> clause in Eiffel. Often, run-time checking can be switched on (for debugging runs) and off (for production runs) by a compiler or a runtime option.{{citation needed|reason=hope that C's or/and Eiffel assert.h supports that?|date=May 2016}}

For 3., some tools exist to support mathematical proofs, usually based on the [[#Floyd–Hoare logic|above]]-shown Floyd–Hoare rule, that a given loop code in fact satisfies a given (set of) loop invariant(s).

The technique of [[abstract interpretation]] can be used to detect loop invariant of given code automatically. However, this approach is limited to very simple invariants (such as <code>0<=i && i<=n && i%2==0</code>).

==Distinction from loop-invariant code==
{{see|Loop-invariant code motion}}
'''Loop-invariant code''' consists of statements or expressions that can be moved outside a loop body without affecting the program semantics. Such transformations, called [[loop-invariant code motion]], are performed by some compilers to [[optimizing compiler|optimize]] programs.
A loop-invariant code example (in the [[C (programming language)|C programming language]]) is
<syntaxhighlight lang="C">
for (int i=0; i<n; ++i) {
    x = y+z;
    a[i] = 6*i + x*x;
}
</syntaxhighlight>
where the calculations <code>x = y+z</code> and <code>x*x</code> can be moved before the loop, resulting in an equivalent, but faster, program:
<syntaxhighlight lang="C">
x = y+z;
t1 = x*x;
for (int i=0; i<n; ++i) {
    a[i] = 6*i + t1;
}
</syntaxhighlight>
In contrast, e.g. the property <code>0<=i && i<=n</code> is a loop invariant for both the original and the optimized program, but is not part of the code, hence it doesn't make sense to speak of "moving it out of the loop".

Loop-invariant code may induce a corresponding loop-invariant property.{{clarify|reason=I guess, once the notion of 'loop-invariant code' is defined in a sufficiently formal way, it can be proven that loop-invariant code *always* induces a corresponding loop invariant property.|date=March 2016}} For the above example, the easiest way to see it is to consider a program where the loop invariant code is computed both before and within the loop:
<syntaxhighlight lang="C">
x1 = y+z;
t1 = x1*x1;
for (int i=0; i<n; ++i) {
    x2 = y+z;
    a[i] = 6*i + t1;
}
</syntaxhighlight>
A loop-invariant property of this code is <code>(x1==x2 && t1==x2*x2) || i==0</code>, indicating that the values computed before the loop agree with those computed within (except before the first iteration).

== See also ==
* [[Invariant (computer science)]]
* [[Loop-invariant code motion]]
* [[Loop variant]]
* [[Predicate transformer semantics#While loop|Weakest-preconditions of While loop]]

== References ==
{{reflist}}

== Further reading ==
* [[Thomas H. Cormen]], [[Charles E. Leiserson]], [[Ronald L. Rivest]], and [[Clifford Stein]]. ''[[Introduction to Algorithms]]'', Second Edition. MIT Press and McGraw-Hill, 2001. {{ISBN|0-262-03293-7}}. Pages 17–19, section 2.1: Insertion sort.
* [[David Gries]]. "[https://www.sciencedirect.com/science/article/pii/0167642383900151/pdf?md5=b36e62073525cbaa449b94ac1f1784fb&isDTMRedir=Y&pid=1-s2.0-0167642383900151-main.pdf&_valck=1 A note on a standard strategy for developing loop invariants and loops]." ''Science of Computer Programming'', vol 2, pp.&nbsp;207–214. 1984.
* Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin. "[http://citeseer.ist.psu.edu/292512.html Dynamically Discovering Likely Program Invariants to Support Program Evolution]." ''International Conference on Software Engineering'', pp.&nbsp;213–224. 1999.
* Robert Paige. "[https://www.cs.tufts.edu/~nr/cs257/archive/robert-paige/invariants.pdf Programming with Invariants]." ''IEEE Software'', 3(1):56–69. January 1986.
* Yanhong A. Liu, Scott D. Stoller, and [[Tim Teitelbaum]]. [http://www.cs.sunysb.edu/~stoller/SIEC-SCP.html Strengthening Invariants for Efficient Computation]. ''Science of Computer Programming'', 41(2):139–172. October 2001.
* Michael Huth, Mark Ryan. "[https://books.google.com/books?id=eUggAwAAQBAJ&q=%22loop+invariant%22 Logic in Computer Science].", Second Edition.

{{DEFAULTSORT:Loop Invariant}}
[[Category:Formal methods]]
[[Category:Control flow]]