Discrete Mathematics for Computer Science

Predicates and Quantification 141

Note that in two of the lines in Table 2.10 we said "." and that in two we said just

"=." We leave it for the reader to find examples of the following:

(3x P(x)) A (3x Q(x)) A --3x (P(x) A Q(x))

and Vx (P(x) V Q(x)) A --(Vx P(x)) V (Vx Q(x))

2.77 Application: Loop Invariant Assertions

One of the most difficult aspects of computer programming is establishing whether pro-

grams produce the correct output. In principle, there is no way to establish the correctness

of all correct programs. (This was proved by Alan Turing.) Tools for establishing correct-

ness, however, do exist for many programs.

The simplest method for checking a program is to test it: Run it on some sample

values, and check whether it produces the correct answers. Testing is often an effective

method for showing that a program is incorrect, but unfortunately, one cannot normally

check all possible inputs-nor even a significant fraction of the possible inputs. Therefore,

one cannot check that a program is correct.

Another method that is often useful is to write a mathematical proof of program cor-

rectness. One of the difficulties in this case is finding tools for proving that any loops

accomplish what they are supposed to.

A somewhat similar problem is encountered in making it obvious to someone else

who is reading the program that the program works correctly. Many algorithms use tricks

that vary from not quite obvious to totally obscure. What is an easy read and short way to

present the trick and explain why the algorithm works? For example, how can one explain

what a loop is accomplishing?

One method that is often useful employs loop invariant assertions. We will explain

these in terms of a familiar algorithm, (one version of the) BubbleSort. We choose Bubble-

Sort not because it is a good sorting algorithm-for most purposes, it definitely is not-but

because it is short and easy to understand.

INPUT: An array A [ 0. .N - 1I] of N integers

OUTPUT: The same array, with its elements sorted into nondecreasing order

for limit = N - 2 down to 0

for position = 0 up to limit

if (A [position ] > A [position + 1 1)

then swap the values of A [position ] and A [position + 1]

A reason this algorithm works is that after k passes through the outer loop, the largest
k elements have reached the last k positions in the array-and in the correct order as well.