💻 computer science

Nonstandard Axiomatic Semantics

Cet article démontre que la sémantique axiomatique basée sur la logique de Hoare admet des modèles non standards similaires à ceux de Skolem, échouant ainsi à définir de manière unique la sémantique opérationnelle, et propose d'enrichir le système avec des obligations de preuve additionnelles pour résoudre cette ambiguïté sans affecter les modèles de traces standards.

Auteurs originaux : Patrick Cousot

Publié 2026-08-25

📖 6 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Patrick Cousot

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

Dans le monde de l'informatique, il existe une tension constante entre la manière dont nous décrivons ce qu'un programme doit faire et la manière dont nous prouvons qu'il le fait réellement. Pendant des décennies, les chercheurs se sont appuyés sur un système appelé logique de Hoare pour vérifier les logiciels. Ce système fonctionne comme un ensemble de règles logiques : si un programme commence dans un certain état, et que nous pouvons prouver qu'il suit des étapes spécifiques, alors il doit se terminer dans un état souhaité. C'est un outil puissant pour garantir que le code est exempt d'erreurs, tout comme une preuve mathématique garantit qu'un théorème est vrai. Cependant, tout comme les mathématiciens ont découvert autrefois que leurs règles de comptage des nombres pouvaient accidentellement décrire des mondes étranges et impossibles, les informaticiens ont découvert que les règles de vérification des programmes pouvaient également décrire des modes d'exécution impossibles. La question est de savoir si la logique que nous utilisons pour faire confiance à nos logiciels est réellement assez précise pour exclure ces scénarios impossibles.

Un chercheur de l'Université de New York a récemment démontré que les règles standards de vérification des programmes sont effectivement trop lâches. Il a démontré que la logique utilisée pour prouver la correction des programmes permet des modèles d'exécution « non standards ». En termes simples, cela signifie que les règles permettent à un programme de s'exécuter de manières qui sont mathématiquement possibles au sein de la logique, mais physiquement impossibles dans le monde réel. Imaginez un programme qui compte indéfiniment. La vision standard est qu'il commence à zéro et va vers un, deux, trois, et ainsi de suite, sans jamais s'arrêter. La logique, cependant, permet aussi une version de ce programme qui aurait tourné pendant un temps infini dans le passé avant même que nous ne commencions à l'observer, ou qui existerait dans une chronologie étrange et étendue qui ne correspond pas à notre compréhension normale du temps. Le chercheur a prouvé que la logique actuelle ne peut pas faire la distinction entre le comportement normal et attendu d'un programme et ces comportements non standards et bizarres. C'est un problème important car si la logique ne peut pas distinguer le monde réel des mondes impossibles, elle ne définit pas de manière unique ce qu'un programme fait réellement.

Pour comprendre pourquoi cela se produit, il faut examiner comment les boucles dans les programmes informatiques sont vérifiées. Lorsqu'un programme répète un bloc de code, comme une boucle qui s'exécute tant qu'une condition est vraie, la logique exige un « invariant de boucle ». Il s'agit d'un énoncé qui reste vrai à chaque fois que la boucle se répète. Le chercheur a montré que pour de nombreux programmes, on peut inventer un invariant de boucle qui est vrai pour l'exécution standard et normale du code, mais qui est également vrai pour ces exécutions non standards et étranges. Par exemple, considérons un programme qui compte vers le haut. La logique permet une preuve qui fonctionne pour un décompte commençant à zéro et montant, mais elle permet aussi une preuve qui fonctionne pour un décompte qui a tourné à rebours depuis l'infini négatif, ou un décompte qui existe dans une chronologie avec des étapes supplémentaires et invisibles que les humains ne peuvent percevoir. Parce que la logique traite ces différentes chronologies comme valides, elle ne parvient pas à fixer une signification unique au programme. La logique est ambiguë, semblable à une ancienne définition des nombres qui permettait des « nombres fantômes » qui se comportent comme des nombres normaux mais ne font pas partie de la séquence de comptage standard.

L'article ne se contente pas d'identifier cette ambiguïté ; il propose un moyen de la corriger. Le cherchenaire propose d'ajouter des exigences supplémentaires au processus de vérification, inspirées par les méthodes utilisées pour prouver qu'un programme finira par s'arrêter. Ces nouvelles exigences agissent comme un filtre. Elles exigent que la preuve de la correction d'un programme montre également que l'exécution du programme suit un chemin temporel spécifique et standard. Plus précisément, les nouvelles règles exigent que si vous comptiez les étapes d'une boucle, le décompte doit suivre la progression standard des nombres que nous utilisons quotidiennement, sans aucune extension infinie cachée. Si le comportement d'un programme repose sur ces chronologies non standards et étranges, les nouvelles règles échoueront à prouver sa correction. Cela force efficacement la logique à ignorer les mondes impossibles pour se concentrer uniquement sur les exécutions réelles et standards qui nous importent.

