L8) Sémantique axiomatique

Prouver qu’un programme est correct

Un programme qui s’exécute sans erreur visible n’est pas nécessairement correct. Seule une preuve mathématique peut le garantir. La sémantique axiomatique fournit les outils pour y parvenir.

Où se situe cet article ?

Dans L5, nous avons vu trois façons de donner du sens à un programme :

Opérationnelle : « comment ça s’exécute » — approfondie dans L6
Dénotationnelle : « quelle fonction mathématique ça calcule » — approfondie dans L7
Axiomatique : « quelles propriétés ça garantit » — c’est le sujet de cet article

Avec L8, la trilogie sémantique est complète. Chaque approche a ses forces : la SOS (Structural Operational Semantics, sémantique opérationnelle structurelle) décrit le comment, la dénotationnelle le quoi, et l’axiomatique le pourquoi c’est correct.

Pourquoi c’est important ?

Les tests peuvent montrer la présence de bugs, jamais leur absence. Un programme peut passer des milliers de tests et contenir une erreur subtile qui ne se manifeste que dans un cas particulier. Les sondes spatiales, les systèmes de freinage, les protocoles cryptographiques — dans ces domaines, « ça a l’air de marcher » ne suffit pas.

La sémantique axiomatique, fondée sur la logique de Hoare, permet de prouver qu’un programme est correct : qu’il fait exactement ce qu’il doit faire, pour toutes les entrées possibles, pas seulement celles qu’on a testées. Cette approche a donné naissance au Design by Contract (conception par contrat — Eiffel, Ada/SPARK), aux contrats intégrés dans les langages modernes, et aux prouveurs de programmes comme Dafny ou Frama-C (outils de vérification automatique de code).

L’idée en une phrase

La sémantique axiomatique décrit le sens d’un programme par les propriétés logiques qu’il préserve : si certaines conditions sont vraies avant l’exécution, d’autres le seront après.

Expliquons pas à pas

Exemple 1 : Le distributeur de café (reprise)

Reprenons le distributeur de café de L5 pour voir comment l’approche axiomatique raisonne sur ce système.

En sémantique opérationnelle, on décrivait les transitions :

(attente, 0€) → (attente, 1€) → (prêt, 2€) → (distribution, 0€)

En sémantique dénotationnelle, on décrivait la fonction :

distributeur(2€, café) = café

En sémantique axiomatique, on décrit ce que le système garantit :

{argent ≥ 2€ ∧ bouton = café}
  appuyer
{café_distribué = vrai ∧ argent = 0€}

Décryptage :

{argent ≥ 2€ ∧ bouton = café} : la précondition — ce qui doit etre vrai avant

appuyer : la commande — l’action exécutée

{café_distribué = vrai ∧ argent = 0€} : la postcondition — ce qui est garanti après

∧ : conjonction logique (« et »)

Lecture : « Si l’utilisateur a inséré au moins 2 euros ET a appuyé sur le bouton café, ALORS le café sera distribué ET le compteur d’argent sera remis à zéro. »

On ne dit pas comment la machine fonctionne (ce sont des engrenages ? un micro-contrôleur ?). On ne dit pas quelle fonction elle calcule. On dit uniquement : voici le contrat — ce qui est garanti si les conditions d’entrée sont remplies.

C’est exactement l’esprit de la sémantique axiomatique : raisonner sur les spécifications, pas sur l’implémentation.

Les triplets de Hoare

Le formalisme central de la sémantique axiomatique est le triplet de Hoare :

{P} C {Q}

Qu’est-ce qu’un triplet de Hoare ?

Inventé par Tony Hoare en 1969, c’est une notation qui lie trois éléments :

P (précondition) : une assertion logique sur l’état du programme avant l’exécution

C (commande) : l’instruction ou le programme à exécuter

Q (postcondition) : une assertion logique sur l’état du programme après l’exécution

Le triplet {P} C {Q} se lit : « si P est vrai avant d’exécuter C, et si C termine, alors Q est vrai après. »

