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   jn  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.

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