Observações sobre invariantes

Esta página trata do conceito de invariantes no contexto de algoritmos iterativos.  Veja também a página Documentação em Algoritmos em C.

Conceitos básicos

• O que é um invariante de um processo iterativo?  Relação entre os valores de variáveis que vale no início de cada iteração e não se altera de uma iteração para outra.
• De onde vem o nome invariante?
• Para que servem invariantes?  Para provar, por indução, que o processo iterativo está correto.
• Invariantes são análogos às hipóteses de indução em provas por indução matemática.
• Um invariante vale em qualquer lugar do processo iterativo?  Não! Só num ponto específico.
• O que são invariantes de um algoritmo recursivo?  Não faz sentido.
• Existem invariantes fora de um processo iterativo?  Não.
• Exemplo. O seguinte método devolve um elemento máximo de um vetor não vazio v:

          public int max(int[] v) { 
              int n = v.length;
              int j, x = v[0];
              for (j = 1; j < n; j++)
                  if (x < v[j]) x = v[j];
              return x;
          }
  

• Certo ou errado?  Aqui está o invariante:   x  é o maior elemento da parte do vetor  v  vista até agora.  Errado.  Isso não é um invariante porque
  • não especifica o ponto do código a que se refere;
  • envolve a ideia de tempo (ao dizer até agora).

  Invariantes devem ser estáticos, parados no tempo.  Um invariante é análogo a uma foto e não a um filme.

• Invariante correto para o processo iterarivo for no exemplo acima:  no início de cada iteração,  x  é um elemento máximo de  v[0..j-1].
• Onde fica esse início de cada iteração?  Imediatamente antes do ponto em que o código decide se o processo iterativo deve parar ou continuar.
• Exemplo: o início de cada iteração fica no ponto  A  e não no ponto ponto  B:

          public int max(int[] v) { 
              int n = v.length;
              int j, x = v[0];
              for (j = 1; /*A*/ j < n; j++)
                  /*B*/ if (x < v[j]) x = v[j];
              return x;
          }
  

  Quanto vale j no início da última iteração?  Errado: j vale n-1.  Certo: j vale n.

• Continuação do exemplo: No fim do processo iterativo temos j == n.  Portanto, deduzimos do invariante que, no fim do processo iterativo,  x  é o maior elemento de v[0..n-1], ou seja, o maior elemento do vetor v todo.

  O invariante serve para levar a essa conclusão, e só para isso.

Exemplo: busca em vetor

• O que o seguinte método devolve?

       public int busca(int x, int[] v) {
          int n = v.length;
          int k = n - 1;
          while (k >= 0 && v[k] != x)  
             k -= 1;
          return k; 
       }
  

• Resposta: Devolve um índice k tal que v[k] == x.  Se tal k não existe, devolve -1.
• Resposta mais detalhada: Devolve o maior k no conjunto 0..n-1  (sendo n o número v.length)  tal que v[k] == x.  Se tal k não existe, devolve -1.

Quais são os invariantes do método busca( )?

• Resposta correta:   no início de cada iteração,  x é diferente de todos os elementos de v[k+1..n-1].
• Respostas erradas::
  • no começo da linha 5,  x é diferente de v[k]
  • na linha 4,  x é diferente de todos os elementos de v[k+1..n-1]
  • na linha 5,  x é diferente de todos os elementos de v[k..n-1]
  • na linha 5,  x é diferente de todos os elementos de v[k+1..n-1]
  • no começo de cada iteração,  x é diferente de todos os elementos de v[k..n-1]
  • na linha 4,  x não está entre as posições do vetor k e n-1
  • x pode estar entre v[0..k]
  • k será um valor no intervalo -1..n-1
  • k é sempre ≥ 0 quando existe x no vetor
  • n é o tamanho do vetor v
  • na linha 6,  k+1 até n-1 não contém x

O conjunto de invariantes deve estar completo

• Os invariantes de um processo iterativo só servem para uma coisa:  provar que o processo iterativo está correto (ou seja, faz o que dele se espera).
• Os invariantes devem ser suficientes para provar que o processo está correto.
• A propriedade  no início de cada iteração tem-se  -1 ≤ k < n  no exemplo acima é um invariante correto, mas ela não é suficiente para provar que o processo iterativo está correto.
• Exercício: No exemplo acima, é verdade que no início de cada iteração tem-se 0 ≤ k < n?  Não. No início da última iteração k pode ser negativo.