💻 computer science

Nonstandard Axiomatic Semantics

Este artigo demonstra que a semântica axiomática baseada na lógica de Hoare admite modelos não padrão semelhantes aos de Skolem, falhando, assim, em definir unicamente a semântica operacional, e propõe o enriquecimento do sistema com obrigações de prova adicionais para resolver essa ambiguidade sem afetar os modelos de traço padrão.

Autores originais: Patrick Cousot

Publicado 2026-08-25

📖 5 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Patrick Cousot

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

No mundo da ciência da computação, existe uma tensão constante entre como descrevemos o que um programa deve fazer e como provamos que ele realmente o faz. Por décadas, pesquisadores têm se baseado em um sistema chamado lógica de Hoare para verificar softwares. Este sistema funciona como um conjunto de regras lógicas: se um programa começa em um certo estado e podemos provar que ele segue passos específicos, então ele deve terminar em um estado desejado. É uma ferramenta poderosa para garantir que o código esteja livre de erros, tal como uma prova matemática garante que um teorema seja verdadeiro. No entanto, assim como os matemáticos descobriram outrora que suas regras para contar números poderiam acidentalmente descrever mundos estranhos e impossíveis, os cientistas da computação descobriram que as regras para verificar programas também podem descrever formas impossíveis de o código ser executado. A questão é se a lógica que usamos para confiar em nosso software é, de fato, precisa o suficiente para excluir esses cenários impossíveis.

Um pesquisador da Universidade de Nova York demonstrou recentemente que as regras padrão para verificar programas são, de fato, muito permissivas. Ele demonstrou que a lógica usada para provar a correção de programas permite modelos de execução "não padrão". Em termos simples, isso significa que as regras permitem que um programa rode de maneiras que são matematicamente possíveis dentro da lógica, mas fisicamente impossíveis no mundo real. Imagine um programa que conta indefinidamente. A visão padrão é que ele começa no zero e vai para um, dois, três, e assim por diante, sem parar. A lógica, contudo, também permite uma versão deste programa que rodou por um tempo infinito no passado antes mesmo de começarmos a observá-lo, ou um que existe em uma linha do tempo estranha e estendida que não condiz com nossa compreensão normal do tempo. O pesquisador provou que a lógica atual não consegue distinguir entre o comportamento normal e esperado de um programa e esses comportamentos estranhos e não padrões. Isso é um problema significativo porque, se a lógica não consegue distinguir entre o mundo real e esses mundos impossíveis, ela não define unicamente o que um programa realmente faz.

Para entender por que isso acontece, deve-se observar como os laços (loops) em programas de computador são verificados. Quando um programa repete um bloco de código, como um laço que executa enquanto uma condição for verdadeira, a lógica exige um "invariante de laço". Este é um enunciado que permanece verdadeiro toda vez que o laço se repete. O pesquisador mostrou que, para muitos programas, é possível inventar um invariante de laço que seja verdadeiro para a execução padrão e normal do código, mas que também seja verdadeiro para essas execções estranhas e não padrões. Por exemplo, considere um programa que conta progressivamente. A lógica permite uma prova que funciona para uma contagem começando em zero e subindo, mas também permite uma prova que funciona para uma contagem que tem rodado para trás desde o infinito negativo, ou uma que existe em uma linha do tempo com passos extras e invisíveis que os humanos não conseguem perceber. Como a lógica trata essas diferentes linhas do tempo como válidas, ela falha em determinar um significado único para o programa. A lógica é ambígua, tal como uma definição antiga de números que permitia a existência de números "fantasmagóricos" que se comportam como números normais, mas não fazem parte da sequência de contagem padrão.

O artigo não apenas identifica essa ambiguidade; ele oferece uma maneira de corrigi-la. O pesquisador propõe adicionar requisitos extras ao processo de verificação, inspirados em métodos usados para provar que um programa eventualmente parará de rodar. Esses novos requisitos atuam como um filtro. Eles exigem que a prova da correção de um programa também mostre que a execução do programa segue um caminho específico e padrão através do tempo. Especificamente, as novas regras exigem que, se você fosse contar os passos de um laço, a contagem deve seguir a progressão padrão de números que usamos todos os dias, sem extensões infinitas ocultas. Se o comportamento de um programa depender dessas linhas do tempo estranhas e não padrões, as novas regras falharão em provar sua correção. Isso efetivamente força a lógica a ignorar os mundos impossíveis e focar apenas nas execuções padrão e do mundo real que nos interessam.

