[Math] 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]).