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

↑ 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

Catégorie :

Méthode formelle

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Logique de Hoare de Wikipédia en français (auteurs)

Игры ⚽ Поможем написать реферат

Regardez d'autres dictionnaires:

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… … Wikipédia en Français
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… … Wikipédia en Français
Logique De Séparation — La logique de séparation (du terme anglais « Separation Logic »), attribuée à John C. Reynolds, est une extension de la logique de Hoare. Par rapport à cette dernière, elle permet de raisonner plus simplement sur les programmes qui… … Wikipédia en Français
Logique de separation — Logique de séparation La logique de séparation (du terme anglais « Separation Logic »), attribuée à John C. Reynolds, est une extension de la logique de Hoare. Par rapport à cette dernière, elle permet de raisonner plus simplement sur… … Wikipédia en Français
Logique de séparation — La logique de séparation (du terme anglais « Separation Logic »), attribuée à John C. Reynolds, est une extension de la logique de Hoare. Par rapport à cette dernière, elle permet de raisonner plus simplement sur les programmes qui… … Wikipédia en Français
C.A.R. Hoare — Charles Antony Richard Hoare C.A.R. Hoare en 2005. Sir Charles Antony Richard Hoare (généralement appelé Tony Hoare ou C.A.R. Hoare), né le 11 janvier 1934 à Colombo, Sri Lanka, est un professeur émérite britannique du Oxford University Computing … Wikipédia en Français
C.A. Hoare — Charles Antony Richard Hoare C.A.R. Hoare en 2005. Sir Charles Antony Richard Hoare (généralement appelé Tony Hoare ou C.A.R. Hoare), né le 11 janvier 1934 à Colombo, Sri Lanka, est un professeur émérite britannique du Oxford University Compu … Wikipédia en Français
C. A. R. Hoare — Charles Antony Richard Hoare C.A.R. Hoare en 2005. Sir Charles Antony Richard Hoare (généralement appelé Tony Hoare ou C.A.R. Hoare), né le 11 janvier 1934 à Colombo, Sri Lanka, est un professeur émérite britannique du Oxford University Compu … Wikipédia en Français
Charles Antony Richard Hoare — C.A.R. Hoare en 2011. Sir Charles Antony Richard Hoare (généralement appelé Tony Hoare ou C.A.R. Hoare), né le 11 janvier 1934 à Colombo, Sri Lanka, est un professeur émérite britannique du Oxford University Computing Laboratory. Il est connu… … Wikipédia en Français
Tony Hoare — Charles Antony Richard Hoare C.A.R. Hoare en 2005. Sir Charles Antony Richard Hoare (généralement appelé Tony Hoare ou C.A.R. Hoare), né le 11 janvier 1934 à Colombo, Sri Lanka, est un professeur émérite britannique du Oxford University Compu … Wikipédia en Français

Dictionnaires et Encyclopédies sur 'Academic'

Logique de Hoare

Sommaire

Triplet de Hoare