Exemples concrets :

{x = 5}  x := x + 1  {x = 6}

Lecture : « Si x vaut 5 avant l’affectation, alors x vaut 6 après. »

{x > 0}  x := x * 2  {x > 0}

Lecture : « Si x est positif avant, alors x reste positif après la multiplication par 2. »

{vrai}  x := 7  {x = 7}

Lecture : « Quel que soit l’état initial (la précondition vrai est toujours satisfaite), après x := 7, x vaut 7. »

La notation {vrai} comme précondition :

La précondition vrai (ou true) signifie « aucune condition requise » — le triplet est valable quel que soit l’état de départ. C’est la précondition la plus faible possible.

Les axiomes et règles de la logique de Hoare

La puissance de la logique de Hoare réside dans un petit ensemble de règles qui permettent de construire des preuves de correction pour des programmes complets, brique par brique.

Axiome d’affectation

C’est la règle la plus fondamentale — et la plus surprenante au premier abord :

─────────────────────────── (Affectation)
{Q[x / e]}  x := e  {Q}

Décryptage :

Q[x / e] (lu « Q où x est remplacé par e ») : on prend la postcondition Q et on remplace chaque occurrence de x par l’expression e

Pas de prémisse au-dessus de la barre : c’est un axiome (toujours vrai, sans condition)

La règle se lit « à l’envers » : on part de la postcondition Q et on remonte vers la précondition

Pourquoi à l’envers ? C’est contre-intuitif, mais logique : pour savoir ce qui doit etre vrai avant l’affectation, on regarde ce qu’on veut après et on « défait » l’affectation.

Exemple :

On veut prouver {???} x := x + 1 {x = 6}.

Appliquons l’axiome : la postcondition est x = 6, donc la précondition est (x = 6)[x / (x+1)], c’est-à-dire on remplace x par x + 1 dans x = 6 :

(x = 6)[x / (x + 1)] = (x + 1 = 6) = (x = 5)

Résultat :

─────────────────────────────── (Affectation)
{x = 5}  x := x + 1  {x = 6}

Vérification intuitive : si x vaut 5 avant, et qu’on ajoute 1, alors x vaut bien 6 après. L’axiome fonctionne.

Autre exemple :

{???}  x := x * 2  {x > 0}

Q = (x > 0)
Q[x / (x * 2)] = (x * 2 > 0) = (x > 0)

─────────────────────────────── (Affectation)
{x > 0}  x := x * 2  {x > 0}

Ici, la précondition et la postcondition sont identiques : multiplier un nombre positif par 2 le garde positif.

Règle de séquence

Quand on enchaîne deux instructions, on compose les preuves :

{P} c₁ {R}    {R} c₂ {Q}
────────────────────────── (Séquence)
    {P}  c₁ ; c₂  {Q}

Décryptage :

R est une assertion intermédiaire : la postcondition de c₁ et la précondition de c₂

La règle dit : si c₁ transforme P en R, et c₂ transforme R en Q, alors la séquence c₁;c₂ transforme P en Q

C’est une composition de preuves, comme enchaîner deux maillons d’une chaîne logique

Exemple :

Prouvons {x = 0} x := x + 1 ; x := x * 3 {x = 3} :

Étape 1 — Axiome d'affectation pour x := x * 3 avec Q = (x = 3) :
    Q[x / (x * 3)] = (x * 3 = 3) = (x = 1)
    Donc : {x = 1}  x := x * 3  {x = 3}

Étape 2 — Axiome d'affectation pour x := x + 1 avec Q = (x = 1) :
    Q[x / (x + 1)] = (x + 1 = 1) = (x = 0)
    Donc : {x = 0}  x := x + 1  {x = 1}

Étape 3 — Règle de séquence avec R = (x = 1) :

    {x = 0} x := x + 1 {x = 1}    {x = 1} x := x * 3 {x = 3}
    ──────────────────────────────────────────────────────────── (Séquence)
                {x = 0}  x := x + 1 ; x := x * 3  {x = 3}

