Especificações: Precondições, Pós-condições e Invariantes

• Definir precondições, pós-condições, invariantes de representação e invariantes de laço como predicados sobre estados de programa.
• Separar as obrigações de quem chama das promessas da implementação em um contrato de software.
• Julgar se uma especificação candidata é fraca demais, forte demais ou presa demais a detalhes de implementação.
• Explicar por que invariantes são necessários para expressar fatos que precisam sobreviver a passos internos, e não só fatos que valem bem no final.
• Ligar a escrita de especificações à lógica de predicados já desenvolvida em Matemática Discreta e Lógica.

testing-shows-presence-proof-shows-absence estabeleceu que toda prova é uma prova de algo específico: uma propriedade, enunciada com precisão, em relação a um modelo fixo de execução. Este conceito fornece o vocabulário de que esse "algo específico" é de fato feito. A prática comum de testes já usava implicitamente saídas esperadas ("dada esta entrada, a função deve devolver aquele valor"), mas esse hábito só descreve um punhado de exemplos concretos. Os métodos formais generalizam o mesmo instinto em contratos precisos o bastante para que um motor de prova, um solver SMT ou um humano escrevendo uma derivação em lógica de Hoare consigam checá-los mecanicamente, contra toda entrada que uma precondição permite, e não só contra as que alguém calhou de anotar.

As três peças desse contrato cumprem, cada uma, um papel distinto. Uma precondição enuncia o que pode ser presumido verdadeiro antes de a execução começar: é uma obrigação imposta a quem chama. Uma pós-condição enuncia o que precisa ser verdade depois que a execução termina: é uma promessa feita pela implementação, condicionada a quem chama ter respeitado a precondição. Um invariante enuncia o que precisa continuar verdadeiro ao longo de uma região da computação que os testes não têm um jeito natural de inspecionar no meio: o corpo de um laço, o estado interno de um tipo abstrato de dados ao longo de muitas operações. Sem essas três peças enunciadas explicitamente, "correto" é só um elogio informal feito a um código que por acaso se comportou bem nos exemplos que alguém testou; com elas, "correto" vira uma afirmação matemática específica que alguém pode de fato tentar provar ou refutar.

A conexão com a fronteira da computabilidade do conceito anterior é direta e vale explicitá-la aqui, em vez de deixá-la implícita: como nenhuma ferramenta consegue inferir automaticamente a intenção semântica completa de quem programa (isso exigiria resolver exatamente o tipo de problema indecidível que o Teorema de Rice exclui), a verificação útil precisa começar com um humano enunciando os predicados certos. Um verificador consegue checar se um programa satisfaz uma especificação enunciada; ele não consegue tirar a própria especificação do nada. É por isso que a escrita de especificações, o assunto deste conceito, é tratada como trabalho pré-requisito, e não como algo acoplado à prova depois.

Estados e predicados

Um estado de programa é, no fundo, um mapeamento de cada variável atualmente em escopo para o valor que ela tem em algum momento específico da execução. Um predicado sobre estados não é nada mais exótico que uma proposição, construída com os conectivos e quantificadores já disponíveis de Matemática Discreta e Lógica, que um dado estado satisfaz ou não; uma asserção como n ≥ 0 ∧ i ≤ n é simplesmente uma regra para classificar estados em duas pilhas, "sim" e "não", sem ambiguidade sobre a pilha a que qualquer estado pertence. É uma mudança de perspectiva sutil, mas importante, em relação à programação comum: uma especificação não é a descrição de um estado, como a saída esperada de um único teste; é a descrição de um conjunto inteiro de estados, possivelmente infinito, caracterizado por quais predicados seus membros satisfazem. O mesmo predicado, avaliado em pontos diferentes da execução, pode mudar de verdadeiro para falso ou o contrário (i ≤ n pode valer antes de o corpo de um laço rodar e falhar depois, se o corpo incrementar i além de n), e é exatamente por isso que as especificações precisam dizer em que ponto da execução uma dada asserção deve valer, em vez de tratar "verdadeiro" como uma propriedade atemporal do programa.

