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.