Logique de Hoare

L'affectation est l'instruction ${\displaystyle x:=E}$, associant à la variable x la valeur de l'expression E.

${\displaystyle {\frac {}{\{P[E/x]\}\ x:=E\ \{P\}}}\!}$

Ici, ${\displaystyle P[E/x]}$ désigne l'expression P dans laquelle les occurrences de la variable x ont été remplacées par l'expression E. Par exemple, si ${\displaystyle P=(x=3)}$, ${\displaystyle P[(y+2)/x]=(y+2=3)}$. Ce remplacement est syntaxique, il faut utiliser la règle de la conséquence ensuite pour considérer ${\displaystyle y=1}$ au lieu de ${\displaystyle y+2=3}$. La règle d'affectation signifie alors que ${\displaystyle \{P[E/x]\}}$ sera vrai si et seulement si ${\displaystyle \{P\}}$ l'est après l'affectation.

Quelques triplets respectant l'axiome de l'affectation :

• ${\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}\!}$
• ${\displaystyle \{x+1\leq N\}\ x:=x+1\ \{x\leq N\}\ \!}$

L'axiome de l'affectation ne s'applique pas lorsque plusieurs noms de variables se réfèrent à la même valeur stockée en mémoire. Par exemple,

${\displaystyle \{y=3\}\ x:=2\ \{y=3\}}$

n'est un triplet valide que si x et y ne sont pas 2 références pour la même variable (phénomène d'aliasing (en)).

La règle de composition s'applique pour les programmes S et T s'ils sont exécutés séquentiellement, où S s'exécute avant T. Le programme issu de cette exécution est noté S;T.

${\displaystyle {\frac {\{P\}\ S\ \{Q\}\ ,\ \{Q\}\ T\ \{R\}}{\{P\}\ S;T\ \{R\}}}\!}$

par exemple, si l'on considère les deux triplets suivants,

${\displaystyle \{x+1=43\}\ y:=x+1\ \{y=43\}}$

${\displaystyle \{y=43\}\ z:=y\ \{z=43\}}$

la règle de composition nous permet de conclure :

${\displaystyle \{x+1=43\}\ y:=x+1;z:=y\ \{z=43\}}$

La règle de la conditionnelle permet de combiner deux programmes dans un bloc si...fin\ si, lorsque les conditions le permettent.

${\displaystyle {\frac {\{B\wedge P\}\ S\ \{Q\}\ ,\ \{\neg B\wedge P\}\ T\ \{Q\}}{\{P\}\ {\textbf {si}}\ B\ {\textbf {alors}}\ S\ {\textbf {sinon}}\ T\ {\textbf {fin\ si}}\ \{Q\}}}\!}$

Cette règle s'applique lorsqu'une postcondition ${\displaystyle Q}$ est commune aux programmes. Dans ce cas, ${\displaystyle Q}$ est la postcondition de l'ensemble du bloc conditionnel si...fin\ si.

Les règles d'inférence étant syntaxiques, elles ne s'appliquent pas si les propriétés écrites ne sont pas exactement identiques. Par exemple, ${\displaystyle x=3}$ et ${\displaystyle x+1=4}$ ne sont pas syntaxiquement identiques mais seulement équivalentes. De plus, ces règles ne s'appliquent pas non plus si les propriétés écrites sont des conséquences des propriétés déduites, par exemple si ${\displaystyle x=1}$ a été déduit, vouloir vérifier que ${\displaystyle x\geq 1}$ n'est a priori pas possible. La règle de la conséquence permet ainsi d'affaiblir les pré-conditions et post-conditions en les remplaçant par des conséquences logiques.

${\displaystyle {\frac {P\rightarrow \ P^{\prime }\ ,\ \lbrace P^{\prime }\rbrace \ S\ \lbrace Q^{\prime }\rbrace \ ,\ Q^{\prime }\rightarrow \ Q}{\lbrace P\ \rbrace \ S\ \lbrace Q\rbrace }}\!}$

