___________________ ___________________ ___________________Loop invariants provide a means to effectively determine the correctness of iterative solutions by helping one reason about the changes from one iteration to the next. A loop invariant is a boolean expression that is true each time the loop condition is evaluated. Typically the boolean expression is composed of variables used in the loop and evaluated each iteration of the loop. In particular, the initial establishment of the truth of the invariant helps determine the proper initial values of variables used in the loop condition and body. In the loop body, some statements make the invariant false, and other statements must then re-establish the invariant so that it is true before the loop condition is evaluated again.
The general structure of a loop is:
while (!done) { // check loop invariant: what is true at every step // body // update to maintain invariant }
Invariants can serve as both aids in recalling the details of an implementation of a particular algorithm and in the construction of an algorithm to meet a specification. You can also use invariants to characterize a variety of iterative processes.
For example, the partition phase of Quicksort is a classic example where an invariant can help in developing the code and in reconstructing the code. An invariant is shown pictorially and as the postcondition of the function partition below. The initial value of pivot is left. This ensures that the invariant is true the first time the loop test is evaluated. When pivot is incremented in the loop, the invariant is false, but the swap re-establishes the invariant.
int partition(String[] a, int left, int right) // precondition: left <= right // postcondition: rearranges entries in vector a // returns pivot such that // forall k, left <= k <= pivot, a[k] <= a[pivot] and // forall k, pivot < k <= right, a[pivot] < a[k] // { int k, pivot = left; String center = a[left]; for(k=left+1; k <= right; k++) { if (a[k].compareTo(center) < 0) { pivot++; swap(a,k,pivot); } } swap(a,left,pivot); return pivot; }
Question: What does swap look like?
The invariant for this shode can be shown pictorially.
As practice, consider the following problems as an introduction to the use of invariants as a tool for reasoning about loops. Use the APT testing page within your browser to test your solution. For each problem below, solve the problem with the APT and also write a loop invariant and put that in a README file.
Dutch class
flagify.