Consider the searching problem:

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

Output: An index \(i\) such that \(v = A[i]\) or the special value \(\text {NIL}\) if \(v\) does not appear 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.

For linear search, we just need to scan the array from the beginning till the end, index \(1\) to index \(n\), and check if the entry at that position equal to \(v\) or not. The pseudocode can be written as follows…

$$\textsc{Linear-Search}(A, v)$$$$\begin{aligned} 1& \quad \textbf{for }\,i\,=\,1\textbf{ to }\,A.length \\ 2& \quad \qquad \textbf{if }\,A[i]\,=\,v \\ 3& \quad \qquad \qquad \textbf{return }\,i \\ 4& \quad \textbf{return }\,\textsc{NIL} \\ \end{aligned}$$

Loop Invariant

At the start of the each iteration of the for loop of lines 1-3, the subarray \(A[1 .. i − 1]\) does not contain the value \(v\).

And here is how the three necessary properties hold for the loop invariant:

Initialization: Initially the subarray is empty. So, none of its’ elements are equal to \(v\).

Maintenance: In \(i\)-th iteration, we check whether \(A[i]\) is equal to \(v\) or not. If yes, we terminate the loop or we continue the iteration. So, if the subarray \(A[1..i - 1]\) did not contain \(v\) before the \(i\)-th iteration, the subarray \(A[1..i]\) will not contain \(v\) before the next iteration (unless \(i\)-th iteration terminates the loop).

Termination: The loop terminates in either of the following cases,

  • We have reached index \(i\) such that \(v\) = \(A[i]\), or
  • We reached the end of the array, i.e. we did not find \(v\) in the array \(A\). So, we return \(\text {NIL}\).

In either case, our algorithm does exactly what was required, which means the algorithm is correct.


Archived Comments

These comments were imported from the previous Disqus comment system.

bernie_haxx Jan 13, 2025
Hi, I was asking about this statement on the maintenance part of the loop schema, does the subarray \(A[1..i]\) may or may not contain the value \(v\) before the next iteration? Like the last portion, cause it doesn't make sense if \(A[1..i]\) is the unchecked subarray.