Um invariante de um processo iterativo é uma relação entre os valores das variáveis que
vale no início de cada iteração e
não se altera de uma iteração para outra. (Um invariante é essencialmente o mesmo que uma hipótese de indução numa prova por indução matemática.) Essas relações invariantes explicam o funcionamento do processo iterativo e permitem provar, por indução, que o processo tem o efeito desejado.
Um exemplo: O algoritmo Máximo recebe um número n ≥ 1 e um vetor A e devolve o valor de um elemento máximo de A[1 .. n]:
Máximo (A, n) |
1 . x := A[1] |
2 . para i crescendo de 2 até n faça |
3 .ooo se x < A[i] |
4 .oooooo então x := A[i] |
5 . devolva x |
Invariante: no início de cada iteração, imediatamente antes da comparação de i com n,
x é um elemento máximo de A[1 .. i−1].
É essencial dizer em que ponto do código, exatamente, o invariante está sendo observado.
Segue daí imediatamente que no início da última iteração (quando i vale n+1) x é um elemento máximo de A[1 .. n] e portanto o algoritmo está correto.