De manière cruciale, le chercheur démontre que pour tout programme qui se comporte normalement, ces nouvelles exigences sont automatiquement satisfaites. Cela signifie que pour la grande majorité du travail de vérification de logiciels que les gens effectuent aujourd'hui, les preuves existantes restent valides et inchangées. Les nouvelles règles ne rendent pas plus difficile la tâche de prouver la correction des programmes pour les cas standards ; elles ferment simplement la porte dérobée qui permettait aux cas impossibles de s'introduire. Le résultat est une définition plus précise de ce que signifie un programme. En ajoutant ces vérifications supplémentaires, la logique devient enfin une description unique du comportement d'un programme, garantissant que lorsque nous disons qu'un programme est correct, nous parlons exactement d'une façon spécifique dont il s'exécute, et non d'une collection de réalités possibles incluant certaines qui défient notre compréhension du temps et de la séquence.

Ce travail relie un problème profond des fondements des mathématiques à la tâche pratique de l'écriture de logiciels sûrs. Tout comme les mathématiciens ont autrefois affiné leur définition des nombres pour exclure les variations impossibles, cette recherche affine la définition de l'exécution d'un programme. Elle garantit que les outils que nous utilisons pour vérifier la sécurité des systèmes critiques ne sont pas seulement logiquement cohérents, mais aussi ancrés dans la réalité unique et standard du fonctionnement réel des ordinateurs. La solution est élégante car elle ne nécessite pas de réécrire l'ensemble du système de vérification de programmes ; elle ajoute simplement un garde-fou qui maintient la logique sur le chemin prévu, garantissant que notre confiance dans les logiciels est basée sur une vérité unique et bien définie.

Résumé Technique : Sémantique Axiomatique Non Standard

Énoncé du Problème

L'article traite d'une ambiguïté fondamentale de la sémantique axiomatique basée sur la logique de Hoare. Analogue aux modèles non standards de l'arithmétique de Peano de Skolem, l'auteur démontre que la logique de Hoare admet des modèles non standards d'exécution de programmes. La logique ne caractérise pas de manière unique la sémantique opérationnelle (sémantique de trace) voulue des langages de programmation à un isomorphisme près.

Le problème central provient de la Règle d'Itération. Bien que la logique de Hoare utilise des invariants inductifs pour raisonner sur les boucles, la théorie logique standard ne peut distinguer entre :

Traces standards : Exécutions finies et exécutions infinies indexées par des entiers naturels standards ( $\mathbb{N}$ ).
Traces non standards : Exécutions indexées par des entiers naturels non standards (par exemple, des modèles de Skolem contenant des « passés infinis » ou des « futurs infinis » au-delà de $\omega$ standard).

Par conséquent, une preuve de logique de Hoare valide pour un modèle de trace standard est également valide pour des modèles non standards où les boucles peuvent avoir des longueurs non standards (par exemple, commençant dans un passé non standard ou se poursuivant dans un futur non standard). Cela implique que la logique de Hoore, telle qu'elle est traditionnellement formulée, ne spécifie pas une sémantique opérationnelle unique et bien définie.

Méthodologie

L'auteur emploie une analyse comparative entre la sémantique de trace standard et la sémantique de trace non standard, en utilisant des concepts d'interprétation abstraite et de théorie des points fixes.

