1
$\begingroup$

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.

Improve this question
$\endgroup$

3 Answers 3

Reset to default
7
$\begingroup$

What about using a "goal" variable initialized to NIL and taking as invariant "After iteration i, the goal variable contains an index $0 \leq j < i$ such that $A[j] = v$ if there exists one (in the range $\{0, \cdots, i - 1\}$), or NIL otherwise" ?

Improve this answer
$\endgroup$
1
  • $\begingroup$ The invariant can be weakened to avoid assuming a specific traversal order. Let $V_i$ the set of the indexes of the elements that have been looked at after $i$ iterations, then the condition $0\le j<i$ becomes $j\in V_i$. $\endgroup$
    – Yves Daoust
    Jan 6 at 14:52
1
$\begingroup$

It's impossible to prove unless you state the algorithm. But, let's say your algorithm maintain a candidate index $j$ for loop iteration, which is update to $j \leftarrow j+1$, if $v_j \neq v$, and if the loop termination depends on $j$ not updating or reaching $n$ and the output is $j$, then you could say that a valid loop invariant is $v_i \neq v_j$ for $1 \leq i < j \le n $.

Improve this answer
$\endgroup$
0
$\begingroup$

So the Initialization condition would be that v is not in our sub array which at the beginning we would consider to be empty.

Then maintenance would be that as we add elements v is not in our sub array still as if we find it we go to termination so we keep iterating if v is not there

The termination would be if we find v or if we reach the end of the array here the meaning full out put is either the index of v or that the counter equals the size of the array From what I gather

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.