Logique de Hoare

La logique de Hoare, parfois appelée logique de Floyd-Hoare, est une méthode formelle définie par le chercheur en informatique britannique Tony Hoare dans un article de 1969 intitulé An Axiomatic Basis for Computer Programming^[1]. La méthode de Hoare met en place un formalisme logique permettant de raisonner sur la correction des programmes informatiques. Elle est fondée sur la syntaxe en ce sens que la correction d'un programme est décrite et démontrée par induction sur la structure du programme : à chaque règle syntaxique de construction d'un programme correspond une règle de la logique de Hoare. Elle a deux utilisations : fournir un outil de vérification formelle des programmes sans les exécuter (analyse statique), décrire rigoureusement la sémantique des langages de programmation (sémantique axiomatique).

La logique de Hoare a des axiomes pour toutes les instructions de base d'un langage de programmation impératif et des règles d'inférence pour les compositions d'instructions comme le si ... alors ... sinon ... ou le tant que. Hoare ajoute dans son article originel des règles pour les procédures, les sauts, les pointeurs et la concurrence.

Hoare s'est inspiré du travail sur les méthodes formelles dans les organigrammes de Robert Floyd^[2], qui lui n'avait pas eu connaissance des travaux d'Alan Turing sur le sujet^[3].

La logique de Hoare permet de dire comment une portion de code fait évoluer l'état d'un système. Il n'y a pas de liaison précise entre l'état antérieur et l'état postérieur, mais une simple description de l'ensemble des états antérieurs et des états postérieurs, par des prédicats. Cette intuition de transformateur de prédicats est formalisée par la notion de triplet de Hoare : ${\displaystyle \{P\}\;C\;\{Q\}}$ où P et Q sont des prédicats et C est un programme.

Le prédicat P, nommé précondition, décrit l'ensemble des états en entrée de la portion de programme C, tandis que le prédicat Q, nommé postcondition, caractérise un ensemble d'états après transformation par le code C.

La logique de Hoare fournit alors un ensemble de règles pour raisonner sur les triplets de Hoare, il s'agit donc d'un ensemble de règles de déduction constituant un système logique. Ces règles permettent donc de répondre à la question informelle suivante : « Si je connais les évolutions de l'état sur des petits bouts de code, que puis-je dire sur les évolutions réalisées par des codes plus grands qui utilisent ces petits bouts de codes ? ».

Les axiomes et règles d'inférence sont des critères syntaxiques permettant d'établir les triplets de Hoare. Elles sont définies pour chaque instruction du langage, à l'exception de la règle de la conséquence (ou de l'affaiblissement) définie indépendamment des instructions du langage.

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).

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}}\ {\textbf {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}}\ {\textbf {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).

Exemple 1
${\displaystyle \{x+1=43\}\!}$	${\displaystyle \ y:=x+1\ \!}$	${\displaystyle \{y=43\}\!}$	(Règle de l'affectation)
			${\displaystyle (x+1=43\Leftrightarrow x=42)}$
${\displaystyle \{x=42\}\!}$	${\displaystyle \ y:=x+1\ \!}$	${\displaystyle \{y=43\land x=42\}\!}$	(Règle de la conséquence)
Exemple 2
${\displaystyle \{x+1\leq N\}\!}$	${\displaystyle \ x:=x+1\ \!}$	${\displaystyle \{x\leq N\}\ \!}$	(Règle de l'affectation)
			(${\displaystyle x<N\implies x+1\leq N}$ x, N sont entiers.)
${\displaystyle \{x<N\}\!}$	${\displaystyle \ x:=x+1\ \!}$	${\displaystyle \{x\leq N\}\ \!}$	(Règle de la conséquence)

Nos règles de déductions permettent d'établir de manière syntaxique un triplet de Hoare de la forme ${\displaystyle \{P\}\;C\;\{Q\}}$. Il est à présent nécessaire de faire un lien formel avec l'intuition initiale : le programme C doit mener un état satisfaisant P vers un état satisfaisant Q. Il nous faut pour cela supposer que notre langage de programmation est équipé d'une sémantique opérationnelle, ou dénotationnelle, que l'on notera ${\displaystyle [\![C]\!]\sigma }$. On obtient ainsi un lien entre un système de déduction défini sur la syntaxe des programmes d'un langage et la sémantique de ce langage^[4].

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 ',~(\sigma \vDash P~\land ~\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}}\ {\textbf {que}}\ B\ {\textbf {faire}}\ S\ {\textbf {fait}}\ \{\neg B\wedge I\}}}\!}$

L'ouvrage en ligne Software Foundations explique comment utiliser la logique de Hoare en COQ, dans deux chapitres :

• chapitre 1 et
• chapitre 2.

• Sémantique axiomatique
• Analyse statique de programmes
• Logique de séparation

• Portail de l’informatique
• Portail de l'informatique théorique