Consider the searching problem:
Input: A sequence of numbers and a value .
Output: An index such that or the special value if does not appear in .
Write pseudocode for linear search, which scans through the sequence, looking for . Using a loop invariant, prove that your algorithm is correct. Make sure that your loop invariant fulfills the three necessary properties.
1 2 3 4 5 for i = 1 to A.length if A[i] == v return i return NIL
Loop invariant for the pseudocode will be:
At the start of the each iteration of the for loop of lines 1-3, the subarray consists of the elements that are not equal to .
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 .
Maintenance: In -th iteration, we check whether is equal to or not. If yes, we terminate the loop or we continue the iteration. So, if the subarray did not contain before the -th iteration, the subarray will not contain before the next iteration (unless -th iteration terminates the loop).
Termination: The loop terminates in either of the following cases,
- We have found index such that = .
- We reached the end of the array, i.e. we did not find in the array . So, we return .
In either case, our algorithm does exactly what was required, which means the algorithm is correct.