Correctness on iterative and recursive processes

Iterative processes are proven using loop invariants, and recursive processes are proven using induction. In some cases it might be trickier to find a good loop invariant, where proving recursive processes is just to follow the very own definitions of the process.

Consider the following recursive definition:

maxList [x] = x
maxList (x:xs) = max(x, maxList xs)

We can prove its correctness using induction:

– Base case: Max element of a list of size 1 is the element itself.

– Inductive step: Assume that maxList of xs is maximum element.

Then for maxList (x:xs) we have 2 cases:
1. maxList of xs is >= x, in which case we select maxList xs
2. x is >= maxList xs, in which case we select x
In either case, we pick the larger element which will be the maximum.

Now consider the following iterative definition:

var max = x[0], i;

for (i = 0; i < x.length; i++) {
     if (x[i] >= max) max = x[i];
}

In this case we need to find a loop invariant to use that will hold pre-, during, and post- processing of that code block.

We can use the following loop invariant: max is the biggest element in the subarray x(0, i).

– Before loop: for array of size 1 we have the same element to be maximum. So the loop invariant holds.

– Within the loop, we have two cases:
1. x[i] >= max, in which we set max to be x[i]
2. x[i] < max, in which we don't change max
In either case, the loop invariant holds.

– After loop: max is the biggest element in the subarray x(0, x.length – 1) which is just x.