Verificação do programa: testes de software e Tripla de Hoare

A verificação do programa garante (ou tenta garantir) que um programa de computador está correto. Ela pode ser feita por meio de testes ou da demonstração de correção.

Um programa está correto se ele se comporta de acordo com as especificações atribuídas a ele. Isso não significa que ele resolve o problema que se pretendia resolver: as especificações podem, por exemplo, não prever todas as necessidades originais do cliente.

Os testes tentam mostrar que, dados alguns valores de entrada, o software produz as saídas esperadas. É uma abordagem empírica, muito usada no dia a dia do desenvolvimento de software. Mas, como diz um ditado comum na área, “os testes provam a existência de erros, mas nunca sua ausência”. Sempre pode haver algum bug escondido no código, à espera do momento de aparecer.

Já a demonstração de correção usa técnicas de lógica formal. Ela prova que, se as variáveis de entrada satisfazem certos predicados (ou propriedades) especificados, então as variáveis de saída, resultado da execução do programa, satisfazem outras propriedades especificadas. Assim, o programa pode ser considerado totalmente correto, desde que obedeça às condições das especificações. Uma técnica comum para essa demonstração é a Tripla de Hoare, que veremos na próxima seção.

Todos os softwares passam por testes (ou deveriam passar), mas nem todos passam pela demonstração de correção, que costuma ser usada em trechos pequenos e críticos do código. As duas abordagens são complementares na verificação de um programa.

Tripla de Hoare

De maneira simplificada, a Tripla de Hoare pode ser entendida assim:

• Ela tem o formato {Q} P {R}, em que Q é a pré-condição do programa P e R é a pós-condição.
• Se a pré-condição Q é verdadeira antes da execução de P, então a pós-condição R será verdadeira depois que P terminar.
• A tripla pode ter predicados intermediários, além da condição inicial (Q) e da final (R). Esses predicados são chamados de asserções e afirmam o que deve ser verdadeiro sobre as variáveis do programa em um determinado ponto.

A imagem abaixo mostra uma Tripla de Hoare com várias asserções:

O programa da imagem só pode ser demonstrado correto se todas as condições forem válidas.

Para facilitar o entendimento, vejamos alguns exemplos práticos em Go.

Exemplos de aplicação

A função abaixo retorna um booleano que indica se o número é par (true) ou não (false):

// EPar retorna se um inteiro recebido é par
func EPar(x int) bool {
    return x%2 == 0
}

As especificações com a Tripla de Hoare são as seguintes:

• Pré-condição (Q): true, a função aceita qualquer inteiro.
• Programa (P): result := x % 2 == 0.
• Pós-condição (R): result == true ⟺ x é par (o símbolo ⟺ lê-se “se e somente se”).

Como a função EPar(x) não tem restrições para o valor de x (desde que seja inteiro, claro), a pré-condição Q é simplesmente true. O comando result := x % 2 == 0 calcula o resto da divisão de x por 2, compara com 0 e armazena o booleano em result. Em R, result deve ser true quando x for par.

De fato, todo número que, dividido por 2, tem resto 0 é par. Portanto, a comparação em P resulta em true quando x é par e em false caso contrário.

A função pode ser formalizada assim:

{true} result := x % 2 == 0 {result = true ⟺ x é par}

O exemplo é simples e pode fazer parecer “desnecessário” ou “trivial” demonstrar sua correção, mas não é. Essa demonstração diz que, independentemente do valor de entrada, a função retorna true se e somente se x é par. Isso prova sua correção para qualquer inteiro.

Veja outro exemplo:

// calcula a soma dos números de 1 a n
func sumToN(n int) int {
    sum := 0
    for i := 1; i <= n; i++ {
        sum += i
    }
    return sum
}

As especificações com a Tripla de Hoare ficam assim:

• Pré-condição (Q): n ≥ 0.
• Programa (P): o corpo da função sumToN.
• Pós-condição (R): sum = n*(n+1)/2.

Essa soma só faz sentido para inteiros não negativos, já que não se pode somar de 1 até um número negativo. Por isso, em Q assume-se que n ≥ 0.

Em P, sum começa em 0 e o laço vai de 1 até n e acumula os valores em sum += i. Ao final, a função retorna sum, que deve ser igual a n*(n+1)/2, a fórmula clássica da soma de 1 até n.

Com indução matemática, provam-se as operações da função. A função sumToN pode ser formalizada assim:

{n ≥ 0} sumToN(n) {sum = n × (n+1)/2}

Ou seja, a função é totalmente correta para qualquer inteiro não negativo.

Testes e demonstração se complementam

O teste de software e a demonstração de correção são úteis e não se excluem. O primeiro é prático e rápido, e pode e deve ser usado em todo desenvolvimento de software. O segundo costuma ficar reservado a trechos críticos, porque seu rigor lógico-matemático garante que uma funcionalidade esteja 100% correta dentro do contexto especificado.

Obrigado por ter lido até aqui!

---

Publicado originalmente no Medium em 30 de julho de 2024.