Editing Loop invariant (section)

==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.