In computer science, a loop invariant is a property of a program loop that is true before (and after) each iteration. It is a logical assertion, sometimes checked with a code assertion. Knowing its invariant(s) is essential in understanding the effect of a loop. In formal program verification, particularly the Floyd-Hoare approach, loop invariants are expressed by formal predicate logic and used to prove properties of loops and by extension algorithms that employ loops (usually 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 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 recursive programs, proving partial correctness of loops with invariants is very similar to proving the correctness of recursive programs via 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 subroutine max() returns the maximum value in its argument array a[], provided its length n 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 i!=n from line 5 has become false. Both properties together imply that m equals the maximum value in a[0...n-1], that is, that the correct value is returned from line 14.
Following a defensive programming paradigm, the loop condition i!=n in line 5 should better be modified to i<n, in order to avoid endless looping for illegitimate negative values of n. While this change in code intuitively shouldn't make a difference, the reasoning leading to its correctness becomes somewhat more complicated, since then only i>=n is known in line 13. In order to obtain that also i<=n holds, that condition has to be included in the loop invariant. It is easy to see that i<=n, too, is an invariant of the loop, since i<n in line 6 can be obtained from the (modified) loop condition in line 5, and hence i<=n holds in line 11 after i 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 i<=n are often overlooked.
Floyd–Hoare logic In Floyd–Hoare logic, the partial correctness of a while loop is governed by the following rule of inference:
{ C ∧ I } b o d y { I } { I } w h i l e ( C ) b o d y { ¬ C ∧ I } {\displaystyle {\frac {\{C\land I\}\;\mathrm {body} \;\{I\}}{\{I\}\;{\mathtt {while}}\ (C)\ \mathrm {body} \;\{\lnot C\land I\}}}}
This means:
… excerpt ends here. Continue reading the full article.
