CIT 594 Proving Loop Correctness
Spring 2015, David Matuszek

Consider the following simple code to fill an integer array with ones:

public static void fillWithOnes(int[] array) {
    int i = 0;
    while (i < array.length) {
        array[i] = 1;
        i += 1;
    }
}


This could be done just as easily with a for loop, but I'm using a while loop here because I think it makes the logic more apparent.

Now let's add some logic assertions to the code:

public static void fillWithOnes(int[] array) {
    int i = 0;
    while (i < array.length) {
        // Invariant: for all j < i, array[j] == 1
        array[i] = 1;
        i += 1;
    }
    // Exit condition: i >= array.length (this is the same as: NOT i < array.length)
    // Invariant + Exit condition: i >= array.length AND for all j < i, array[j] == 1
}


Consider the loop invariant, for all j < i, array[j] = 1.

We leave the loop whenever the condition (i < array.length) becomes false. However, the loop invariant is still true.

Now the question is, Did the loop accomplish what we wanted it to do? That is, has every element in the array been set to one? If it has, then the conjunction (and) of the above two conditions, the loop invariant and the exit condition, should express that every location in the array is equal to 1.

Executable assertions

Java has an assert statement, with two forms:

assert boolean_expression;
assert boolean_expression: expression;

By default, assert statements are treated as comments, that is, ignored. to make them executable, you have to give the flag -ea (or -enableassertions) to the compiler. In Eclipse, go to Run → Run Configurations... → Java Application → Your Application, choose the Arguments tab, and type -ea into the VM arguments field.

Once enabled, the assert statement behaves like this: The boolean_expression is evaluated, and if true, the statement doesn't do anything. But if the boolean_expression is false, an AssertionError is thrown. If you wish to add information to the message in the thrown exception, you can put that extra information as the expression after the colon.

A boolean expression is good for expressing simple conditions, such as the exit condition (assert i >= array.length;), but cannot by itself express quantifiers such as for all (∀) or there exists (∃). For that, you need to put the assert statement in a loop.

public static void fillWithOnes(int[] array) {
    int i = 0;
    while (i < array.length) {
        for (int j = 0; j < i; j++) assert array[j] == 1; // loop invariant
        array[i] = 1;
        i += 1;
    }
    assert i >= array.length; // exit condition
    for (int j = 0; j < array.length; j++) assert array[j] == 1; // invariant + exit
}

So what?

The fact is, you can do just fine as a programmer without ever even having heard of loop invariants.

However, many people who are primarily mathematicians, and who approach computer science from the viewpoint of mathematics, feel that the correct way to write any loop is to start from the loop invariant, and use that to drive the code. And this includes some of the most brilliant minds in computer science.

That's not me. Neither the part about deciding the invariant before writing the loop (though I have done that on occasion), nor, sadly, the part about being one of the most brilliant minds in computer science. The late Edsger Dijkstra comes to mind, and I certainly would never want to argue with him.

So my view is, you may occasionally meet people who will have a higher opinion of you if you understand loop invariants. And besides, it's another tool in your mental toolbox, one that may sometimes come in handy. I don't use loop invariants every day, but I do use them every once in awhile.