Lógica para Especificação: Proposicional e de Primeira Ordem

• Traduzir requisitos informais em asserções proposicionais e de primeira ordem sobre estados de programa.
• Combinar afirmações menores com precisão usando os conectivos ¬, ∧, ∨, → e ↔.
• Usar quantificadores limitados para especificar propriedades de arrays, heaps e coleções sem deixar nenhuma ambiguidade sobre o escopo.
• Distinguir satisfatibilidade, validade e consequência lógica como três perguntas diferentes que uma obrigação de verificação pode fazer.
• Reconhecer o trade-off entre a expressividade lógica (quanto uma linguagem de especificação consegue dizer) e o quanto checá-la acaba sendo automatizável.

specifications-preconditions-postconditions-invariants apresentou precondições, pós-condições e invariantes como predicados sobre estados, mas deixou em grande parte implícita a linguagem em que esses predicados são de fato escritos. Antes que uma tripla de Hoare possa ser provada ou que uma propriedade de model checking possa ser avaliada contra um sistema de transição, asserções como x ≥ 0, sorted(a) ou "toda requisição acaba sendo confirmada" precisam ser escritas com precisão suficiente para que um sistema de prova (ou, mais tarde, um solver automatizado) consiga manipulá-las mecanicamente, sem nunca precisar adivinhar o que uma frase em linguagem natural tentava dizer.

Os blocos de construção aqui não são novos: os conectivos da lógica proposicional e os predicados, funções e quantificadores da lógica de primeira ordem são exatamente o mecanismo que Matemática Discreta e Lógica já desenvolveu e provou correto. O que é genuinamente novo neste conceito é a interpretação: essas fórmulas não são mais avaliadas sobre domínios matemáticos abstratos escolhidos por conveniência didática, mas sobre estados de programa, heaps, arrays e, mais adiante, rastros de execução inteiros. A lógica não muda; o universo de que ela fala é que muda, e essa mudança de universo é o que transforma um kit matemático familiar em uma linguagem de especificação.

Vale enunciar logo de início, em vez de descobrir de surpresa depois, a conexão com Computabilidade e Complexidade: linguagens lógicas mais ricas conseguem expressar estritamente mais propriedades, mas uma ferramenta que conseguisse decidir automaticamente a verdade de toda fórmula de primeira ordem sobre todo programa possível equivaleria a um verificador de programas de uso geral, e isso contradiria diretamente os resultados de indecidibilidade (o Problema da Parada, o Teorema de Rice) que Computabilidade e Complexidade já provou. Cada escolha feita neste conceito sobre quão expressiva deixar uma linguagem de especificação é, implicitamente, também uma escolha sobre quanto suporte automatizado essa linguagem pode esperar receber depois, uma tensão que ressurge explicitamente quando os solvers SAT e SMT entram em cena.

Asserções sobre estados

Uma asserção não é uma verdade eterna e livre de contexto: é uma fórmula avaliada em um estado específico, e seu valor-verdade pode depender inteiramente de qual estado é escolhido. A asserção x < y é verdadeira em um estado em que x vale 3 e y vale 5, e falsa em um estado em que os valores estão invertidos; a mesma fórmula sintática, dois veredictos diferentes, porque os dois estados diferem. É exatamente por isso que as regras de prova da lógica de Hoare são descritas como "transformadoras de asserções" à medida que os comandos transformam estados: provar {P} C {Q} é, na verdade, um argumento sobre como o valor-verdade das asserções muda conforme a execução avança de um estado que satisfaz P, passando pelo que quer que C faça, até um estado final que precisa satisfazer Q. Uma asserção de estado bem formada, por boa prática, deve mencionar só as variáveis e os componentes do modelo de que sua afirmação genuinamente depende; uma asserção que referencia em silêncio uma variável que um comando nunca toca convida à confusão sobre se o valor dessa variável está de fato restrito por alguma coisa.

Estrutura proposicional

Os cinco conectivos familiares fazem um trabalho real e distinto quando aplicados a asserções de programa, e não a proposições abstratas. A conjunção P ∧ Q exige que as duas subafirmações valham ao mesmo tempo, no mesmo estado; exatamente o formato de um invariante como 0 ≤ top ≤ capacity, do exemplo da pilha do conceito anterior, em que as duas metades precisam valer juntas, e não separadamente em momentos diferentes. A disjunção P ∨ Q permite que qualquer uma das subafirmações valha, o formato natural para descrever uma especificação que admite mais de um resultado aceitável; digamos, uma operação que ou tem sucesso e atualiza o estado, ou falha de forma limpa e deixa o estado inalterado. A implicação P → Q é, de longe, o formato mais comum que uma obrigação de prova de verificação de fato assume: "se a precondição e a guarda do laço valem, então a pós-condição deste passo vale" é exatamente o formato de uma obrigação de consequência da lógica de Hoare, e reconhecer uma obrigação como uma implicação costuma ser o primeiro passo para saber como atacá-la (supor o antecedente, derivar o consequente). A equivalência P ↔ Q sustenta o tipo de reescrita e simplificação que torna uma asserção difícil de ler mais fácil de trabalhar sem mudar seu significado; trocar ¬(x < y) por x ≥ y nos inteiros, por exemplo, é autorizado exatamente por esse conectivo.

