When no further information is given about the searched data, the obvious approach is to proceed sequentially through the array in order to increase step by step the size of the section, where the desired element is known not to exist. This approach is called linear search. There are two conditions which terminate the search:
1. The element is found, i.e. ai = x.
2. The entire array has been scanned, and no match was found.
This results in the following algorithm:
i := 0;
WHILE (i < N) & (a[i] # x) DO INC(i) END Note that the order of the terms in the Boolean expression is relevant. The invariant, i.e the condition satisfied before each incrementing of the index i, is
i < N) & (Ak : 0
k < i : ak
expressing that for all values of k less than i no match exists. From this and the fact that the search terminates only if the condition in the while-clause is false, the resulting condition is derived as
((i = N) OR (ai = x )) & (Ak : 0 < k < i : ak
This condition not only is our desired result, but also implies that when the algorithm did find a match, it found the one with the least index, i.e. the first one. i = N implies that no match exists.
Termination of the repetition is evidently guaranteed, because in each step i is increased and therefore certainly will reach the limit N after a finite number of steps; in fact, after N steps, if no match exists.
Each step evidently requires the incrementing of the index and the evaluation of a Boolean expression. Could this task be simplifed, and could the search thereby be accelerated? The only possibility lies in finding a simplification of the Boolean expression which notably consists of two factors. Hence, the only chance for finding a simpler solution lies in establishing a condition consisting of a single factor that implies both factors. This is possible only by guaranteeing that a match will be found, and is achieved by posting an additional element with value x at the end of the array. We call this auxiliary element a sentinel, because it prevents the search from passing beyond the index limit. The array a is now declared as
a: ARRAY N+1 OF INTEGER
and the linear search algorithm with sentinel is expressed by
a[N] := x; i := 0;
WHILE a[i] # x DO INC(i) END
The resulting condition, derived from the same invariant, i = N implies that no match (except that for the sentinel) was encountered.