Invariantes

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.