loop invariant for simple algorithms

Question

The following is an algorithm which finds the maximum value in a list of integers, and I want to prove that it is correct by using a loop invariant.

algorithm max(list A[0..n − 1])
x ← A[0]
i ← 1
while i < n do
if A[i] > x then x = A[i]
i ← i + 1
return x

I really struggle when it comes to finding appropriate loop invariants, so any tips regarding this would also be appreciated.

Anyway, for the above algorithm I have (tentatively) come up with a loop invariant as follows:

$x \ge A[i-1]$

I am not sure how to actually use this to prove the correctness of the algorithm, or even if the invariant I have come up with is correct.

Answer 1

I'd use x == max(A[0..i-1]) as the loop invariant, positioned immediately after the increment to i (last line of while loop). To make it even easier to prove that the invariant holds on each pass through the loop, you can use more assertions within the loop body:

algorithm max(list A[0..n − 1])
x ← A[0]
i ← 1
while i < n do
    ## x == max(A[0..i-1])
    if A[i] > x then x = A[i]
    ## x == max(A[0..i]) 
    i ← i + 1
    ## x == max(A[0..i-1])

## x == max(A[0..n-1])
return x

It's then obviously true that once the loop has terminated, x == max(A[0..n-1]).

Answer 2

Your loop invariant is correct. To use it in a proof, you must say when it is correct and for which values it is correct. In your case, you begin with $x=A[0]$ so the loop invariant is true before each iteration of the loop. It is not enough to say $x\ge A[i-1]$ because that just says that $x$ is at least as big as it was on the last iteration. You must state that this is true for all previous $i$. In your case it is because of the transitivity of the ordering operation.

Then, after the last iteration, you conclude that $x\ge A[i-1]$ for all $i$ and therefore, $x$ must be the maximum.