Application de la logique de Hoare aux réseaux de régulation génétique - Article 4 : Opérateurs de la logique de Hoare

Dans mon précédent article, je vous avais présenté la logique de Hoare sans faire de lien avec mon sujet de Master. Ce lien sera l'objet de mon présent article, où je vais présenter un nouvel outil de la logique de Hoare, et expliquer comment cet outil peut être utile pour l'étude des réseaux de régulation génétique.

Pour mémoire, la logique de Hoare consiste en la construction de triplets de Hoare qui permettent d'associer une pré-condition et une post-condition à un programme. Les triplets prennent la forme qui suit :

{ P } Q { R }

Q est le programme, et P et R sont respectivement la pré-condition et la post-condition. Un tel triplet signifie que si P est vraie avant l'exécution de Q, et si Q se termine, alors R sera vraie après son exécution. En procédant par étapes à partir de morceaux de programmes atomiques (les instructions) et en appliquant les axiomes et règles relatifs à cette logique, on peut démontrer qu'un programme possède le comportement désiré.

Notions de plus faible pré-condition et plus forte post-condition

La principale difficulté de cette logique est la formulation de pré-conditions et post-conditions judicieusement choisis pour chaque étape (i.e. Pour chaque instruction ou groupement d'instructions) afin de prouver que le programme global se comporte comme désiré. Pour donner une approche un peu plus pratique, reprenons l'exemple suivant :

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

Ce triplet relativement intuitif signifie que si, avant l'exécution d'une incrémentation, la valeur d'une variable appelée y est supérieure à 4, alors après son exécution cette valeur sera supérieure à 5. Ce triplet est assez général, mais on pourrait imaginer des conditions différentes, comme dans les exemples suivants :

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

Dans le premier exemple, la pré-condition a été restreinte. Le triplet est toujours correct, mais il traite un ensemble de cas d'exécutions beaucoup plus restreint ! Le second exemple, quant à lui, voit sa post-condition généralisée : l'ensemble des cas d'utilisation est toujours le même, mais la condition finale est moins forte, et pourrait être insuffisante si la suite du programme nécessitait d'être certain que y soit supérieure à 5.

De façon plus générale, il faut éviter de trop restreindre la pré-condition, ou trop étendre la post-condition si on veut conserver le pouvoir d'expression de cette logique. Les cas extrêmes seraient les suivants :

{ faux } Q { R }
{ P } Q { vrai }

Ces deux triplets sont corrects : en effet, la pré-condition du premier n'est jamais satisfaite (donc on ne cherchera jamais à exécuter son programme et à vérifier sa post-condition), tandis que la post-condition du second l'est toujours (et ne présente aucun intérêt pour une démonstration, d'autant plus qu'on ne cherche pas ici à prouver la terminaison du programme).

Ces cas extrêmes nous amènent aux notions de plus faible pré-condition et plus forte post-condition. On les définit comme suit :

  • Pour un programme Q et une post-condition R donnés, la plus faible pré-condition, notée WP(Q, R), est l'assertion la plus large possible pour laquelle Q se termine et R est satisfaite après exécution de Q.
  • Pour un programme Q et une pré-condition P donnés, la plus forte post-condition, notée SP(P, Q), est l'assertion la plus restreinte possible qui soit satisfaite après exécution de Q, si P est vraie avant, et sous réserve de terminaison de Q.

En pratique, l'opérateur de plus faible pré-condition est le plus souvent utilisé, notamment parce que l'axiome d'affectation le rend assez simple à mettre en pratique. C'est aussi celui qui sera utilisé pour faire le lien avec les réseaux de régulation génétique.

Il est à noter que ces opérateurs comportent la notion de terminaison du programme. Cette notion est à mettre en parallèle avec la forme que j'appellerai « forte » de la logique de Hoare. Lorsque cette forme est utilisée, un triplet possède non seulement la signification de la forme « faible », mais suppose aussi la terminaison du programme.

Règles

Les règles de la logique de Hoare permettent de montrer de nombreuses propriétés sur les opérateurs définis ci-dessus. Pour commencer, de façon très générale, si on considère la forme « forte » de la logique de Haore, on a la propriété suivante :

{ P } Q { R } ssi P ⇒ WP(Q, R) ssi SP(P, Q) ⇒ R

Il est ensuite possible de définir le résultat de l'opérateur WP pour certaines structures à l'aide des axiomes et règles que j'avais énoncées dans mon dernier article. En voici deux exemples.

  • Pour l'affectation :
    WP(var := expr, R) ≡ R [var/expr]
    ce qui signifie : « R où toutes les occurrences du nom de variable var sont remplacées par l'expression expr ». On retrouve donc une formulation très proche de la règle d'affectation.
  • Pour la structure conditionnelle :
    WP(Si C Alors_Faire S1 Sinon_Faire S2, R) ≡ C ⇒ WP(S1, R) ∧ ¬C ⇒ WP(S2, R)
    qui dépend des plus faibles pré-conditions des deux chemins possibles selon la condition C.

Une telle formule existe aussi pour la structure répétitive. Je ne l'expose pas ici car elle s'énonce de façon itérative et est donc plus complexe.

Liens avec la bio-informatique

Comme je l'avais exposé dans mes deux premiers articles, le modèle de Thomas étudie les interactions entre gènes. Pour cela, il utilise un modèle simplifié du gène, caractérisé par un niveau d'expression fini et discret. Après avoir formalisé le système de gènes à étudier sous forme de graphe, et défini une paramétrisation (qui permet d'établir les points d'attraction de chaque gène en fonction de ses prédécesseurs dans le graphe), on obtient un graphe d'états qui recense toutes les combinaisons de niveaux d'expression accessibles par les gènes et leurs successeurs possibles.

Dans ce contexte, il devient légitime de se poser des questions du type : « étant donnés un état de mon système de gènes (défini par les niveaux d'expression des gènes qui le composent) et une certaine évolution de ce système, quels sont les états qui me permettront d'y accéder via cette évolution ? ». Pour de petits graphes d'états, on peut se permettre d'effectuer une recherche « à la main ». Malheureusement, la taille du graphe d'états explose lorsque le nombre de gènes augmente, non seulement parce que le nombre de gènes à modéliser augmente, mais aussi parce que les gènes peuvent prendre un nombre plus important de niveaux d'expression. Il devient donc nécessaire d'automatiser ce type de recherche, et de se doter du formalisme adéquat.

Il a alors été proposé d'utiliser la logique de Hoare pour formaliser les problèmes de ce type, et d'utiliser la notion de plus faible pré-condition. Pour rapprocher le modèle de Thomas à la logique de Hoare, il suffit de définir des notions de condition et de programme communes, ce qui a été fait de la manière suivante :

  • Une condition est formée d'un ensemble d'assertions sur les gènes du type : a ~ K où a est le niveau d'expression d'un gène, K est une constante entière, et ~ est un opérateur de comparaison parmi ≤, ≥ et =. Les assertions sont combinées à l'aide des connecteurs logiques ∧ et ∨.
  • Un programme est un chemin constitué d'une succession d'instructions du type : a±, où a est le nom d'un gène et ± est soit l'opération d'incrémentation (notée +) soit l'opération de décrémentation (notée -) du niveau d'expression ce gène. Le chemin en lui-même ne suppose en rien de son état de départ ni d'arrivée.

On est alors en mesure d'exprimer l'action de l'exécution d'un chemin sur le système de gènes à partir d'un ensemble d'états donnés, à l'aide d'un triplet de Hoare. De plus, une question concernant une configuration du système comme celle posée ci-dessus peut être formalisée à l'aide de l'opérateur de plus faible pré-condition, et résolue en utilisant les règles et définition fournies.

Références

C. A. R. Hoare : « An Axiomatic Basis for Computer Programming », Communications of the ACM, octobre 1969
La notion de plus faible pré-condition a notamment été évoquée dans l'article d'E. W. Dijkstra : « Guarded commands, nondeterminacy and formal derivation of programs », Communications of the ACM, août 1975
Des compléments sur cette notion sont disponible au sein du cours d'Anders Møller : « Program Verification with Hoare Logic », Technical report, University of Aarhus (2004)

Dans mon prochain article, je m'intéresserai brièvement à une autre méthode qui permet de formaliser des « questions » du même type sur un graphe d'états : il s'agit des logiques temporelles.

Comments