Editing Loop invariant (section)

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