Discrete Mathematics for Computer Science

142 CHAPTER 2 Formal Logic

A formula that states this property is intuitively easy to understand, but it is not so easy

to state formally. Part of the formula is that after k passes through the outer loop, the last

k elements (in positions N - k, N - k + 1 ... , N - 1) are in increasing order and are

larger than or equal to all elements of the array that occur in positions 0, 1 .... k - 1. We

can state more, since the elements in positions k, k + 1 .... j - 1 also have values that

are less than the value of the element at position j. Thus, for any position j among the last

k positions, the value in each position i where 0 < i < j is less than or equal to the value

in position j.

Let Ind denote the set {0, 1. N - 11 of legal indices for array A:

Vi E IndVj E Ind((O < i) A (i < j) A (j > (N - k)) -- (A[i] < A[j])

For k = 0, this says that

Vi E IndVj E Ind(i < j A j > N -* A[i] < A[j])

which is a true predicate, because j > N is false, making this an implication with hypothe-

sis FALSE. When k = N - 1, we are claiming that all the elements are in increasing order.

The predicate is

Vi E IndVj E Ind(i < j A j > 0 -+ A[i] < A[j])

The reader should verify that this does mean that the elements of the array are in increasing

order. This predicate can be put into the code as a comment called a loop invariant assertion,

as seen in the Outer Loop Invariant algorithm. (We now go back to informal usage and use

both the < and the < symbol in the formula.)

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

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

for limit = N - 2 down to 0

/* loop invariant for limit loop

Vi E IndVj e Ind((i < j A j > limit + 1) -) (A[i] < A[j]))

*/

for position = 0 up to limit

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

swap the values

When limit = N - 2, j > N - 1 is false, because 0 < j < N - 1. Therefore, the im-

plication is TRUE. When limit = -1 and the loop terminates, the implication says that,