Linear Search#
Contents#
Naive Linear Search#
Incremental/Iterative
INPUT an array A[0:n - 1] of n values where n >= 0 and a value x
OUTPUT either an index i such that A[i] = x or the special value NOT_FOUND when A does not contain x
LINEAR_SEARCH(A, n, x)
1 result = NOT_FOUND
2 for i = 0 to n - 1
3 if A[i] == x
4 result = i
5 return result
LINEAR_SEARCH(A, n, x)
1 result = NOT_FOUND
2 i = 0
3 while i < n
4 if A[i] == x
5 result = i
6 i++
7 return result
Complexity#
Naive linear search always iterates over all \(n\) values and doesn’t ever terminate early and so its running time is \(T(n) = \Theta(n)\).
Naive linear search does not use any auxiliary data structures other than a variable to store the output value and so its space requirement is \(S(n) = \Theta(1)\).
Correctness#
Invariant
At the start of iteration \(i\), if \(\texttt{result}\) is an index then \(A[\texttt{result}] = x\). Otherwise, \(x \not\in A[0:i - 1]\).
Initialization
\(i = 0\)
Prior to executing the loop, \(\texttt{result}\) is not an index and so it is true that \(x \not\in A[0:-1]\)
Maintenance
Assume that it is true that at the start of iteration \(i\), if \(\texttt{result}\) is an index then \(A[\texttt{result}] = x\). Otherwise, \(x \not\in A[0:i - 1]\).
Then it must be shown that at the start of iteration \(i + 1\), if \(\texttt{result}\) is an index then \(A[\texttt{result}] = x\). Otherwise, \(x \not\in A[0:i]\).
CASE 1. If \(\texttt{result}\) is an index and \(A[\texttt{result}] = x\) at the start of iteration \(i\), then this continues to hold at the start of iteration \(i + 1\).
CASE 2. At the start of iteration \(i + 1\), if \(A[i] = x\) then \(\texttt{result} = i\) and \(A[\texttt{result}] = x\).
CASE 3. At the start of iteration \(i + 1\), if \(A[i] \ne x\) then \(x \not\in A[0:i - 1] \cup A[i] = A[0:i]\).
Termination
\(i = n\)
If \(\texttt{result}\) is an index then \(A[\texttt{result}] = x\). Otherwise, \(x \not\in A[0:n - 1]\).
Linear Search#
Incremental/Iterative
INPUT an array A[0:n - 1] of n values where n >= 0
OUTPUT either an index i such that A[i] = x or the special value NOT_FOUND when A does not contain x
LINEAR_SEARCH(A, n, x)
1 for i = 0 to n - 1
2 if A[i] == x
3 return i
4 return NOT_FOUND
LINEAR_SEARCH(A, n, x)
1 i = 0
2 while i < n
3 if A[i] == x
4 return i
5 i++
6 return NOT_FOUND
Complexity#
Linear search iterates over \(n\) values in the worst case and so its worst case running time is \(T(n) = O(n)\). In the best case, it iterates over a single value and so its best case running time is \(T(n) = O(1)\).
Linear search does not use any auxiliary data structures other than a variable to store the output value and so its space requirement is \(S(n) = \Theta(1)\).
Correctness#
Precondition
\(A\) is an array of \(n\) values where \(n \ge 0\)
\(i = 0\)
Postcondition
\(x = A[i]\) or \(x = \texttt{NOT\_FOUND}\)
Condition
\(x \ne A[i]\) and \(i \lt n\)
Invariant
\(0 \le i \le n\)
\(x \in A[i:n-1] \cup \{ \texttt{NOT\_FOUND} \}\)
If \(x \in A\) then \(x \in A[i:n - 1]\). If \(x \not\in A[i:n - 1]\) then \(x \not\in A\).
\(x \not\in A[0:i - 1]\)
Variant
\(n - i\)
Initialization
It must be shown that if the \(\texttt{precondition}\) is true then the \(\texttt{invariant}\) is true.
Prior to the first iteration of the loop, \(i = 0\) and \(n \ge 0\) and so the inequality \(0 \le i \le n\) holds. Further it is true that \(x \in A[i:n - 1] \cup \{ \texttt{NOT\_FOUND} \}\) since \(A[i:n - 1]\) is just the entire array.
Maintenance
It must be shown that if both the \(\texttt{condition}\) is true and the \(\texttt{invariant}\) is true prior to iteration \(i\) then the \(\texttt{invariant}\) is true prior to iteration \(i' = i + 1\).
\(i \lt n \iff i + 1 \le n\)
At the start of each iteration, if \(x \in A\) then \(x \in A[i:n - 1]\).
If the algorithm does not return then \(A[i] \ne x\) and so if \(x \in A\) then \(x \in A[i + 1:n - 1]\).
Postcondition
It must be shown that if both the \(\texttt{condition}\) is false and the \(\texttt{invariant}\) is true then the \(\texttt{postcondition}\) is true.
The negation of the condition states \(\lnot(i \lt n) \iff i \ge n\) and the invariant states \(i \le n\) and so it must be the case that \(i = n\).
If \(x \not\in A[i:n - 1]\) then \(x \not\in A\).
\(\underbrace{x \not\in A[n:n - 1]}_{\text{always true}}\)
Therefore \(x \not\in A\) and so \(x = \texttt{NOT\_FOUND}\)
Termination
Up to now it has been shown that if the loop eventually terminates then the algorithm is correct. It must now be shown that the loop eventually terminates.
Acknowledgments#
02-08-2021. Algorithms Lab. “Loop Invariant Proofs (proofs, part 1)”. https://www.youtube.com/watch?v=_maJ4Qy7Q0E.