Observation : on travaille « de droite à gauche » — on commence par la dernière instruction et on remonte. C’est la méthode naturelle avec l’axiome d’affectation.

Règle du if

{P ∧ b} c₁ {Q}    {P ∧ ¬b} c₂ {Q}
────────────────────────────────────── (If)
  {P}  if b then c₁ else c₂  {Q}

Décryptage :

P ∧ b : la précondition P est vraie ET la condition b est vraie (on entre dans la branche then)

P ∧ ¬b : la précondition P est vraie ET la condition b est fausse (on entre dans la branche else)

¬b : négation de b (« b est faux »)

Les deux branches doivent aboutir à la même postcondition Q

La règle dit : peu importe la branche prise, on arrive à Q

Exemple :

Prouvons {vrai} if x ≥ 0 then y := x else y := -x {y = |x|} :

Branche then (x ≥ 0) :
    {vrai ∧ x ≥ 0} y := x {y = |x|}
    Si x ≥ 0, alors x = |x|, donc y := x donne y = |x|  ✓

Branche else (x < 0) :
    {vrai ∧ ¬(x ≥ 0)} y := -x {y = |x|}
    Si x < 0, alors -x = |x|, donc y := -x donne y = |x|  ✓

    {vrai ∧ x ≥ 0} y := x {y = |x|}    {vrai ∧ x < 0} y := -x {y = |x|}
    ──────────────────────────────────────────────────────────────────────── (If)
            {vrai}  if x ≥ 0 then y := x else y := -x  {y = |x|}

Ce programme calcule bien la valeur absolue de x, et la preuve le confirme formellement.

Règle du while et invariant de boucle

C’est la règle la plus puissante — et la plus difficile :

    {I ∧ b}  c  {I}
─────────────────────────── (While)
{I}  while b do c  {I ∧ ¬b}

Décryptage :

I est l’invariant de boucle : une propriété qui reste vraie à chaque itération

La prémisse dit : si l’invariant I est vrai ET la condition b est vraie, alors après une itération de c, l’invariant I est toujours vrai

La conclusion dit : si I est vrai au départ, alors à la sortie de la boucle (quand b devient faux), on a I ET ¬b

Analogie : L’invariant est comme un équilibriste sur un fil. À chaque pas (itération), il peut osciller (l’état change), mais il reste toujours sur le fil (l’invariant est préservé). Quand il s’arrête (la boucle termine), on sait qu’il est toujours sur le fil (I) et qu’il a atteint l’autre côté (¬b).

L’invariant est la clé. Trouver le bon invariant est souvent la partie la plus difficile d’une preuve de correction. C’est un art autant qu’une science.

Règle de conséquence

Cette règle permet d’ajuster les préconditions et postconditions :

P' ⟹ P    {P} C {Q}    Q ⟹ Q'
──────────────────────────────── (Conséquence)
         {P'} C {Q'}

Décryptage :

P' ⟹ P : P’ est plus forte que P (P’ implique P) — on renforce la précondition

Q ⟹ Q' : Q implique Q’ — on affaiblit la postcondition

Si on sait que {P} C {Q}, et qu’on dispose de conditions plus fortes en entrée ou plus faibles en sortie, le triplet reste valide

Intuition : Si un programme est correct sous certaines conditions, il l’est a fortiori sous des conditions plus restrictives (précondition renforcée) ou avec des garanties moindres (postcondition affaiblie).

Exemple :

On sait que {x = 5} x := x + 1 {x = 6}.

Or x = 6 implique x > 0. Par la règle de conséquence :

{x = 5} x := x + 1 {x = 6}    (x = 6) ⟹ (x > 0)
───────────────────────────────────────────────────── (Conséquence)
          {x = 5}  x := x + 1  {x > 0}

On a affaibli la postcondition : au lieu de garantir que x vaut exactement 6, on garantit seulement qu’il est positif. C’est moins précis, mais toujours correct.

Les invariants de boucle

Qu’est-ce qu’un invariant de boucle ?

