Application de la logique de Hoare aux réseaux de régulation génétique - Article 3 : La logique de Hoare

Bien que mes précédents articles traitaient de bio-informatique (et plus précisément du modèle de réseau de régulation génétique), celui-ci sera davantage orienté logique et informatique. En effet, je serai amené lors de mon stage de Master Recherche à utiliser la logique de Hoare, développée par C. A. R. Hoare en 1969, dans son article intitulé An Axiomatic Basis for Computer Programming.

Présentation de la logique de Hoare

La logique de Hoare permet de caractériser un programme informatique (ou, plus généralement, un algorithme informatique) à l'aide de deux conditions : une pré-condition et une post-condition. On obtient donc un triplet de Hoare de la forme suivante : (pré-condition, programme, post-condition) qui spécifie que si la pré-condition est vraie avant l'exécution du programme, alors la post-condition sera vraie après son exécution. Il est à noter cependant que sous sa forme dite partielle (telle que je la présente ici), la logique de Hoare ne présume en rien de la terminaison d'un programme ; aussi, la post-condition ne sera finalement vérifiée que sous l'hypothèse que le programme se termine.
Une formule en logique de Hoare est généralement représentée selon la notation suivante :

{ P } Q { R }

Q est le programme, et P et R sont respectivement la pré-condition et la post-condition.

Règles et axiomes

Afin de construire la logique de Hoare, comme pour toute logique, nous avons besoin de formuler diverses règles. La première sera un axiome concernant l'affectation. Celui-ci peut s'écrire :

{ R [var/expr] } var := expr { R }

Ici, var représente un nom de variable, et expr représente une expression dont on peut calculer la valeur avant l'exécution du programme. De plus, la syntaxe de la pré-condition signifie : « R (est vraie) en remplaçant toute occurrence de var par expr » (et dépend donc fortement de la post-condition). Voici un exemple d'application pratique de cet axiome :

{ y + 1 ≥ 5 } y := y + 1 { y ≥ 5 }

Ce qui se réécrit naturellement :

{ y ≥ 4 } y := y + 1 { y ≥ 5 }

Il faut noter qu'on aurait pu, à la place du membre de droite de l'affectation (« y + 1 »), choisir une expression faisant entrer en jeu d'autres variables que y, voire uniquement des constantes. Cet axiome, bien qu'il paraisse évident hors de tout contexte, va nous permettre de prouver des programmes plus complexes faisant entrer en jeu des affectations.