Precondições

Uma precondição registra as premissas que um trecho de código tem direito de fazer sobre o estado em que começa e, correspondentemente, as obrigações impostas a quem o chama. Há um trade-off de engenharia genuíno escondido no modo como uma precondição é escolhida: uma precondição fraca (que aceita um grande conjunto de estados iniciais possíveis) torna a operação utilizável por mais chamadores, mas, por outro lado, dá a quem implementa menos com que trabalhar, o que pode tornar a pós-condição mais difícil, ou até impossível, de estabelecer. Uma precondição forte (que exclui a maioria dos estados iniciais) pode tornar a prova interna trivial, ao custo de uma operação especificada de forma tão restritiva que poucos chamadores reais conseguem de fato satisfazê-la. Precondições faltantes ou subespecificadas não são uma lacuna cosmética de documentação; são exatamente onde moram os bugs reais na prática: divisão por zero, violações de limites de arrays e operações de protocolo chamadas no estado errado são, quase sem exceção, casos em que uma precondição que deveria ter sido checada e imposta foi deixada implícita, presumida ou simplesmente esquecida.

Pós-condições

Uma pós-condição registra a promessa que uma operação faz a quem a chama, desde que a operação retorne normalmente a partir de um estado que satisfazia a precondição. Uma pós-condição bem escolhida descreve comportamento observável de fora (aquilo de que quem chama pode depender sem saber nada sobre como a operação é implementada), em vez de vazar detalhes privados de implementação dos quais quem chama não deveria depender e que uma refatoração futura poderia legitimamente mudar. A força de uma pós-condição importa muito e é fácil de errar na direção de fraca demais para ser útil: para uma rotina de ordenação, "a saída está ordenada e é uma permutação da entrada" fixa completamente o comportamento pretendido, enquanto "o primeiro elemento da saída é menor ou igual ao segundo" é tecnicamente uma pós-condição verdadeira de qualquer ordenação correta, mas também é satisfeita por um número imenso de implementações incorretas, então prová-la estabelece quase nada de valor prático. Algumas pós-condições, além disso, nem podem ser enunciadas puramente como um predicado sobre o estado final: uma propriedade de segurança como "o valor secreto nunca aparece no canal publicamente observável, em nenhum ponto da execução" é uma afirmação sobre o rastro inteiro da computação, e não só sobre o seu fim, e especificá-la corretamente exige exatamente o raciocínio baseado em rastros para o qual a lógica temporal e o model checking, vistos bem mais adiante nesta disciplina, são construídos.

Invariantes

Os invariantes existem porque alguns fatos precisam sobreviver a uma computação que não é visível de fora: o meio de um laço, ou o interior de um tipo abstrato de dados ao longo de uma longa sequência de operações públicas que ninguém de fora do tipo consegue inspecionar diretamente. Um invariante de laço precisa valer logo antes de a guarda do laço ser checada e de novo logo depois de cada execução do corpo do laço; é precisamente a propriedade que vai permitir a loop-invariants-and-the-while-rule transformar arbitrariamente muitas quantidades possíveis de iterações em uma única obrigação de prova finita. Um invariante de representação cumpre o papel análogo para um tipo abstrato de dados: ele precisa valer antes e depois de cada operação pública, capturando as condições de consistência interna ("o índice do topo da pilha nunca passa da capacidade", digamos) em que a implementação do tipo se apoia internamente, embora nenhum cliente jamais veja a representação bruta diretamente. Um invariante de protocolo generaliza a mesma ideia para um sistema de transição: um fato que precisa valer em todo estado alcançável, exatamente a noção que transition-systems-and-kripke-structures vai formalizar para o model checking. Em cada um desses três casos, o invariante faz o mesmo trabalho essencial: é como o raciocínio local sobre um passo da computação (uma iteração do laço, uma operação sobre um tipo abstrato de dados, uma transição de um protocolo) é levado a escalar para uma afirmação sobre sequências arbitrariamente longas ou ilimitadas desses passos, sem nunca precisar raciocinar sobre cada sequência individual separadamente.