Un invariant de boucle est une propriété logique qui est :

Vraie avant la première itération (initialisation)

Préservée par chaque itération (conservation)

Utile à la sortie : combinée avec la condition d’arret, elle donne la postcondition souhaitée

C’est le « fil rouge » qui traverse toutes les itérations et permet de conclure que le résultat est correct.

Exemple : somme des entiers de 1 à n

Considérons ce programme qui calcule la somme 1 + 2 + … + n :

s := 0 ;
i := 1 ;
while i ≤ n do
    s := s + i ;
    i := i + 1

Postcondition souhaitée : {s = n × (n + 1) / 2}

Trouver l’invariant :

L’idée est que s contient toujours la somme des entiers de 1 à i - 1. Formellement :

I : s = (i - 1) × i / 2  ∧  1 ≤ i ≤ n + 1

Comment trouver un invariant ?

Quelques heuristiques :

Regarder la postcondition : l’invariant est souvent une « version partielle » du résultat final

Remplacer une constante par une variable : dans s = n(n+1)/2, remplacer n par la variable de boucle i - 1

Vérifier sur les cas limites : l’invariant est-il vrai au début (i = 1, s = 0) ? À la fin (i = n + 1) ?

Preuve de correction :

1. Initialisation : Avant la boucle, s = 0 et i = 1.

I = (0 = (1 - 1) × 1 / 2) ∧ (1 ≤ 1 ≤ n + 1)
  = (0 = 0) ∧ (1 ≤ 1 ≤ n + 1)
  = vrai  ✓  (en supposant n ≥ 0)

2. Conservation : On suppose I ∧ i ≤ n et on exécute le corps :

Avant :  s = (i - 1) × i / 2  ∧  i ≤ n
Après s := s + i :  s_new = (i - 1) × i / 2 + i = i × (i + 1) / 2
Après i := i + 1 :  i_new = i + 1

Vérification de I avec les nouvelles valeurs :
    s_new = (i_new - 1) × i_new / 2
    i × (i + 1) / 2 = ((i + 1) - 1) × (i + 1) / 2
    i × (i + 1) / 2 = i × (i + 1) / 2  ✓

3. Terminaison de la boucle : Quand la boucle s’arrete, ¬(i ≤ n), donc i = n + 1 (car i augmente de 1 à chaque itération et i ≤ n + 1 par l’invariant).

I ∧ ¬(i ≤ n) :
    s = (i - 1) × i / 2  ∧  i = n + 1
    s = ((n + 1) - 1) × (n + 1) / 2
    s = n × (n + 1) / 2  ✓

La preuve est complète : le programme calcule bien la somme des entiers de 1 à n.

Correction partielle vs correction totale

Jusqu’ici, nous avons parlé de correction partielle. Il existe une distinction importante :

Correction partielle	Correction totale
Notation	`{P} C {Q}`
Signification	Si C termine, alors Q est vrai
Terminaison	Non garantie
Difficulté	Plus simple

Qu’est-ce que la correction partielle ?

Le triplet {P} C {Q} dit : « Si P est vrai au départ ET si C finit par terminer, alors Q sera vrai. » Mais il ne dit rien sur la terminaison. Si C boucle indéfiniment, le triplet est vacuously true (trivialement vrai, car la condition « si C termine » n’est jamais remplie).

Exemple : {vrai} while true do skip {faux} est un triplet de correction partielle valide. Puisque la boucle ne termine jamais, la postcondition faux n’est jamais atteinte, et le triplet n’est jamais violé.

Qu’est-ce que la correction totale ?

Le triplet [P] C [Q] (avec des crochets au lieu d’accolades) dit : « Si P est vrai, alors C termine ET Q est vrai après. » C’est une garantie plus forte : on prouve à la fois que le résultat est correct ET que le calcul se termine.

Prouver la terminaison : les variants de boucle

Pour passer de la correction partielle à la correction totale, il faut prouver la terminaison. L’outil principal est le variant (ou fonction de terminaison).