Les règles de conséquence de la logique de Hoare permettent d'établir des liens entre les théorèmes. Elles s'énoncent comme ci-dessous. (Pour des raisons de lisibilité, j'ai souligné les triplets de Hoare dans cette partie, afin de les distinguer des autres formules et opérateurs de logique.)

Si { P } Q { R } et (RS) alors { P } Q { S }
Si { P } Q { R } et (SP) alors { S } Q { R }

La règle de composition permet de composer (au sens de concaténer) les programmes :

Si { P } Q1 { R } et { R } Q2 { S } alors { P } (Q1 ; Q2) { S }

Les deux règles suivantes (appelées règles de condition et d'itération) permettent de faire entrer en jeu les structures de contrôle conditionnelles Si et Tant_Que :

Si { PC } S1 { Q } et { P ∧ ¬C } S2 { Q } alors { P } Si (C) Alors_Faire S1 Sinon_Faire S2 { Q }
Si { PC } S { P } alors { P } Tant_Que (C) Faire S { P ∧ ¬C }

Deux points méritent d'être soulignés concernant la règle du Tant_Que. Tout d'abord, on constate que l'utilisation d'une telle boucle permet l'utilisation d'un invariant (ici, la condition P). Le choix de cet invariant est crucial pour certaines preuves, car il permet à une propriété de se transmettre à chaque itération de la boucle. De plus, il est nécessaire de rappeler que la logique de Hoare ne présume pas, dans sa forme partielle, de la finitude du programme concerné. Ainsi, cette dernière règle indique que sous la condition que le programme se termine, sa post-condition vérifiera la condition « P ∧ ¬C ».

Exemple d'application

Pour illustrer mon propos, je vous propose un exemple de programme itératif calculant la factorielle. Ce programme prend comme entrée une variable entière t, et a pour sortie la variable entière r qui vaut alors t!. Ce programme relativement simple se compose d'une boucle Tant_Que précédée de l'initialisation des variables utilisées (la variable de sortie r, ainsi qu'un compteur n). La seule pré-condition de ce triplet de Hoare est que la variable d'entrée t soit un entier positif, et sa post-condition est que sa variable de sortie r soit égale à la factorielle de t.

{ t ≥ 0 }

1  n := t;
2 r := 1;
3 Tant_Que n ≠ 0
4 r := r * n;
5 n := n - 1;
6 Fin_Tant_Que

{ r = t! }

Afin de démontrer le triplet de Hoare ci-dessus, nous allons procéder par étapes successives, et montrer des propriétés sur chacun des lignes en utilisant les règles et l'axiome d'affectation. Puis nous finirons par relier ces propriétés entre elles à l'aide des règles de conséquence et de composition pour démontrer la propriété globale du programme.
Commençons par la première ligne. d'après l'axiome d'affectation, son exécution vérifie :
{ t ≥ 0 ∧ t = t } n := t; { n ≥ 0 ∧ t = n }
Soit, après simplification de la pré-condition (son dernier membre n'apportant aucune information) :
{ t ≥ 0 } n := t; { n ≥ 0 ∧ t = n }
De même, toujours d'après l'axiome d'affectation, l'exécution de la ligne 2 vérifie le triplet de Hoare suivant (après simplification de la pré-condition) :
{ n ≥ 0 ∧ t = n } r := 1; { n ≥ 0 ∧ t = nr = 1 }
Ici, nous avons fait en sorte que la post-condition du premier triplet soit identique à la pré-condition du second triplet. Nous pouvons alors directement composer les deux programmes pour obtenir un unique triplet de Hoare :
{ t ≥ 0 } n := t; r := 1; { n ≥ 0 ∧ t = nr = 1 }
Intéressons-nous maintenant aux lignes 3 à 6 : elles forment une boucle répétitive. (La ligne 6 n'est pas une véritable instruction, elle ne sert qu'à terminer la structure de contrôle Tant_Que.) Prenons en compte séparément les deux lignes au sein de cette boucle. La ligne 4 vérifie :
{ r = t! / n! ∧ tnn ≥ 0 ∧ n ≠ 0 } r := r * n; { r = t! / (n - 1)! ∧ tnn ≥ 0 ∧ n ≠ 0 }
Tandis que l'instruction de la ligne 5 vérifie :
{ r = t! / (n - 1)! ∧ tnn ≥ 0 ∧ n ≠ 0 } n := n - 1; { r = t! / n! ∧ tnn ≥ 0 }
On peut alors réunir les deux lignes contenues dans la boucle pour obtenir :
{ r = t! / n! ∧ tnn ≥ 0 ∧ n ≠ 0 } r := r * n; n := n - 1; { r = t! / n! ∧ tnn ≥ 0 }
Toutes les instructions contenues dans la boucle se trouvent dans ce triplet de Hoare, et il est possible d'extraire un invariant des deux conditions du triplet, qui est : « r = t! / n! ∧ tnn ≥ 0 ». En revanche, la formule « n ≠ 0 » ne se trouve que dans la pré-condition, et on va s'en servir comme condition pour la terminaison de la boucle (ce qui explique pourquoi j'avais décidé de ne pas la simplifier avec la formule « n ≥ 0 »). On peut donc appliquer la règle relative à l'itération :
{ r = t! / n! ∧ tnn ≥ 0 } Tant_Que (n ≠ 0) r := r * n; n := n - 1; Fin_Tant_Que { r = t! / n! ∧ tnn ≥ 0 ∧ n = 0 }
Ici, la post-condition se simplifie naturellement en : « r = t! », ce qui est bien la post-condition finale que l'on cherche à obtenir.
Pour finir, il ne nous reste plus qu'à constater (naïvement) que :
n ≥ 0 ∧ t = nr = 1 ⇒ r = t! / n! ∧ tnn ≥ 0
D'après les règles de conséquence et de composition, on peut alors « brancher », par implication puis concaténation, le triplet caractérisant les lignes 1 et 2 à celui caractérisant la boucle (lignes 3 à 6)... CQFD !

Un autre exemple intéressant, que je ne détaillerai pas ici, mais que Hoare propose dans son article originel, est celui du calcul de la division euclidienne. Ce programme propose un cas intéressant de pré-condition toujours vraie, ce qui signifie que sa post-condition sera toujours vérifiée (sous réserve de terminaison) :

{ vrai }

1  r := x;
2 q := 0;
3 Tant_Que y ≤ r
4 r := r - y;
5 q := q + 1;
6 Fin_Tant_Que

{ y > rx = r + q.y }

Références

C. A. R. Hoare : « An Axiomatic Basis for Computer Programming », Communications of the ACM, octobre 1969
L'exemple de cet article est très largement inspiré du cours d'Anders Møller : « Program Verification with Hoare Logic », Technical report, University of Aarhus (2004)
Je peux aussi vous proposer l'article Wikipédia sur la logique de Hoare qui en rappelle les principaux éléments (l'article anglais est cependant conseillé, car plus complet et plus juste à ce jour).

Comments

Morgan Magnin
Jan 18, 2011

C'est une présentation très claire de la logique de Hoare, notamment grâce à l'exemple que tu détailles dans ton article. La question qui vient naturellement après cette lecture, c'est "quel est l'intérêt d'un tel formalisme ?" Autrement dit, quels en sont les avantages ? Est-ce que cela peut être utile en pratique à tout informaticien qui fait de la programmation, de sorte à vérifier ses programmes ? Quelles sont, a contrario, les limites de la logique ?
Des questions que, j'imagine, tu vas traiter dans la suite de tes travaux.

info3
Jan 28, 2011

Cette logique offre un formalisme simple et puissant pour la vérification de programme, comme le montre l'exemple de la factorielle (bien que cet exemple ne soit pas très complexe). De plus, il est possible d'effectuer des preuves de façon très modulaire. Par exemple, après avoir prouvé que l'algorithme de la factorielle était correct, je serai en mesure de m'en re-servir pour effectuer la preuve d'autres programmes plus complexes (en le faisant intervenir sous la forme d'une fonction par exemple).
Cependant, l'intérêt pratique pour tout informaticien est assez limité, notamment du fait que les preuves sont parfois assez fastidieuses. Ici, j'ai passé sous silence certaines règles d'arithmétique informatique, et je n'ai pas pris en compte toutes les limitations d'un ordinateur, notamment les problèmes de dépassements d'entiers qui peuvent intervenir lors de l'exécution et mener à un blocage ou un résultat erroné, selon l'architecture modélisée.
En définitive, cette logique est surtout utilisée dans la recherche, d'autant plus qu'elle offre des outils puissants mais parfois assez abstraits pour les ingénieurs-informaticiens, et que je présenterai dans mon prochain article.