Contrato de divisão inteira

Considere um procedimento div(n, d) que deve dividir n por d. Antes que qualquer pós-condição possa sequer ser enunciada com sentido, a precondição d ≠ 0 não é opcional: dividir por zero é matematicamente indefinido, então qualquer contrato que omita essa precondição está afirmando implicitamente (e incorretamente) que a operação é total quando não é. Com essa precondição no lugar, a pós-condição ainda depende de uma decisão de projeto que a frase informal "dividir n por d" deixa completamente em aberto: se a divisão exata é a pretendida, uma pós-condição adequada é result * d = n, que fixa completamente a semântica para o caso em que d divide n exatamente. Se a pretendida é a divisão inteira com truncamento (o comportamento que a maioria das linguagens de programação de fato dá ao operador / sobre inteiros), o contrato precisa dizer algo mais rico, mencionando um quociente e um resto e restringindo a magnitude e o sinal do resto em relação a d, porque a "divisão com truncamento" é uma operação matemática genuinamente diferente da divisão exata e merece uma pós-condição genuinamente diferente. A lição vai muito além deste exemplo: uma frase em linguagem natural descrevendo o que uma operação faz muitas vezes é ambígua entre dois ou mais comportamentos matematicamente distintos, e escrever a precondição e a pós-condição explicitamente é exatamente o passo que força essa ambiguidade a ser resolvida antes que qualquer tentativa de prova possa sequer começar.

Invariante de representação de uma pilha

Considere uma pilha implementada como um array de tamanho fixo data junto com um inteiro top que registra quantos elementos estão guardados no momento. O invariante de representação 0 ≤ top ≤ capacity é o fato que cada uma das operações públicas dessa pilha precisa tanto presumir na entrada quanto garantir na saída; é a condição de consistência interna que faz de data[0..top-1] uma descrição com sentido de "os elementos que estão na pilha agora". A precondição de push é top < capacity, porque empilhar em uma pilha cheia não tem significado sensato sob essa representação; sua pós-condição é que top aumenta exatamente em um e o elemento recém-empilhado agora ocupa o que era, logo antes da chamada, o valor antigo de top. A precondição de pop, simetricamente, é top > 0, já que desempilhar uma pilha vazia é igualmente sem sentido. O invariante 0 ≤ top ≤ capacity é aquilo que cada uma dessas operações é individualmente responsável por preservar; se push algum dia pudesse violá-lo, deixando top passar de capacity, o raciocínio de cada operação seguinte, por mais cuidadosamente provado isoladamente, ficaria silenciosamente incorreto, porque a prova de cada operação presumia implicitamente que o invariante ainda estava intacto quando ela começou.

Fortalecendo uma pós-condição fraca

Suponha que uma função de valor absoluto seja especificada apenas pela pós-condição result ≥ 0. Isso parece plausível à primeira vista, mas é satisfeito pela função abs(x) = 0 para toda entrada x; uma função que obviamente não calcula o valor absoluto, mas para a qual a pós-condição enunciada vale incondicionalmente. A pós-condição é fraca demais justamente porque diz algo sobre o formato da saída (não negativa) sem dizer nada sobre como a saída se relaciona com a entrada, e é exatamente essa relação faltante que faz do valor absoluto a função específica que ele é, em vez de uma função arbitrária com valores não negativos. Fortalecer a pós-condição para result ≥ 0 ∧ (result = x ∨ result = -x) fecha essa lacuna: ela agora exige que a saída seja de fato um dos dois valores que poderiam plausivelmente ser "o valor absoluto de x", o que exclui a implementação constante zero para todo x diferente de zero (já que nem 0 = x nem 0 = -x valem quando x ≠ 0) e ainda permite a implementação correta. O princípio geral que isso ilustra: uma pós-condição que só restringe o formato do resultado, sem relacionar o resultado de volta às entradas que a operação de fato recebeu, quase sempre é fraca demais para fixar o comportamento pretendido, por mais natural que pareça na primeira leitura.