Qu’est-ce qu’un variant de boucle ?

Un variant est une expression à valeurs entières qui :

Est positive (ou nulle) à chaque itération

Décroît strictement à chaque itération

Puisqu’un entier ne peut pas décroître indéfiniment tout en restant positif, la boucle doit terminer.

Exemple : Pour la boucle de la somme, le variant est n + 1 - i :

Avant la boucle : n + 1 - 1 = n ≥ 0 (si n ≥ 0) ✓
À chaque itération : i augmente de 1, donc n + 1 - i décroît de 1 ✓
Quand le variant atteint 0 : i = n + 1, la condition i ≤ n est fausse, la boucle s’arrete ✓

Invariant vs variant :

Invariant : ce qui ne change pas (propriété préservée) — prouve la correction

Variant : ce qui change (quantité qui décroît) — prouve la terminaison

Les deux ensemble donnent la correction totale

Application à BP3

Que pourrait-on prouver axiomatiquement sur une grammaire BP3 ?

Terminaison des grammaires :

En BP3, une grammaire peut boucler indéfiniment si une règle est récursive sans condition d’arret :

RND[1]
gram#1[1] S --> do4 S
gram#1[2] S --> do4

En sémantique axiomatique, on pourrait formuler :

{poids(gram#1[1]) = w ∧ w > 0}
  dériver(S)
{nombre_dérivations ≤ f(w)}

Avec des poids décrémentaux (<50-12>), le variant serait la somme des poids des règles récursives : elle décroît à chaque application jusqu’à atteindre zéro, forçant la terminaison.

Propriétés musicales :

On pourrait exprimer des invariants musicaux :

{tessiture ⊆ [do3, do6]}
  dériver_complet(Grammaire)
{∀ note ∈ résultat : do3 ≤ note ≤ do6}

« Si toutes les notes terminales de la grammaire sont dans la tessiture [do3, do6], alors le résultat restera dans cette tessiture. »

Pourquoi c’est la sémantique la moins utilisée pour BP3 :

Pas de boucles classiques : BP3 utilise la réécriture récursive, pas des boucles while. L’axiome d’affectation ne s’applique pas directement.
Stochasticité (caractère probabiliste du processus de dérivation) : la logique de Hoare classique est déterministe. Prouver des propriétés sur un processus aléatoire demande des extensions probabilistes (logiques de Hoare probabilistes).
Complexité : les preuves axiomatiques pour des grammaires stochastiques à poids décrémentaux seraient très lourdes.

La sémantique opérationnelle (L6) reste l’outil le plus naturel pour BP3. Pour une exploration détaillée, voir la série B.

Tableau comparatif des trois sémantiques

Critère	Opérationnelle (SOS)	Dénotationnelle	Axiomatique (Hoare)
Question	Comment ça s’exécute ?	Quelle fonction ça calcule ?	Qu’est-ce que ça garantit ?
Formalisme	Règles de transition	Fonctions sur domaines	Pré/postconditions
Notation	`⟨e, σ⟩ ⟹ ⟨e', σ'⟩`	`e : D → D'`	`{P} C {Q}`
Forces	Proche du code, exécutable	Compositionnelle, abstraite	Preuves de correction
Faiblesses	Verbeux, bas niveau	Difficile pour les effets	Annotations manuelles
Idéal pour	Interpréteurs, débogueurs	Optimisation, équivalence	Vérification, contrats
Gère la stochasticité	Naturellement (via probabilités)	Via monades probabilistes	Extensions nécessaires
Gère l’état mutable	Naturellement (via configurations)	Via monades d’état	Naturellement (via assertions)
Pour BP3	Choix principal (SOS)	Possible mais complexe	Limité (pas de boucles classiques)

Outils modernes de vérification formelle

La logique de Hoare est restée longtemps un outil théorique. Depuis les années 2000, des outils pratiques ont rendu la vérification formelle accessible.

Prouveurs interactifs :

Coq (France, INRIA) : prouveur de théorèmes basé sur la théorie des types. Utilisé pour certifier le compilateur CompCert (compilateur C formellement vérifié), les fondements mathématiques (théorème des quatre couleurs), et des protocoles cryptographiques
Isabelle/HOL (Cambridge/Munich) : prouveur général utilisé dans la vérification de systèmes d’exploitation (seL4, micro-noyau formellement vérifié) et de protocoles
Lean (Microsoft Research) : prouveur récent, très actif dans la communauté mathématique (projet Mathlib)

Vérification intégrée aux langages :

SPARK/Ada : sous-ensemble d’Ada avec des contrats (préconditions, postconditions, invariants) vérifiés statiquement. Utilisé dans l’aéronautique, le ferroviaire et la défense
Dafny (Microsoft Research) : langage avec vérification automatique. On écrit les invariants, Dafny prouve automatiquement la correction
Eiffel : pionnier du Design by Contract (Bertrand Meyer, 1986). Les préconditions (require), postconditions (ensure) et invariants de classe (invariant) sont intégrés au langage

Design by Contract :

L’idée de Bertrand Meyer est d’appliquer les triplets de Hoare directement dans le code :

-- Exemple en Eiffel (syntaxe simplifiée)
retirer (montant : INTEGER)
    require
        montant > 0
        solde >= montant
    do
        solde := solde - montant
    ensure
        solde = old solde - montant
        solde >= 0
    end

Ce style a été adopté (sous diverses formes) par Java (@Contract), Python (assert), Kotlin (require/ensure), et bien d’autres.

Un peu d’histoire

Robert Floyd (1967) pose les fondations avec sa méthode des « assertions intermédiaires » sur les organigrammes. L’idée : annoter chaque point d’un programme avec une assertion logique et vérifier que les transitions préservent ces assertions. Floyd est le premier à formaliser la notion d’invariant de boucle.

C.A.R. Hoare (1969) publie « An Axiomatic Basis for Computer Programming » dans Communications of the ACM. Il distille les idées de Floyd en un système déductif élégant : les triplets {P} C {Q} et un petit ensemble de règles (affectation, séquence, if, while, conséquence). L’article, d’une concision remarquable (12 pages), est l’un des plus cités de l’informatique.

Edsger Dijkstra (1975-1976) renverse la perspective avec le calcul des plus faibles préconditions (weakest preconditions). Au lieu de demander « cette précondition est-elle suffisante ? », il demande « quelle est la précondition la plus faible qui garantit cette postcondition ? ». La notation wp(C, Q) donne la plus faible précondition P telle que {P} C {Q}. Son livre A Discipline of Programming (1976) systématise cette approche et influence profondément le génie logiciel.

wp et la logique de Hoare :

Le calcul wp de Dijkstra est en quelque sorte la version « mécanisée » de la logique de Hoare. Pour l’axiome d’affectation, wp(x := e, Q) = Q[x / e] — exactement la règle de Hoare, mais formulée comme un calcul automatique plutôt qu’une déduction manuelle. C’est ce calcul qui est à la base des vérificateurs automatiques modernes comme Dafny.

Ce qu’il faut retenir

Triplet de Hoare {P} C {Q} : si P est vrai avant et C termine, alors Q est vrai après. C’est le formalisme central de la sémantique axiomatique.
Axiome d’affectation : on « remonte » de la postcondition vers la précondition en substituant la variable. {Q[x/e]} x := e {Q}.
Invariant de boucle : propriété préservée à chaque itération. Trouver le bon invariant est le coeur de la preuve.
Variant de boucle : quantité qui décroît strictement à chaque itération, garantissant la terminaison.
Correction partielle vs totale : {P} C {Q} ne garantit pas la terminaison ; [P] C [Q] la garantit.
Règle de conséquence : permet de renforcer les préconditions et d’affaiblir les postconditions.
Pour BP3 : la sémantique axiomatique est la moins directe (pas de boucles classiques, stochasticité), mais les concepts d’invariant et de terminaison restent pertinents pour raisonner sur les grammaires.

Pour aller plus loin

Article fondateur : Hoare, C.A.R. (1969). « An Axiomatic Basis for Computer Programming ». Communications of the ACM, 12(10), 576-580.
Le calcul wp : Dijkstra, E.W. (1976). A Discipline of Programming. Prentice-Hall. — systématise les plus faibles préconditions.
Manuel de référence : Winskel, G. (1993). The Formal Semantics of Programming Languages, chapitre 6. MIT Press. — traitement rigoureux de la logique de Hoare.
Introduction accessible : Nielson, H.R. & Nielson, F. (1992). Semantics with Applications: A Formal Introduction, chapitre 6. Wiley. — présentation pédagogique progressive.
Dans cette série : L6 pour la sémantique opérationnelle, L7 pour l’approche fonctionnelle.

Glossaire

Affaiblissement : remplacement d’une postcondition par une condition plus faible (moins précise mais toujours correcte). Si x = 6 est vrai, alors x > 0 l’est aussi : on a affaibli la postcondition.
Assertion : propriété logique sur l’état du programme à un point donné. Les préconditions et postconditions sont des assertions.
Axiome : règle sans prémisse, toujours applicable. L’axiome d’affectation est le seul axiome de la logique de Hoare.
Correction partielle : propriété {P} C {Q} — si C termine, Q est vrai. Ne dit rien sur la terminaison.
Correction totale : propriété [P] C [Q] — C termine ET Q est vrai. Combine correction partielle et terminaison.
Design by Contract : méthodologie de programmation où les fonctions sont annotées avec des préconditions, postconditions et invariants. Inventé par Bertrand Meyer (Eiffel, 1986).
Invariant de boucle : propriété logique vraie avant la boucle et préservée par chaque itération. Clé des preuves de correction des boucles.
Invariant de classe : propriété qui doit etre vraie pour tout objet d’une classe, à tout moment observable (entre les appels de méthode).
Logique de Hoare : système formel de triplets {P} C {Q} et de règles d’inférence pour prouver la correction des programmes. Introduit par C.A.R. Hoare en 1969.
Plus faible précondition (wp) : la condition P la moins restrictive telle que {P} C {Q} soit valide. Notation : wp(C, Q). Introduit par Dijkstra (1975).
Postcondition : assertion décrivant ce qui est garanti après l’exécution d’une commande. Notée Q dans {P} C {Q}.
Précondition : assertion décrivant ce qui doit etre vrai avant l’exécution d’une commande. Notée P dans {P} C {Q}.
Renforcement : remplacement d’une précondition par une condition plus forte (plus restrictive). Si on sait que {x > 0} C {Q}, alors {x = 5} C {Q} est aussi valide car x = 5 implique x > 0.
Substitution Q[x / e] : opération qui remplace chaque occurrence de la variable x par l’expression e dans la formule Q. Exemple : (x > 3)[x / (x + 1)] = (x + 1 > 3) = (x > 2).
Triplet de Hoare : notation {P} C {Q} qui lie une précondition P, une commande C et une postcondition Q. Se lit « si P est vrai avant C, et si C termine, alors Q est vrai après ».
Variant (fonction de terminaison) : expression entière positive qui décroît strictement à chaque itération d’une boucle. Son existence prouve la terminaison.
Vérification formelle : utilisation de méthodes mathématiques pour prouver qu’un système (logiciel ou matériel) satisfait sa spécification.
∧ (conjonction) : connecteur logique « et ». P ∧ Q est vrai si et seulement si P et Q sont tous les deux vrais.
¬ (négation) : connecteur logique « non ». ¬P est vrai si et seulement si P est faux.
⟹ (implication) : connecteur logique « implique ». P ⟹ Q signifie « si P est vrai, alors Q est vrai ».

Prérequis : L5
Temps de lecture : 12 min
Tags : #semantique-axiomatique #logique-hoare #verification #preuve-programme

Article précédent : L7
Série L complétée. Pour l’application à BP3, voir : série B