How to find the loop invariant and prove correctness?

Question

int i, temp; 
a is an array of integers [1...100] 

i = 1; 

while i < 100 
    if a[i] > a[i+1] 
        temp = a[i]
        a[i] = a[i+1]
        a[i+1] = temp 
    i = i+1

I'm having trouble understanding how to find loop invariants and writing a formal statement for them. So a loop invariant is just a condition that is true immediately before and after each iteration of a loop. It looks like the code is doing a swap: if the following element is greater in the array than the current one, switch places. I mean from the definition of a loop invariant, it really sounds like it's i < 100 because that must be true for the loop to run, but I don't really understand. Would greatly appreciate some clarification.

Answer 1

Your loop is controlled by the test i < 100. Within the body of the loop, i is used in several places but is only assigned in one place. The assignment always happens, and for any value of i which permits entry to the loop the assignment will converge towards the terminating condition. Thus the loop is guaranteed to terminate.

As for correctness of your program, that's a different issue. Depending on whether your arrays use zero-based or one-based indexing, the way you're using i for array accesses could be problematic. If it's zero-based, you never look at the first element and you'll step out of bounds with a[i+1] on the last iteration.

Answer 2

Going by your definition, I can see two loop invariant conditions:

1. i < 100
2. a[i] = greater than a[j] for all j < i, where i is the loop variable.

This is in fact one outer loop iteration of bubble sort. At the end of this loop, the highest value in the array bubbles to the top (a[100]) .

Answer 3

Roughly speaking, you are right. A loop invariant is "just a condition that is true immediately before and after each iteration of a loop." However, under this definition, there are literally an infinite number of loop invariants for the code in question and most of them are of no particular interest. For example, i < 101, i < 102, i < 103, ... are all loop invariants for the given code.

However, usually we are not interested in simply finding a loop invariant just for the sake of finding a loop invariant. Instead, we are interested in proving a program correct and if we want to prove a program correct then a well-chosen loop invariant turns out to be very useful.

For example, the code in question is the inner loop of the bubble sort algorithm and its purpose is to make the array "more sorted". Hence, to prove total correctness of this code we must prove three things:

(1) When execution gets to the end of the code, the array is a permutation of the array at the beginning of the code. (2) When execution gets to the end of the code, the number of inversions in the array is either zero or it is less than the number of inversions in the array at the beginning of the code (this condition helps us prove that the outer loop of the bubble sort algorithm terminates). (3) The code terminates.

To prove (1) we need to consider three execution paths (and a loop invariant will play a critical role when we consider PATH 2).

(PATH 1) Consider what happens when execution starts at the beginning of the code and arrives at the top of the loop for the first time. Since nothing is done to the array on this execution path, the array is a permutation of the array at the beginning of the code.

(PATH 2) Now consider what happens when execution starts at the top of the loop, goes around the loop, and returns to the top of the loop. If a[i] <= a[i+1] then the swap does not occur and, thus, the array is still a permutation of the array at the beginning of the code (since nothing is done to it). Alternatively, if a[i] > a[i+1] then the swap does occur. However, the array is still a permutation of the array at the beginning of the code (since a swap is a type of permutation). Thus, whenever execution gets to the top of the loop, the array is a permutation of the array at the beginning of the code. Note that the statement "the array is a permutation of the array at the beginning of the code" is the well-chosen loop invariant that we need to help us prove that the code is correct.

(PATH 3) Finally, consider what happens when execution starts at the top of the loop but does not enter the loop and instead it goes to the end of the code. Since nothing is done to the array on this execution path, the array is a permutation of the array at the beginning of the code.

These three paths cover all possible ways that execution can go from the beginning of the code to the end of the code and, hence, we have proved (1) the array at the end of the code is a permutation of the array at the beginning of the code.

Answer 4

A loop invariant is some predicate (condition) that holds for every iteration of the loop, that is necessarily true immediately before and immediately after each iteration of a loop.

There can be of course infinitely many loop invariants, but the fact that the loop invariant property is used to prove correctness of the algorithm, restricts us to consider only the so-called "interesting loop invariants".

Your program, whose aim is to sort the given array, is a simple bubble sort.

Goal Statement: The array a is sorted at the end of while loop
Some interesting properties can be like: At the end of ith iteration, a[0:i] is sorted, which when extended to i=100, results in the whole array being sorted.

Loop Invariant for your case: a[100-i: 100-1] is sorted

Note that when i equals 100, the above statement would mean that the complete array is sorted, which is what you want to be true at the end of the algorithm.

PS: Just realized it is an old question, anyway helps in improving my answering skills:)