Algorithms Design | Index

Invariant of the find function

[Statement of the exercise]

int find (int x, int n, int v[]) {
   int k = n-1;
   while (/*A*/ k >= 0 && v[k] != x)  
      k -= 1;
   return k; 
}

At the beginning of each iteration, i.e., every time the execution goes through point A, the following property holds:

x  is different from every element of  v[k+1..n-1].

Exercises:

• Prove (by induction) that the stated invariant is correct.
• Use the invariant to prove that the algorithm is correct.