Crucialmente, o pesquisador mostra que, para qualquer programa que se comporte normalmente, esses novos requisitos são automaticamente satisfeitos. Isso significa que para a vasta maioria do trabalho de verificação de software que as pessoas realizam hoje, as provas existentes permanecem válidas e inalteradas. As novas regras não tornam o trabalho de provar programas mais difícil para os casos padrão; elas simplesmente fecham a porta dos fundos que permitia que os casos impossíveis entrassem. O resultado é uma definição mais precisa do que um programa significa. Ao adicionar esses controles extras, a lógica finalmente torna-se uma descrição única do comportamento do programa, garantindo que, quando dizemos que um programa está correto, estamos falando de exatamente uma forma específica de ele rodar, e não de uma coleção de realidades possíveis, incluindo algumas que desafiam nossa compreensão de tempo e sequência.

Este trabalho conecta um problema profundo nos fundamentos da matemática com a tarefa prática de escrever software seguro. Assim como os matemáticos outrora refinaram sua definição de números para excluir variações impossíveis, esta pesquisa refina a definição de execução de programas. Ela garante que as ferramentas que usamos para verificar a segurança de sistemas críticos não sejam apenas logicamente consistentes, mas também fundamentadas na única realidade padrão de como os computadores realmente operam. A solução é elegante porque não exige a reescrita de todo o sistema de verificação de programas; ela simplesmente adiciona um trilho de proteção que mantém a lógica no caminho pretendido, garantindo que nossa confiança no software seja baseada em uma verdade única e bem definida.

Resumo Técnico: Semântica Axiomática Não Padrão

Declaração do Problema

O artigo aborda uma ambiguidade fundamental na semântica axiomática baseada na lógica de Hoare. Análogo aos modelos não padrões de Skolem para a aritmética de Peano, o autor demonstra que a lógica de Hoare admite modelos não padrões de execução de programas. Especificamente, a lógica não caracteriza unicamente a semântica operacional pretendida (semântica de traço) das linguagens de programação até o isomorfismo.

O problema central surge na Regra de Iteração. Embora a lógica de Hoare utilize invariantes indutivos para raciocinar sobre laços, a teoria lógica padrão não consegue distinguir entre:

Traços padrão: Execuções finitas e execuções infinitas indexadas por números naturais padrão ( $\mathbb{N}$ ).
Traços não padrões: Execuções indexadas por conjuntos naturais não padrões (por exemplo, modelos de Skolem contendo "passados infinitos" ou "futuros infinitos" além de $\omega$ ).

Consequentemente, uma prova de lógica de Hoare válida para um modelo de traço padrão também é válida para modelos não padrões onde os laços podem ter comprimentos não padrões (por exemplo, começando em um passado não padrão ou continuando em um futuro não padrão). Isso implica que a lógica de Hoare, como tradicionalmente formulada, não especifica uma semântica operacional única e bem definida.

Metodologia

O autor emprega uma análise comparativa entre a semântica de traço padrão e a semântica de traço não padrão, utilizando conceitos de interpretação abstrata e teoria de ponto fixo.

