Exercise 2.1.3

Consider the searching problem:

Input: A sequence of $ n $ numbers $ A = \langle a_1, a_2, \ldots, a_n \rangle $ and a value $\nu$.

Output: And index $i$ such that $ \nu = A[i] $ or the special value $\mathrm{NIL}$ if $\nu$ does not appear in $A$

Write the pseudocode for linear search, which scans through the sequence, looking for $\nu$. Using a loop invariant, prove that your algorithm is correct. Make sure that your loop invariant fulfills the three necessary properties.

The pseudocode looks like this:

SEARCH(A, v):
  for i = 1 to A.length
      if A[i] == v
          return i
  return NIL

I'm going to state the loop invariant as:

At the start of each iteration of the for loop, the subarray $A[1..i - 1]$ consists of elements that are different than $\nu$.

Here are the three properties:

Initialization

Initially the subarray is the empty array, so proving it is trivial.

Maintenance

On each step, we know that $A[1..i-1]$ does not contain $\nu$. We compare it with $A[i]$. If they are the same, we return $i$, which is a correct result. Otherwise, we continue to the next step. We have already insured that $A[A..i-1]$ does not contain $\nu$ and that $A[i]$ is different from $\nu$, so this step preserves the invariant.

Termination

The loop terminates when $i > A.length$. Since $i$ increases by $1$ and $i > A.length$, we know that all the elements in $A$ have been checked and it has been found that $\nu$ is not among them. Thus, we return $\mathrm{NIL}$.