CIT 594 Proving Loop Correctness
Spring 2015, David Matuszek

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.

• This is slightly condensed, as i and j are both bounded variables. In more detail, the invariant should read for all 0 <= j < i < array.length, array[j] = 1.
• When the loop is first entered, the invariant is vacuously true. That is, there are no contradictory instances. Specifically, since i is 0, there does not exist a j such that 0 <= j < 0. A common example from logic is "All unicorns are white"--this statement is true for every single unicorn, of which there are none. Why do we consider this true rather than false? Because true is the identity element for the and operator (true and x = x for all x), just as 1 is the identity element for multiplication (1 * x = x for all x). (Similarly, false is the identity element for or, although we aren't using this fact in the example.)
• Each time through the loop, array[i] is set to 1, and i is incremented. So when we get back to the top of the loop, the invariant is once again true--it hasn't varied. The invariant may or may not be true at other locations within the loop, but when we get back to here, it's still true (or true again).

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

• Since (i < array.length) is false, not (i < array.length) is true, and this is more simply expressed as i >= array.length.

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.

• What does the condition (for all 0 <= j < i < array.length, array[j] = 1) and (i >= array.length) tell us?
• If array[j] = 1 is true for all 0 <= j < i , but i >= array.length, it follows that array[j] = 1 is true for all j < array.length.
• Therefore, for all 0 <= j < array.length, array[j] = 1. In words, this says that every element of the array is 1, which is what we wanted.

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.