Formalização da Semântica de Traço:
- Semântica Padrão: Definida via pontos fixos mínimos ($lfp$) e máximos ($gfp$) no reticulado de traços finitos ( $\Sigma^*$ ) e infinitos ( $\Sigma^\infty$ ) indexados por $\mathbb{N}$ .
- Semântica Não Padrão: Estendida para traços indexados por conjuntos não padrões como $\mathbb{N} + \delta$ (traços não padrões para frente com um futuro infinito) e $\mathbb{N} - \delta$ (traços não padrões para trás com um passado infinito), onde $\delta > 0$ . Esses conjuntos modelam estruturas do tipo Skolem.
Abstração e Equivalência:
- O artigo define uma função de abstração $\alpha_S$ mapeando a semântica de traço para o conjunto de triplas de Hoare válidas.
- O Teorema 1 prova que o conjunto de triplas de Hoare válidas para a semântica padrão ( $H(L)$ ) é idêntico ao conjunto de triplas válidas para a semântica não padrão ( $\tilde{H}(L)$ ). Isso confirma que as regras de prova padrão de Hoare são insuficientes para excluir interpretações não padrões.
Remédio Proposto (Padronização):
Para resolver essa ambiguidade, o autor propõe enriquecer a semântica axiomática com obrigações de prova adicionais inspiradas em métodos de prova de terminação (especificamente o método de Knuth e variantes ordinais).
- Prevenção de Traços para Frente Não Padrões: A lógica é estendida para exigir a existência de uma função crescente $K$ que mapeia posições de traço para ordinais ( $\mathcal{O}$ ) tal que o contador do laço seja limitado pelo primeiro limite ordinal infinito $\omega$ . Como partes inteiras não padrões não podem ser isomorfas por ordem a ordinais bem fundados, esse requisito elimina traços infinitos para frente não padrões.
- Prevenção de Traços para Trás Não Padrões: Um requisito dual é introduzido para traços para trás, exigindo uma função decrescente $K$ (antitônica) que garanta que a travessia para trás termine dentro de um limite padrão.

Principais Contribuições

Identificação de Modelos Não Padrões: O artigo estabelece formalmente que a lógica de Hoare sofre do mesmo problema de não-unicidade da aritmética de Peano sem a condição de categoricidade de Dedekind. Mostra que os invariantes de laço em lógica de primeira ordem não podem distinguir entre modelos de traço padrão e não padrão devido ao teorema da compacidade.
Equivalência de Teorias: Prova que as teorias de lógica de Hoare padrão e não padrão são idênticas ( $H(L) = \tilde{H}(L)$ ), o que significa que as provas existentes não excluem inerentemente execuções não padrões.
Padronização via Restrições Ordinais: O artigo propõe um método para restringir a semântica axiomática aos modelos padrão através da adição de obrigações de prova envolvendo contadores ordinais (limitados por $\omega$ para traços para frente e exigindo terminação para traços para trás).
Preservação de Provas Padrão: Um resultado crucial é que essas obrigações de prova adicionais são sempre satisfeitas pela semântica de traço padrão. Portanto, se um assume a interpretação padrão (como é implícito na maioria dos usos da lógica de Hoare), as provas de Hoare existentes permanecem válidas e inalteradas. As novas obrigações servem para excluir formalmente modelos não padrões sem alterar a verificação prática de programas padrão.

Resultados

Equivalência Teórica: O conjunto de triplas de Hoare válidas para modelos de traço não padrão é exatamente o mesmo que para modelos padrão.
Resolução de Ambiguidade: Ao impor as condições de limitação ordinal (Equações 9 e 10), a semântica axiomática é restrita ao modelo padrão.
Aplicabilidade: A padronização proposta é compatível com algoritmos de análise estática e de tipagem existentes que dependem da lógica de Hoare, desde que a suposição subjacente de semântica padrão seja tornada explícita ou as novas obrigações sejam verificadas (o que é trivial para modelos padrão).
Limitações: O artigo observa que em Lógicas de Hoare Abstratas, onde o domínio concreto é substituído por um domínio abstrato que pode não ser expressivo o suficiente para definir as funções ordinais requeridas, os métodos de padronização podem não ser diretamente aplicáveis.

Significância

O artigo argumenta que a afirmação comum de que "a semântica axiomática define o significado de um programa por seus efeitos em asserções lógicas" é tecnicamente falha porque o significado definido não é único até o isomorfismo. A significância reside em:

Esclarecimento dos Fundamentos: Destaca que a lógica de Hoare, como a aritmética de Peano, requer uma condição de "categoricidade" (neste caso, padronização via limites ordinais) para garantir uma interpretação operacional única.
Formalização de Suposições Implícitas: Torna explícita a hipótese implícita de que a lógica de Hoare é interpretada sobre modelos de computação padrão.
Ponte entre Lógica e Semântica: Demonstra como técnicas de prova de terminação (usando ordinais) podem ser integradas à semântica axiomática para eliminar interpretações não padrões, alinhando assim a semântica axiomática de forma mais rigorosa com a semântica de traço operacional.

O autor conclui que, embora as provas de lógica de Hoare não precisem ser alteradas para modelos padrão, o quadro teórico deve reconhecer e excluir formalmente modelos não padrões para reivindicar uma definição única de semântica de programa.