Logique de Hoare

Un article de Wikipédia, l'encyclopédie libre.
Aller à : navigation, rechercher

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. Hoare s'est inspiré du travail sur les méthodes formelles dans les organigrammes de Robert Floyd, qui lui n'avait pas eu connaissance des travaux d'Alan Turing sur le sujet.

La logique de Hoare a des axiomes et des règles d'inférence pour toutes les instructions de base d'un langage de programmation impératif. Hoare rajoute dans son papier originel des règles pour les procédures, les sauts, les pointeurs et la concurrence.

Triplet de Hoare[modifier | modifier le code]

La logique de Hoare décrit les évolutions possibles de l'état d'un programme informatique. Les évolutions sont modélisées par des règles et l'état d'un programme est symbolisé par un triplet appelé triplet de Hoare :

\{P\}\;C\;\{Q\},

où P et Q sont des prédicats et C est une commande (une action sur le programme). La condition P est appelée la précondition et Q la postcondition.

Règles[modifier | modifier le code]

Règle de l'affectation[modifier | modifier le code]

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

Ici, P[E/x] désigne l'expression P dans laquelle les occurrences de la variable x ont été remplacées par l'expression E.

La règle d'affectation signifie que \{P[E/x]\} sera vrai si et seulement si \{P\} l'est après l'affectation.

Quelques triplets respectant la règle d'affectation :

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

La règle d'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,

\{ 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.

Règle de composition[modifier | modifier le code]

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.

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

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

\{ x + 1 = 43\} \ y:=x + 1\ \{y =43 \}
\{ y = 43\} \ z:=y\ \{z =43 \}

la règle de composition nous permet de conclure :

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


Règle de la conditionnelle[modifier | modifier le code]

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

Règle de la conséquence[modifier | modifier le code]


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

Il est à noter que lorsque l'on prouve automatiquement qu'un programme est correct, ce seront les implications les plus dures à prouver issues de l'application de cette règle qu'il restera à faire manuellement à la fin.

Règle de l'itération[modifier | modifier le code]

\frac { \{P \wedge B \}\ S\ \{P\} }
              { \{P \}\ \textbf{tant que}\ B\ \textbf{faire}\ S\ \textbf{fait}\ \{\neg B \wedge P\} }
\!

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

Exemples[modifier | modifier le code]

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


Voir aussi[modifier | modifier le code]

Références[modifier | modifier le code]

  1. C. A. R. Hoare. [PDF] "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, octobre 1969. DOI 10.1145/363235.363259.