Invariantes de laço e corretude

Um invariante de laço é uma afirmação que vale antes de cada iteração. Provar que o código está correto se resume a três passos:

Inicialização:  o invariante vale antes da 1ª iteração
Manutenção:     se vale antes de uma iteração, vale depois dela
Término:        quando o laço para, invariante + condição de parada ⇒ resultado correto

Repare que isso é indução sobre o número de iterações.

Exemplo: busca binária

def busca(xs, alvo):
    lo, hi = 0, len(xs)          # intervalo semiaberto [lo, hi)
    # Invariante: se alvo está em xs, está em xs[lo:hi]
    while lo < hi:
        mid = (lo + hi) // 2
        if xs[mid] < alvo:
            lo = mid + 1         # alvo não está em xs[:mid+1]
        elif xs[mid] > alvo:
            hi = mid             # alvo não está em xs[mid:]
        else:
            return mid
    return -1                    # intervalo vazio: alvo não está em xs

Terminação: a quantidade hi − lo é um inteiro não negativo que diminui estritamente a cada volta. Uma quantidade assim se chama variante (ou função de limite) e garante que o laço termina.