Predicados de primeira ordem

A lógica proposicional sozinha não consegue dizer "todo elemento deste array é não negativo"; isso exige nomear uma propriedade que se aplica de forma uniforme a um domínio de indivíduos, e é para isso que existem predicados e quantificadores. Um predicado como sorted(a, n) ou owns(user, file) nomeia uma propriedade que pode ou não valer para argumentos específicos, e é genuinamente diferente de uma variável booleana, porque sua verdade depende de quais argumentos são usados. O quantificador universal ∀ expressa "isto vale para todo elemento relevante", o formato natural de especificações no estilo de segurança que precisam valer de forma uniforme, como "todo índice de um array ordenado respeita a ordem". O quantificador existencial ∃ expressa "existe pelo menos um elemento para o qual isto vale", o formato natural de afirmações de que algo existe em algum lugar, sem dizer onde, como "existe um caminho válido do estado inicial ao objetivo". Crucialmente, o domínio sobre o qual cada quantificador varia precisa ser enunciado explicitamente, e não deixado para o contexto, porque "para todos os elementos" de um domínio ilimitado ou mal definido é uma afirmação diferente, e muitas vezes sem sentido ou indemonstrável, de "para todos os elementos dentro destes limites do array"; é exatamente por isso que limites explícitos nos quantificadores importam tanto na prática, e por isso que omiti-los é apontado abaixo como uma armadilha genuína, e não como um capricho de estilo.

Consequência lógica e satisfatibilidade

Três perguntas lógicas distintas aparecem o tempo todo quando fórmulas são usadas como especificações, e confundi-las é uma fonte real de confusão. A consequência lógica, escrita P ⊨ Q, pergunta se todo estado que satisfaz P também satisfaz Q; é exatamente o formato lógico de um passo de consequência da lógica de Hoare, em que uma prova precisa mostrar que o que a asserção atual garante é forte o bastante para implicar o que é necessário a seguir. A satisfatibilidade faz uma pergunta mais fraca: existe pelo menos um estado que torna uma dada fórmula verdadeira? Uma fórmula pode ser satisfatível sem ser sempre verdadeira, o que importa muito para a busca de bugs, em que o objetivo muitas vezes é justamente encontrar algum estado que viole uma propriedade de segurança. A validade faz a pergunta mais forte: todo estado torna a fórmula verdadeira, sem nenhuma exceção? Essas três noções são intimamente ligadas, e não independentes: muitos verificadores práticos provam uma consequência lógica P ⊨ Q de forma indireta, mostrando que a fórmula P ∧ ¬Q é insatisfatível; se nenhum estado consegue ao mesmo tempo satisfazer P e violar Q, então todo estado que satisfaz P precisa satisfazer Q, que é exatamente o que a consequência lógica afirma. Essa tradução de "provar uma consequência lógica" em "mostrar que uma conjunção é insatisfatível" é exatamente a ponte conceitual que os solvers SAT e SMT, apresentados mais adiante nesta disciplina, são construídos para explorar em escala automatizada.

Uma obrigação proposicional

Suponha que uma prova em lógica de Hoare já tenha estabelecido a asserção x ≥ 5 em algum ponto, e que o passo seguinte da prova exija que x > 0 valha nesse mesmo ponto. É uma pergunta de consequência lógica: x ≥ 5 ⊨ x > 0? O argumento é imediato quando enunciado como aritmética comum: qualquer inteiro x que satisfaça x ≥ 5 é pelo menos 5, e todo inteiro que é pelo menos 5 certamente é maior que 0, então todo estado que satisfaz a primeira asserção também satisfaz a segunda. Esse pequeno raciocínio aritmético não é um exercício de brinquedo desconectado do resto da disciplina; é exatamente o trabalho lógico feito por um passo de consequência na lógica de Hoare, a regra que permite a uma prova fortalecer ou enfraquecer uma asserção em qualquer ponto recorrendo à implicação lógica comum, em vez de reexaminar a execução do programa.

Um predicado de ordenação

Considere especificar que um array a de tamanho n está ordenado em ordem não decrescente. Escrever isso com precisão exige exatamente o mecanismo de quantificadores recém-apresentado:

text
∀ i. ∀ j. 0 ≤ i ≤ j < n → a[i] ≤ a[j]

