A while statement takes a controlling logical expression and a code block. It runs the code block repeatedly while the logical expression evaulates to true. The code block is called the body of the while loop. Because it can run a block over and over again, it is called a looping construct.
This is the first construct we have shown that allows a program to repeat a section of code, even to run indefinitely, forever repeating the code block.
It is very difficult to verify that a program does what it is intended to do. Many of those difficulties arise during the analysis of looping constructs. The method of loop invariants helps with this analysis. A loop invariant is an assertion, a logical statement that is placed prior to the entry of the loop and placed at the bottom of the loop, and should at those positions in the code always evaluate to true.
☆ For example, in a loop that identifies the maximum value in an array, the loop might scan the array by increasing index and the loop invariant will state that the maximum has been identified among the indices so far scanned. The L.I. is initialized by considering only the first index scanned, and therefore the first index is the maximum. With each passage through the loop an additional index is considered, the the L.I. re-established by updating if the element at the index is larger than the previously identified maximum element.
The L.I. provides one aspect of correctness, but does not consider whether the loop terminates. All loops need to be analyzed for termination. The method of loop invariants also advocates for the separate arguing for termination. In the example of scanning an array for the maximum element, termination is argued by the advance of the index at each pass through the loop towards a finite value.