Loop invariant of linear search

Question

As seen on Introduction to Algorithms (http://mitpress.mit.edu/algorithms), the exercise states the following:

Input: Array A[1...n]

Output: i, where A[i]=v or NIL when not found

Write a pseudocode for LINEAR-SEARCH, which scans through the sequence, looking for v. Using a loop invariant, prove that your algorithm is correct. (Make sure that your loop invariant fulfills the three necessary properties – initialization, maintenance, termination.)

I have no problem creating the algorithm, but what I don't get is how can I decide what's my loop invariant. I think I understood the concept of loop invariant, that is, a condition that is always true before the beginning of the loop, at the end/beginning of each iteration and still true when the loop ends. This is usually the goal, so for example, at insertion sort, itearting over j, starting at j=2, the [1, j-1] elements are always sorted. This makes sense for me. But for a linear search? I can't think of anything, it just sounds too simple to think of a loop invariant. Did I understand something wrong? I can only think of something obvious like (it's either NIL or between 0 and n). Thanks a lot in advance!

Answer 1

Loop invariant would be

forevery 0 <= i < k, where k is the current value of the loop iteration variable, A[i] != v

On loop termination:

if A[k] == v, then the loop terminates and outputs k

if A[k] != v, and k + 1 == n (size of list) then loop terminates with value nil

Proof of Correctness: left as an exercise