Program Verification: Loop Invariants ======================================= Loop invariants are a useful tool for proving to yourself and to the reader that your program works. Most people are frightened by them, because they associate them with formal mathematical mumble jumble that one comes up with after the fact and which they don't really understand. Within the assignments (unless otherwise stated), we don't require a formal proof of correctness. However, understanding the concept of a loop invariant will help you in your programming. Below is a list of questions to ask yourself about your loop along with the answers for a simple example loop. The purpose of the loop in the example is to compute 2^n, where n is a variable that has some value. The method decided upon is to repeatedly multiply a variable y by two. For each loop, think about - What is the task of the loop? > To compute 2^n. - What state do you want the data to be in after the loop terminates? This is called the POST-LOOP INVARIANT. > The variable y should have the value 2^n. - What progress towards this final goal do you want to make by going once around the loop? - What state do you what the data to be in EVERY time the program is at the top of the loop? This is called the LOOP INVARIANT. > y = 2^i for some index i. - and what state at the bottom of the loop? This is called the BOTTOM-LOOP INVARIANT. > y = 2 * 2^i = 2^(i+1) (The bottom invariant should be the same as top invariant, except with the indexes incremented.) - What code do you need within the loop to get the data from the state required by top loop invariant to that required by the bottom. > y = y*2; - What code do you need before the loop, to get the data into the state required by the loop invariant? > y=1; i=0; - The loop invariant together with the halting condition of the loop should conclude the post-loop condition. Check this. > From (y = 2^i and i=n), we conclude that (y = 2^n). Explanations and pictures of these invariants should be included in your external documentation. /**************************************************************/ /* exp: */ /* ------ */ /* input: n (integer) */ /* output: 2^n (integer) */ /* Method: multiple multiplications by 2 */ /* Precondition: n>=0 */ /* Postcondition: output 2^n */ /* ************************************************************/ int exp( int n ) { int y=1; int i=0; /* loop invariant y = 2^i */ for( ; i loop exit when end loop Goal: prove P => Q Steps 1) P => I 2) (I' & not E) and B exicuted => I'' 3) I & E => Q 4) Loop terminates. --------------------------------------------------------- Demonstrating the use of Internal Documentation, Prologues, and Loop Invariants in an Insertion Sort Program ----------------------------------------- A description of the algorithm used, loop invariants, and comments on key lines of code need to be included. However, these should not simply parrot the code. They do not need to be a lot of formal mathematical mumble jumble. They need to reveal the underlying meaning that you as the programmer had in mind, yet that is not immediately clear from the code. The description of the algorithm should not trace out a running of the program and should not describe the code. (We can see the code ourselves.) It needs to be a high level, intuitive, conceptual description of what is happening, how the data is stored, and why it works. Loop invariants are a useful tool for proving to yourself and to the reader that your program works. Most people are frightened by them, because they associate them with formal mathematical mumble jumble that one comes up with after the fact and which they don't really understand. Instead explain what you had in mind with this loop. You came up with the loop. What were your thought processes? Conceptually (underlying meaning) what is true every time the program is at this point in the code. Why is it true the first time through the loop. If under any circumstances the loop invariant happens to be true, why would it be true again after going around the loop again? Bottom-loop invariants have been included to demonstrate how the top-loop invariant plus the code can imply the bottom-loop invariant and how the bottom-loop invariant plus an incrementing or decrementing of a key variable can imply the top-loop invariant again. What progress is made towards your final goal by going once around the loop? Post-loop invariants state what we want to be true when the loop breaks. This statement should follow from combining the loop invariant with the condition that caused the loop to break. Does achieving the post-loop invariant solve the algorithmic problem? Chose your variable names carefully. They need to be informative. They need to reveal what the variable is used for. Sometimes they should also indicate what data type the variable is, eg add "Ptr" or simply "P" if it is a pointer and "Index" if it is an index. For example "compareIndex" would reveal that this is the index of the value currently being compared. On the other hand, if the variable names are too lengthy, then the code and the comments can become overly cumbersome. Your own judgment is required. In this case, we opted for the description of the variable to be in the header and for the name it self to be just enough for the reader to recall its purpose. %*********************************************************************** * * * arraySort * * --------- * * Input: A() - array to be sorted * * (an array of pointers to character strings) * * N - the number of elements in the array * * Output: A() - the original strings in sorted order * * * * Method: linear insertion sort * * * * Preconditions: * * N >= 0 * * A(1), ... , A(N) are valid pointers * * to null-terminated strings * * * * Postcondition: * * Array A is sorted in lexicographic order * * i.e. *A(1) <= ... <= *A(N) * * * ************************************************************************ Algorithm Used: Linear Insertion Sort Bad Version ------------------------------------------- We loop through nextI being from 0 to N-1. For each of these loops, we loop though compI from nextI-1 down to 0. As we do this A(compI+1) is assigned A(compI). (and perhaps more useless stuff .... Algorithm Used: Linear Insertion Sort High Level Conceptual Underlying Meaning Version ------------------------------------------- We will maintain a sorted list of elements. The remaining elements will be be thought of as being off to the side somewhere. Initially, think of the first element in the array as a sorted list of length one. One at a time we take one of the elements that is off to the side and we INSERT it into the sorted list where it belongs. This gives a sorted list that is one element longer then it was before. When the last element has been inserted, the array is completely sorted. There are two steps in inserting an element into a sorted list. The most obvious step is that the location where it belongs must be found. The second step is that all the elements that are bigger then the element to be inserted must be shifted one to the right to make room for the new element. The location for the element to be inserted could be found using binary search. However, it is easier to search and shift the larger elements simultaneously. ********************************************************************* arraySort (A : array 1 .. * of string, N : int) % next string to be inserted in its proper place var str : string % index of next string in array to be inserted in its proper place var nextI : int % index of string to be compared with string being inserted var compI : int nextI := 2 loop exit when nextI >= N + 1 % Loop Invariant: % The sub-array A(1..nextI-1) is sorted % i.e. A(1) <= ... <= A(nextI-1) % String str is taken and put on the side and % is to be inserted into the sorted sub-list. % The entry A(nextI) is made "empty" str := A (nextI); compI := nextI - 1 loop % Loop Invariant: % The sub-array A(1..nextI) is sorted, % except entry A(compI+1) is "empty". % The string *str belongs somewhere % in the sub-array A(1..compI+1) if compI < 1 or A (compI) <= str then % Invariant: % The string *str belongs in entry A(compI+1), % (which is empty) exit % to insert end if % else str belongs in sub-array A(1..compI) % Shift "empty" spot left from A(compI+1) to A(compI) A (compI + 1) := A (compI); % Bottom-Loop Invariant: % Entry A(compI) is "empty". % The string *str belongs in the sub-array A(1..compI) end loop % Post-Loop Invariant: The string str belongs in entry A(compI+1) % and this entry is empty % Fill the "empty" spot with string *str to be inserted A (compI + 1) := str; % Bottom-Loop Invariant % The sub-array A (1 .. nextI) is sorted end loop % Post-Loop Invariant % The sub-array A(1..nextI-1) is sorted and nextI=N. % Hence, the array A(1..N-1) is sorted. end loop end arraySort