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

. 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 this0 <= j < 0 `true`

rather than`false`

? Because`true`

is the*identity element*for the`and`

operator( , just as`true and x = x for all x`

)`1`

is the identity element for multiplication( (Similarly,`1 * x = x for all x`

).`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

tell us?( for all 0 <= j < i < array.length, array[j] = 1 ) and(i >= array.length) - If

is true for allarray[j] = 1 `0 <= j < i`

, but`i >= array.length`

, it follows that

is true for allarray[j] = 1 `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.

Java has an `assert`

statement, with two forms:

assertboolean_expression; assertboolean_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 → `

, choose the *Your Application*`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`

`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`

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 }

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.