Algorithm design problem set

LE/EECS3101: Design and Analysis of Algorithms

Weekly Digest

Week 1: Iterative Algorithms & Loop Invariants

1 Iterative algorithms

Almost any algorithm, including iterative ones, maintains information about the state of the computation throughout its execution. In each iteration, an iterative algorithm makes one move that modifies the state of the compu- tation and brings the algorithm closer to its destination and exit condi- tion.

• In FindMax, the state of the computation is the variable max that holds the maximum element seen so far, and the loop index i that tells the algorithm which element it should check next. In each iteration, FindMax compares the element at i with the maximum element seen so far, max, and updates max if necessary.

• In BinarySearch, the state of the computation are the two indices i and j that define the sub-array that the algorithm is searching for key in. In each iteration, and assuming key is not found at the middle of the sub-array, BinarySearch modifies i and j to point to a new sub-array that contains key if key is in the input array.

2 Preconditions, Postconditions, and Loop Invari- ants

• A precondition is an assertion about the state of the program before the execution of the loop (i.e., before the first iteration).

• A postcondition is an assertion about the state of the program after the execution of the loop (i.e., after the last iteration).

• A loop invariant is an assertion about the state of the program before each iteration of the loop. A loop invariant allows us to explicitly

1

specify the assumptions that each iteration of the loop body makes about the state of the program.

In FindMax, the loop searches for the maximum element in A[2..n]. Before the execution of the first iteration, the loop assumes that A[1] is the maxi- mum. The precondition must therefore state that max holds the first element of the array.

The postcondition simply states what is true after the execution of the loop. This is typically the goal of the computation. In the case of FindMax the postcondition is simply that max holds the largest element in the array.

Each iteration in FindMax makes an assumption that is necessary for the correct computation of that iteration. Each iteration assumes that max holds the maximum element seen so far in the array, and compares that against the next element in the array, A[i]. That is exactly the loop invariant, i.e., max holds the maximum in A[1..i-1]. Each iteration of the loop is responsible for maintaining the loop invariant for the next iteration. The ith-1 iteration must update max if necessary so that the loop invariant holds in the ith iteration.

3 Correctness

An algorithm is correct if (1) it terminates, and (2) <precondition> ∧ <algorithm> =⇒ <postcondition>. That is it, an algorithm is correct if whenever the precondition holds, the postcondition also holds.

Proving the correctness of an iterative algorithm can be done by proving the correctness of its loop invariants. Proving the correctness of a loop invariant requires proving three things:

• Initialization: prove that the loop invariant (LI) is true before the first iteration, i.e., LI(1) is true. Here, preconditions are often useful.

• Maintenance: prove that the loop invariant is true before each iter- ation. This can be done by assuming that the loop invariant is true for the ith-1 iteration (i > 1), and showing how the code maintains, or re-establishes, the loop invariant for the ith (next) iteration. That is LI(i-1) =⇒ LI(i) for all i > 1.

• Termination: prove that the loop terminates and that the loop in- variant implies the postcondition. Proving that the loop terminates can be trivial when the termination condition is simple (e.g., typical for loops). Some extra effort might be required when the termination condition is not very obvious (e.g., binary search). Once we establish that the loop terminates, we show how the loop invariant of the last iteration implies the postcondition. That is LI(n) =⇒ postcondition.

2

Why does this work?

Correctly proving the initialization of a loop invariants proves that <precondition> =⇒ L(1). The maintenance phase of the proof proves that LI(i-1) =⇒ LI(i) for all i > 1. Proving the initialization and maintenance shows that L(1) =⇒ L(2) =⇒ ... =⇒ L(n) where n is the number of iterations. We call this partial correctness.

The termination phase proves full correctness: (1) that the algorithm ter- minates, and (2) the loop invariant implies the postcondition. In the end, proving all three stages gives us L(1) =⇒ L(2) =⇒ ... =⇒ L(n) =⇒ postcondition.

3