• Escrever exemplos quando é preciso um predicado universal. "Deve devolver 4 quando receber 2" é um caso de teste, e não uma especificação; uma precondição e uma pós-condição de verdade precisam caracterizar toda entrada que a operação deve tratar de uma vez, usando variáveis e predicados, e não uma lista finita de pares de entrada e saída ilustrativos, por mais representativos que esses pares pareçam.
• Tornar a precondição tão forte que quase nenhum chamador realista consegue satisfazê-la. Uma precondição como "o array já está ordenado, não tem duplicatas e tem tamanho exatamente igual a uma potência de dois" pode tornar uma prova interna trivial, mas, se chamadores reais violam rotineiramente uma dessas partes, a especificação moveu em silêncio o problema real (tratar o caso geral) para fora do que o código verificado sequer cobre, sem tornar esse estreitamento visível em lugar nenhum além das letras miúdas.
• Deixar a pós-condição mencionar detalhes privados de implementação dos quais os clientes nunca deveriam depender. Uma pós-condição que promete "o array interno de cache tem exatamente este layout" amarra o código cliente a uma escolha de implementação que uma refatoração futura tem o direito de mudar; as pós-condições devem descrever só o comportamento observável de fora, exatamente a mesma disciplina que mantém a implementação de uma abstração livre para evoluir sem quebrar seu contrato.
• Chamar a guarda do laço de invariante. A guarda (i < n, digamos) é a condição checada para decidir se o laço continua; o invariante é uma asserção separada que precisa ser verdadeira tanto quando a guarda vale quanto depois que ela fica falsa. Confundir as duas é um erro inicial comum, e importa porque é o invariante, e não a guarda, que leva a prova de "verdadeiro antes do laço" a "verdadeiro depois de arbitrariamente muitas iterações".
• Omitir condições de frame, deixando obscuro quais variáveis podem mudar. Uma pós-condição que diz "o array-alvo agora está ordenado", mas nunca diz se outros campos não relacionados do mesmo objeto podem mudar, deixa quem chama sem como raciocinar sobre o que mais pode ter sido modificado em silêncio; uma condição de frame implícita ("nada mais muda") muitas vezes é presumida, mas deveria ser enunciada, especialmente quando estado compartilhado mutável ou aliasing entram em cena.

As especificações são a camada de contrato sobre a qual todo o resto da verificação formal é construído: uma precondição enuncia o que quem chama precisa estabelecer antes de invocar uma operação, uma pós-condição enuncia o que a operação promete em troca, e um invariante enuncia o que precisa sobreviver à computação que acontece longe da vista de quem chama (dentro do corpo de um laço ou ao longo de uma longa sequência de operações sobre um tipo abstrato de dados). Escolher bem esses predicados é uma habilidade de projeto genuína, com trade-offs reais, e não uma transcrição mecânica da intenção: precondições fortes demais excluem sem necessidade chamadores legítimos, pós-condições fracas demais não fixam o comportamento de fato pretendido, e os invariantes são o mecanismo específico que transforma o raciocínio local, de um passo, em uma prova que escala para execuções ilimitadamente longas. Como nenhuma ferramenta consegue inferir esses predicados automaticamente a partir de uma descrição da intenção em linguagem natural, escrevê-los com precisão é inevitavelmente uma responsabilidade humana; uma que cada técnica apresentada mais adiante nesta disciplina, das regras de inferência da lógica de Hoare às propriedades temporais de um model checker, toma como ponto de partida, em vez de tentar contorná-la.