Consider the search problem:
Input: A sequence of $n$ numbers $A=(a_1, a_2, \ldots , a_n)$ and a value $v$.
Output: An index $i$ such that $v = a_i$ or the special value 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.
The algorithm is clearly very simple to prove. However, could someone prove the correctness of the algorithm using a loop invariant? Note the "three necessary properties" are:
Initialization: It is true prior to the first iteration of the loop.
Maintenance: If it is true before an iteration of the loop, it remains true before the
Termination: When the loop terminates, the invariant gives us a useful property that helps show that the algorithm is correct.