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] and a value v

Output: Index i, where A[i] = v or NIL if v does not found in A

Write 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, iterating over j, starting at j = 2, the A[1..j-1] elements are always sorted. This makes sense to 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

LINEAR-SEARCH(A, ν) 1  for i = 1 to A.length 2      if A[i] == ν  3          return i 4  return NIL  

Loop invariant: at the start of the ith iteration of the for loop (lines 1–4),

∀ k ∈ [1, i) A[k] ≠ ν.   

Initialization:

i == 1 ⟹ [1, i) == Ø ⟹ ∀ k ∈ Ø A[k] ≠ ν, 

which is true, as any statement regarding the empty set is true (vacuous truth).

Maintenance: let's suppose the loop invariant is true at the start of the ith iteration of the for loop. If A[i] == ν, the current iteration is the final one (see the termination section), as line 3 is executed; otherwise, if A[i] ≠ ν, we have

∀ k ∈ [1, i) A[k] ≠ ν and A[i] ≠ ν ⟺ ∀ k ∈ [1, i+1) A[k] ≠ ν, 

which means that the invariant loop will still be true at the start of the next iteration (the i+1th).

Termination: the for loop may end for two reasons:

1. return i (line 3), if A[i] == ν;

2. i == A.length + 1 (last test of the for loop), in which case we are at the beginning of the A.length + 1th iteration, therefore the loop invariant is

   ∀ k ∈ [1, A.length + 1) A[k] ≠ ν ⟺ ∀ k ∈ [1, A.length] A[k] ≠ ν 

   and the NIL value is returned (line 4).

In both cases, LINEAR-SEARCH ends as expected.

Answer 2

After you have looked at index i, and not found v yet, what can you say about v with regard to the part of the array before i and with regard to the part of the array after i?