Projeto de Algoritmos | Índice Remissivo

Invariantes da busca sequencial

[Enunciado]  A seguinte função recebe um inteiro x e um vetor crescente v[0..n-1] e devolve um índice j em 0..n tal que v[j-1] < x <= v[j]:

int buscaSequencial (int x, int n, int v[]) {
   int j = 0;
   while (/*A*/ j < n && v[j] < x) 
      ++j;
   return j;
}

O valor de j muda a cada iteração, mas as relações   j ≤ n  e  v[j-1] < x   são invariantes: elas valem no início de cada iteração.  Mais precisamente, essas relações invariantes valem imediatamente antes de cada comparação de j com n (ponto A do código).

No começo da primeira iteração, as relações valem se estivermos dispostos a imaginar que v[-1] é −∞.

As relações invariantes valem, em particular, no início da última iteração, quando  j ≥ n  ou  v[j] ≥ x.

• No primeiro caso, temos j == n e v[n-1] < x.  A função devolve n, que é a resposta correta.
• No segundo caso, temos j < n e v[j-1] < x ≤ v[j].  A função devolve j, que é a resposta correta.

Essa discussão mostra que a função buscaSequencial está correta.