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

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

Règle de l'affectation

$\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

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

$\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

$\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

$\frac { \{P \wedge B \}\ S\ \{P\} } { \{P \}\ \textbf{TANT QUE}\ B\ \textbf{FAIRE}\ S\ \textbf{FAIT}\ \{\neg B \wedge P\} } \!$

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

Exemples

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

• Sémantique axiomatique

Références

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