Lido parte por parte: os dois quantificadores universais variam sobre todo par de índices i e j; a guarda 0 ≤ i ≤ j < n restringe a atenção a pares que são índices válidos do array e ordenados, com i em j ou antes dele, excluindo totalmente da afirmação pares de índices sem sentido ou fora da faixa; a implicação então diz que, para todo par válido e ordenado assim, o elemento anterior não é maior que o posterior. Cada parte desta fórmula faz um trabalho necessário: tirar o limite 0 ≤ i ≤ j < n deixaria os quantificadores variando sobre um domínio irrestrito e sem sentido, e inverter a implicação ou trocar os papéis de i e j produziria uma fórmula superficialmente parecida, mas que afirma outra coisa (ou nada coerente). É uma ilustração direta e concreta de por que limites explícitos nos quantificadores não são decoração opcional: sem eles, "todo elemento do array" não determina de fato sobre o que o "todo" varia.

Negando uma propriedade de segurança

Uma técnica comum na verificação automatizada é buscar a negação da propriedade sendo provada, em vez de buscar uma prova direta da própria propriedade. Suponha que a afirmação de segurança seja "todo estado alcançável satisfaz balance ≥ 0". Provar isso diretamente sobre um espaço de estados ilimitado ou complexo pode ser difícil; mas sua negação ("algum estado alcançável satisfaz balance < 0") transforma a mesma pergunta em um problema de busca: esse estado existe em algum lugar do espaço de estados alcançável? É exatamente a reformulação que um model checker ou um verificador limitado baseado em SMT costuma fazer internamente: em vez de tentar uma prova universal direta, ele busca uma testemunha da negação. Se a busca tiver sucesso e encontrar esse estado, a testemunha é um contraexemplo genuíno da afirmação de segurança original, e não só evidência de uma tentativa de prova que falhou; é uma demonstração construtiva, no mesmo espírito do teste finito que falha do conceito anterior, de que a afirmação universal é falsa. Se a busca esgotar todo o espaço de estados alcançável sem encontrar testemunha, a propriedade de segurança original está provada, porque a negação foi mostrada insatisfatível exatamente sobre o domínio que importava.

• Ler a implicação como se significasse tempo ou causalidade. P → Q é uma relação puramente lógica ("sempre que P é verdadeiro, Q também é", no mesmo estado ou sob as mesmas premissas), e não uma afirmação de que P acontecer faz Q acontecer depois. Confundir implicação lógica com sequência temporal é uma fonte frequente de confusão quando a lógica temporal, em que os operadores de fato falam de "depois", entra mais adiante na disciplina e as duas noções precisam ser mantidas bem separadas.
• Esquecer em que estado uma asserção é avaliada. Como a mesma fórmula pode ser verdadeira em um estado e falsa em outro, escrever uma asserção sem deixar claro exatamente em que ponto da execução ela deve valer (antes de um comando, depois dele, em todo ponto durante um laço) deixa a afirmação genuinamente ambígua, e não apenas enunciada de forma informal.
• Escrever uma afirmação existencial quando o requisito é, na verdade, universal. "Existe um caminho que satisfaz o requisito" (∃) é uma afirmação de natureza mais fraca e mais fácil de satisfazer que "todo caminho satisfaz o requisito" (∀); confundir uma com a outra é um jeito comum de uma especificação acabar muito mais fraca do que o autor pretendia, deixando passar em silêncio programas que deveriam ter sido rejeitados.
• Deixar implícitos os limites dos quantificadores de arrays e heaps. Como o exemplo da ordenação mostra de forma concreta, ∀ i. a[i] ≤ a[i+1] sem nenhum limite enunciado para i não é sequer uma afirmação bem formada sobre um array finito; o limite não é acabamento estilístico, é o que faz a fórmula se referir ao domínio real e finito pretendido, e não a um irrestrito.
• Confundir satisfatível com válido. Uma fórmula ser satisfatível (verdadeira em pelo menos um estado) é um fato muito mais fraco que uma fórmula ser válida (verdadeira em todo estado); uma fórmula pode facilmente ser satisfatível e ainda assim falsa na maioria dos estados, e confundir "um solver encontrou uma atribuição satisfatória" com "esta propriedade sempre vale" inverte o conteúdo lógico real do que acabou de ser estabelecido.

A lógica é o que dá precisão às especificações, e nada desse mecanismo é novo: conectivos estruturam afirmações a partir de afirmações menores, predicados descrevem propriedades de estados de programa, quantificadores variam explicitamente sobre os elementos a que essas propriedades se aplicam, e a consequência lógica transforma uma especificação em uma obrigação de verificação checável. O que é novo em relação a Matemática Discreta e Lógica é só a interpretação: essas fórmulas agora são avaliadas sobre estados de programa, arrays e heaps, e não sobre domínios abstratos, e as mesmas três perguntas (satisfatibilidade, validade e consequência lógica) aparecem em todo o resto desta disciplina, em cada técnica seguinte, dos passos de consequência da lógica de Hoare às codificações SAT e SMT que os automatizam em escala mais adiante.