1 key = 1 2 for i = 2 to A.length 3 if A[i] < A[key] 4 key = i

... initialization?

... termination?

Prove loop invariant holds at initialization, mantenance, and termination.