Projeto de Algoritmos | Índice Remissivo

Invariante da função busca

[Enunciado do exercício]

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

No início de cada iteração, ou seja, a cada passagem pelo ponto A, temos a seguinte propriedade invariante:

x  é diferente de todos os elementos de  v[k+1..n-1].

Exercícios:

• Prove (por indução) que a propriedade invariante está correta.
• A partir do invariante, prove que o algoritmo está correto.