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 $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:
Initially the subarray is the empty array, so proving it is trivial.
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.
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 $NIL$.