Formalisation de la Sémantique de Trace :
- Sémantique Standard : Définie via les points fixes inférieurs ($lfp$) et supérieurs ($gfp$) sur le treillis des traces finies ( $\Sigma^*$ ) et infinies ( $\Sigma^\infty$ ) indexées par $\mathbb{N}$ .
- Sémantique Non Standard : Étendue aux traces indexées par des ensembles non standards tels que $\mathbb{N} + \delta$ (traces non standards vers l'avant avec un futur infini) et $\mathbb{N} - \delta$ (traces non standards vers l'arrière avec un passé infini), où $\delta > 0$ . Ces ensembles modélisent des structures de type Skolem.
Abstraction et Équivalence :
- L'article définit une fonction d'abstraction $\alpha_S$ faisant correspondre la sémantique de trace à l'ensemble des triplets de Hoare valides.
- Le Théorème 1 prouve que l'ensemble des triplets de Hoare valides pour la sémantique standard ( $H(L)$ ) est identique à l'ensemble des triplets valides pour la sémantique non standard ( $\tilde{H}(L)$ ). Cela confirme que les règles de preuve de Hoare standard sont insuffisantes pour exclure les interprétations non standards.
Remède Proposé (Standardisation) :
Pour résoudre cette ambiguïté, l'auteur propose d'enrichir la sémantique axiomatique avec des obligations de preuve supplémentaires inspirées des méthodes de preuve de terminaison (spécifiquement la méthode de Knuth et les variantes ordinales).
- Prévenir les Traces Vers l'Avant Non Standards : La logique est étendue pour exiger l'existence d'une fonction croissante $K$ associant les positions de trace à des ordinaux ( $\mathcal{O}$ ) telle que le compteur de boucle soit borné par le premier ordinal limite infini $\omega$ . Puisque les parties entières non standards ne peuvent être isomorphes par ordre à des ordinaux bien fondés, cette exigence élimine les traces vers l'avant infinies non standards.
- Prévenir les Traces Vers l'Arrière Non Standards : Une exigence duale est introduite pour les traces vers l'arrière, exigeant une fonction décroissante $K$ (antitone) qui garantit que le parcours vers l'arrière se termine dans une borne standard.

Contributions Clés

Identification des Modèles Non Standards : L'article établit formellement que la logique de Hoare souffre du même problème de non-unicité que l'arithmétique de Peano sans la condition de catégoricité de Dedekind. Il montre que les invariants de boucle en logique du premier ordre ne peuvent pas distinguer les modèles de traces standards des modèles de traces non standards en raison du théorème de compacité.
Équivalence des Théories : Il prouve que les théories de la logique de Hoare standard et non standard sont identiques ( $H(L) = \tilde{H}(L)$ ), ce qui signifie que les preuves existantes n'excluent pas intrinsèquement les exécutions non standards.
Standardisation via les Contraintes Ordinales : L'article propose une méthode pour restreindre la sémantique axiomatique aux modèles standards en ajoutant des obligations de preuve impliquant des compteurs ordinaux (bornés par $\omega$ pour les traces vers l'avant et exigeant la terminaison pour les traces vers l'arrière).
Préservation des Preuves Standards : Un résultat crucial est que ces obligations de preuve supplémentaires sont toujours satisfaites par la sémantique de trace standard. Par conséquent, si l'on suppose l'interprétation standard (comme c'est implicite dans la plupart des utilisations de la logique de Hoare), les preuves de Hoare existantes restent valides et inchangées. Les nouvelles obligations servent à exclure formellement les modèles non standards sans modifier la vérification pratique des programmes standards.

Résultats

Équivalence Théorique : L'ensemble des triplets de Hoare valides pour les modèles de trace non standards est exactement le même que pour les modèles standards.
Résolution de l'Ambiguïté : En imposant les conditions de bornage ordinal (Équations 9 et 10), la sémantique axiomatique est restreinte au modèle standard.
Applicabilité : La standardisation proposée est compatible avec les algorithmes d'analyse statique et de typage existants qui reposent sur la logique de Hoare, à condition que l'hypothèse sous-jacente de la sémantique standard soit explicite ou que les nouvelles obligations soient vérifiées (ce qui est trivial pour les modèles standards).
Limites : L'article note que dans les Logiques de Hoare Abstraites, où le domaine concret est remplacé par un domaine abstrait qui peut ne pas être assez expressif pour définir les fonctions ordinales requises, les méthodes de standardisation pourraient ne pas être directement applicables.

Signification

L'article soutient que l'affirmation commune selon laquelle « la sémantique axiomatique définit la signification d'un programme par ses effets sur les assertions logiques » est techniquement erronée car la signification définie n'est pas unique à un isomorphisme près. La signification réside dans :

Clarification des Fondements : Il souligne que la logique de Hoare, comme l'arithmétique de Peano, nécessite une condition de « catégoricité » (dans ce cas, la standardisation via des bornes ordinales) pour garantir une interprétation opérationnelle unique.
Formalisation des Hypothèses Implicites : Il rend explicite l'hypothèse implicite selon laquelle la logique de Hoare est interprétée sur des modèles de calcul standards.
Pont entre Logique et Sémantique : Il démontre comment les techniques de preuve de terminaison (utilisant des ordinaux) peuvent être intégrées à la sémantique axiomatique pour éliminer les interprétations non standards, alignant ainsi plus rigoureusement la sémantique axiomatique avec la sémantique de trace opérationnelle.

L'auteur conclut que, bien que les preuves de la logique de Hoare n'aient pas besoin d'être modifiées pour les modèles standards, le cadre théorique doit reconnaître et exclure formellement les modèles non standards pour revendiquer une définition unique de la sémantique des programmes.