Correção e Invariantes

Objetivos de aprendizado

• Expressar um algoritmo como um contrato.
• Usar inicialização, manutenção e terminação para justificar um laço.
• Distinguir correção parcial de terminação.

Contratos

Uma pré-condição descreve entradas válidas. Uma pós-condição descreve o resultado necessário. Para um método que retorna o máximo de elementos:

• pré-condição: a sequência não está vazia;
• pós-condição: o valor retornado pertence à sequência e é maior ou igual a todo elemento nela.

Um algoritmo é parcialmente correto se sua pós-condição vale sempre que ele termina. É totalmente correto se for parcialmente correto e terminar para toda entrada satisfazendo sua pré-condição.

Um invariante de laço

Considere este método:

static int maximum(int[] values) {
    if (values.length == 0) {
        throw new IllegalArgumentException("values must not be empty");
    }

    int best = values[0];
    for (int i = 1; i < values.length; i++) {
        if (values[i] > best) {
            best = values[i];
        }
    }
    return best;
}

No início de cada iteração com índice i, use o invariante:

best é o máximo de values[0..i).

Inicialização: antes da primeira iteração, [0, 1) contém apenas values[0], portanto o invariante vale.

Manutenção: comparando values[i] com best produz o máximo do prefixo antigo mais o novo elemento. O invariante portanto vale para o próximo prefixo.

Terminação: quando i == values.length, o prefixo é todo o array, portanto o invariante implica a pós-condição.

O laço termina porque i aumenta e é limitado superiormente pelo comprimento finito do array. A função variante values.length - i é um inteiro não negativo que decresce estritamente.

Padrões de prova comuns

Construção	Argumento típico
Composição sequencial	A pós-condição do primeiro estabelece a pré-condição do segundo
Laço	Invariante mais uma função variante decrescente
Recursão	Caso base mais uma hipótese indutiva sobre entradas menores
Método guloso	Argumento de troca ou de que a solução se mantém à frente
Programação dinâmica	Indução sobre a ordem de dependência de subproblemas

Exercícios

1. Especificar um invariante útil para insertion sort.
2. Explicar por que "os testes passam" é evidência, mas não uma prova para todas as entradas.
3. Dar um argumento de correção parcial para um laço que pode nunca terminar.

Referências

Ver Cormen et al. e Hoare na bibliografia.