Cette règle signifie que pour établir le triplet ${\displaystyle \{P\}\ S\ \{Q\}}$, il suffit d'établir à la place le triplet ${\displaystyle \{P'\}\ S\ \{Q'\}}$ où P' est une conséquence de P et Q est une conséquence de Q'. Il est à noter que dans la preuve automatique de programmes, ce seront les implications les plus dures à prouver issues de l'application de cette règle qu'il restera à faire manuellement à la fin.

${\displaystyle {\frac {\{I\wedge B\}\ S\ \{I\}}{\{I\}\ {\textbf {tant\ que}}\ B\ {\textbf {faire}}\ S\ {\textbf {fait}}\ \{\neg B\wedge I\}}}\!}$

où I est l'invariant. On le qualifie alors d'invariant de boucle.

À noter que cette règle là n'assure pas la terminaison de la boucle, mais assure seulement que la post-condition soit vérifiée une fois la boucle terminée (si elle termine).

La validité sémantique d'un triplet, notée ${\displaystyle \vDash \{P\}\;C\;\{Q\}}$, formalise l'intuition initiale vis-à-vis de la sémantique opérationnelle ou dénotationnelle : des états ${\displaystyle \sigma }$ satisfaisant P terminent dans des états ${\displaystyle \sigma '}$satisfaisant Q après exécution de C.

Soit formellement :

${\displaystyle \vDash \{P\}\;C\;\{Q\}}$ si et seulement si ${\displaystyle (\forall \sigma ,~\sigma \vDash P)\Rightarrow (\forall ~\sigma ',~\sigma '=[\![C]\!]\sigma )\Rightarrow (\sigma '\vDash Q)}$

La correction de la logique de Hoare établit la validité de l'interprétation sémantique de tout triplet de Hoare dérivable dans le système de déduction. Soit formellement : ${\displaystyle \vdash \{P\}\;C\;\{Q\}\Rightarrow \vDash \{P\}\;C\;\{Q\}}$.

La correction s'établit en prouvant la correction de chaque règle de déduction du système. La preuve procède donc par induction sur le jugement ${\displaystyle \vdash \{P\}\;C\;\{Q\}}$. Le cas le plus délicat est celui de la boucle tant que : il nécessite lui-même une récurrence sur le nombre de tour de boucles effectués pour terminer.

La complétude de la logique de Hoare est le pendant inverse : tout triplet de Hoare valide vis-à-vis de la sémantique opérationnelle ou dénotationnelle de référence peut être dérivée dans le système de déduction. Soit formellement : ${\displaystyle \vDash \{P\}\;C\;\{Q\}\Rightarrow \vdash \{P\}\;C\;\{Q\}}$.

Établir la complétude nécessite plus de travail, en deux phases essentielles.

La définition de la notion de plus faible précondition : étant donné une postcondition Q et un programme C, on cherche à établir le plus grand ensemble d'états de départ licites pour que l'exécution de C mène à des états inclus dans Q. Cette procédure est définie par induction sur le système de preuve.

Reste alors à prouver que le langage d'assertion considéré est suffisamment expressif pour que tout ensemble calculé par ce procédé de plus faible précondition corresponde effectivement à l'interprétation d'une formule de ce langage d'expression. Ce lemme s'établit lui-même par induction structurelle sur C.

La notion de correction introduite jusqu'à présent est dite partielle : elle impose la validité de la postcondition Q pour tout état atteint lorsque le programme C termine. Remarquons néanmoins que le triplet suivant est donc valide : ${\displaystyle \vDash \{Vrai\}\;Tant\ que\ vrai\ faire\ Skip\;\{Faux\}}$. En effet on demande à tout état atteint de satisfaire le prédicat faux, mais aucune exécution ne termine : c'est donc vrai par vacuité.

La notion de correction totale permet de pallier ce défaut : elle impose également la terminaison. Soit formellement :

${\displaystyle \vDash \{P\}\;C\;\{Q\}}$ si et seulement si ${\displaystyle \forall \sigma ,~\sigma \vDash P\Rightarrow (\exists ~\sigma ',~[\![C]\!]\sigma =\sigma '\land \sigma '\vDash Q)}$

Mais la logique de Hoare présentée précédemment n'est pas correcte vis-à-vis de cette interprétation : la règle de déduction de la boucle tant que n'impose pas sa terminaison. Elle doit donc être enrichie avec la notion de variant : une fonction des états dans un ensemble bien fondé dont la valeur décroit strictement à chaque tour de boucle. L'absence de chaîne infinie décroissante garantit donc la terminaison du programme.

${\displaystyle {\frac {\{I\wedge B\wedge V=z\}\ S\ \{I\wedge V<z\}}{\{I\}\ {\textbf {tant\ que}}\ B\ {\textbf {faire}}\ S\ {\textbf {fait}}\ \{\neg B\wedge I\}}}\!}$