Question

Consider the following algorithm, which will sum the values in an integer array a[ ], and in particular sum = a[0] + a[1] + ... + a[length-1].

sum = 0

k = 0

while k < length

sum = sum + a[k]

k = k + 1

Prove that the algorithm will have sum = a[0] + a[1] + ... + a[length-1] using a loop invariant for the while loop. For the proof, answer the following questions, and do the subsequent steps.

What is the loop invariant predicate P(k)?

Answer 1

The loop invariant predicate P(k) is that at the start of each iteration of the loop, the variable 'sum' contains the sum of the first 'k' elements of the array.

Step-by-step explanation:

To prove this, we need to show that P(k) holds before the loop starts (at k=0), and that if P(k) holds before an iteration of the loop, then it also holds after that iteration. For the base case, P(0) is true because 'sum' is initialized to 0.

For the induction step, let's assume that P(k) holds before an iteration. After the iteration, 'sum' is updated by adding the value of 'a[k]' to it.

So the new value of 'sum' becomes the sum of the first 'k+1' elements of the array, which satisfies P(k+1). Therefore, P(k) → P(k+1) holds for any iteration of the loop.

Since P(k) is true before the loop starts and holds after each iteration, it is a loop invariant. This means that when the loop terminates (when k = length), P(k) still holds.

Therefore, at the end of the loop, 'sum' will contain the sum of all elements in the array, which is the desired result.