EPITA

Introdution à Prolog, projet 2011

Jean-François Perrot

LOGIQUE DE HOARE, APPLICATION À MIL

Réflexion préliminaire sur les preuves de programmes
MIL et la logique de Hoare
Récapitulation, mise en œuvre

Réflexion préliminaire sur les preuves de programmes
1. Programme = schéma + interprétation
  Dans le texte d'un programme MIL, on sépare facilement
  - les expressions (arithmétiques et booléennes)
    de la
  - structure de contrôle, formée par les points-virgules, les symboles d'affectation ":="
    et autres mots-clefs (boucles, conditionnelles etc.).
  Cette dernière détermine la forme des séquences de calcul du programme,
  mais ne dit rien sur les objets qui seront manipulés : la même structure de contrôle peut
  s'appliquer aussi bien à des entiers qu'à des réels, à des chaînes de caractères ou à des listes.
  Ce sont les expressions qui doivent décrire ces objets.
  
  Pour cela, il faut déclarer le domaine sur lequel on calcule,
  et donner pour chaque opérateur (et pour chaque constante) une signification dans ce domaine :
  le tout s'appelle une interprétation,
  tandis que la structure du programme, abstraction faite du domaine de calcul, est
  traditionnellement nommée le schéma du programme.
  
  En somme, le schéma est donné par le texte du programme seul,
  sans l'information supplémentaire fournie par l'interprétation des expressions.
  
  Exemples :
  1. Tout programme MIL admet au moins deux interprétations :
    - sur les entiers (avec la division entière)
      et
    - sur les réels (avec la division réelle).
    Il est clair que ces deux interprétations sont très différentes !
    Elles sont même incompatibles, en ce sens qu'un schéma qui donne un calcul "raisonnable" avec l'une
    a fort peu de chances de rester raisonnable avec l'autre - sauf si la division n'intervient pas.
  2. Si on décide d'interpréter
    - le chiffre "1" comme le nom du nombre zéro
    - le symbole "*" comme celui de l'addition,
    - en conservant a "-1" (vu comme un opérateur unaire) son sens de "prédécesseur",
    le programme prévu pour calculer n! se met à produire n*(n+1)/2 :
    
    :m := 1 ; TANTQUE n <> 1 FAIRE m := n*m ; n := n -1 FINTQ ...
  3. Le même schéma est applicable au domaine des chaînes de caractères : si
    - "1" designe la chaîne vide,
    - "*" la préfixation du second opérande par l'initiale du premier
      (un peu tire' par les cheveux, certes, mais avez-vous jamais inspecté le jeu d'instructions d'un processeur ?)
    - "-1" l'opération de suppression du premier caractere
    alors il donne la chaine renversée de sa donnée.
  4. Idem si on opère sur le domaine des listes LISP, avec
    - "1" --> nil,
    - "*" --> (lambda (n m) (cons (car n) m).
    - "-1" --> cdr.
    Si vous etes sceptique, faites l'expérience suivante : ouvrez Le_Lisp, et définissez :
     (de foo (n) ; traduction du texte MIL en syntaxe Le_Lisp       (let ((m un))          (while (not (equal n un)) (setq m (* n m)) (setq n (1- n)))          m         ))
  
     faites ensuite " (setq un 1) " et demandez " (foo 5) " pour être bien sûr de ne pas avoir fait de faute de frappe.
     Puis redéfinissez la constante et les opérateurs :
  
     (setq un ())    (de 1- (x) (cdr x))    (de * (x y) (cons (car x) y))
  
     et demandez à présent " (foo '(1 2 3 4 5)) "...
  
     Cette redéfinition opère-t-elle la même métamorphose sur le programme récursif correspondant ?
  
                (de foo (n) (if (equal n un) un (* n (foo (1- n)))))
2. "Conditions de vérification" de la correction d'un programme
  Nous parlons ici de la correction d'un programme MIL avec invariants de boucles, précondition et postcondition,
  au sens faible c'est-a-dire en supposant que le calcul se termine.
  Pour démontrer qu'un programme est correct par la méthode des assertions,
  on est amené à utiliser un certain nombre de propriétes du domaine sur lequel le programme travaille
  (pour MIL, ce sont normalement les entiers).
  
  Souvent, ces propriétes ne sont pas autre chose que les lois du calcul arithmetique,
  comme pour le classique programme de division entière :
  
      -------------------------------------------------------------------------
           { le pere de tous les programmes imperatifs }          r := a ; q := 0 ;          TANTQUE r >= b INVARIANT a = b*q+r & r>=0          FAIRE r := r - b ; q := q + 1          FINTQ.          {precondition} a>=0 & b>0. {postcondition} a = b*q+r & r>=0 & r<b.
      -------------------------------------------------------------------------
  
  qui utilise essentiellement l'égalité "b*q+r = b*(q+1)+(r-b)".
  
  Mais on peut voir apparaître des propriétés moins banales.
  Par exemple, la preuve de la validité du programme "ppcm" :
  
      -------------------------------------------------------------------------
  
                { Le programme PGCD/PPCM de Dijkstra. Les assertions utilisent                 deux "fonctions inconnues" : P (pour PGCD) et M (pour PPCM) }               x := a ; y := b ; u := b ; v := a ;               TANTQUE x<>y INVARIANT P(x,y) = P(a,b) & x*u+y*v = 2*a*b               FAIRE SI x>y ALORS x := x-y ; v := u+v                            SINON y := y-x ; u := u+v                     FINSI               FINTQ.               {avec la precondition } a > 0 & b > 0.               {et la postcondition } (x+y)/2 = P(a,b) & (u+v)/2 = M(a,b).
  
      -------------------------------------------------------------------------
  
  repose en premier lieu sur la propriété arithmétique
  
                  PGCD (a, b) * PPCM (a, b) = a * b.
  
  Les différentes propriétés du domaine de calcul qui doivent être vérifiées
  pour assurer la correction d'un programme s'appellent
  
  les conditions de vérification de ce programme.
  
  Exemples de conditions de vérification, sous la forme "brute" livrée par le calcul des assertions,
  sans aucune simplification :
  - Pour le programme de division entière ci-dessus, le calcul des assertions en fait apparaitre trois :
    1. a >= 0 & b > 0 ==> a = b*0+a & a >= 0 {pour l'entrée dans la boucle}
    2. a = b*q+r & r >= 0 & r >= b ==> a = b*(q+1)+(r-b) & r-b >= 0{invariant}
    3. a = b*q+r & r >= 0 & ~(r >= b) ==> a = b*q+r & r >= 0 & r < b {sortie}
  - Pour le programme "ppcm", le même calcul en trouve quatre :
    1. a > 0 & b > 0 ==> P(a,b) = P(a,b) & a*b+b*a = 2*a*b{entrée}
    2. P(x,y) = P(a,b) & x*u+y*v = 2*a*b & x <> y {invariant, cond. positif}
      ==> x > y ==> P(x-y,y) = P(a,b) & (x-y)*u+y*(u+v) = 2*a*b
    3. P(x,y) = P(a,b) & x*u+y*v = 2*a*b & x <> y {invariant, cond. négatif}
      ==> ~(x > y) ==> P(x,(y-x)) = P(a,b) & x*(u+v)+(y-x)*v = 2*a*b
    4. P(x,y) = P(a,b) & x*u+y*v = 2*a*b & ~(x <> y) {sortie de boucle}
      ==> (x+y)/2 = P(a,b) & (u+v)/2 = M(a,b)
  Comme on voit, il s'agit d'énoncés d'arithmétique élémentaire,
  dont le nombre et la forme sont directement reliés à la structure du programme
  (plus exactement, au schéma du programme, aux invariants de boucle et aux pré- et postconditions),
  mais qui en sont logiquement indépendants :
  ils sont vrais ou non dans l'interprétation considerée, indépendamment du programme qui a conduit a les considerer.
  Leur démonstration (ou leur réfutation) est l'affaire du mathématicien, non celle du programmeur.
3. Extraction automatique des conditions de vérification
  Le caractère stéréotypé du calcul des assertions fait entrevoir la possibilite de de l'effectuer automatiquement
  à partir du texte du programme (considéré comme schéma) et des assertions qui l'agrémentent.
  
  Le résultat de ce calcul sera exactement l'ensemble des conditions de verification annoncées ci-dessus.
  Pour achever la preuve de la correction du programme, il faudra ensuite faire la démonstration de ces conditions
  pour l'interprétation des expressions considérée.
  Cette démonstration est alors un exercice purement mathématique, dans lequel le programme donne' n'intervient plus.
  
  Pour arriver à cette automatisation, nous formaliserons le calcul des assertions sous la forme d'un système déductif,
  appelé Logique de Hoare, du nom de son inventeur C.A.R. Hoare, de l'Université d'Oxford.
  
  Nous verrons apparaître naturellement un algorithme pour la recherche des arbres de preuve dans ce système,
  qui nous fournira ipso facto un procédé pour engendrer les conditions de vérification.
  Ce système déductif, apparu en 1969, a été la première en date des formalisations qui ont ete proposées
  pour saisir la "logique des programmes", comme la "logique dynamique", la "logique temporelle" (aux U.S.A)
  et la "logique algorithmique" (en Pologne).
  
  Dijkstra a proposé une variante de la logique de Hoare permettant de traiter de la correction totale des programmes, c'est-à-dire de démontrer que le programme se termine.
  Cette méthode ne se prête pas à un traitement automatique, c'est pourquoi nous n'en parlerons pas ici.
  D'ailleurs, nous n'exposerons pas toute la logique de Hoare, seulement ce qui est utile pour MIL.
  Le lecteur interesse' par des compléments pourra en trouver dans le livre de Berlioux et Bizard, Algorithmique,
  Dunod 1983.
  
  Le mot "logique" doit etre pris ici en son sens propre de "science du discours" (logos) :
  les préoccupations des anciens Grecs se trouvent ainsi appliquees à cet objet nouveau
  qu'est le programme vu comme discours.
  Il ne s'agit plus de réfuter les argumentations contradictoires des sophistes,
  mais de mettre de l'ordre dans celles des programmeurs.
  Et l'appareil mathématique s'est nettement perfectionné depuis Platon et Aristote, comme nous allons le voir.
MIL et la logique de Hoare
1. Les formules du langage
  Comme toujours lors de l'élaboration d'un système déductif, il faut avant tout savoir
  quels sont les objets du discours, susceptibles de recevoir une "valeur de vérité".
  Ici, la "vérité" est plutôt la "correction faible", et elle s'applique à des triplets
  forme's
  - d'un programme MIL (avec ses invariants de boucle),
  - une précondition
  - et une postcondition.
  Nous noterons de tels triplets ainsi :
  
  Précondition { Programme } Postcondition
  Ces triplets constituent une premiere categorie de formules de notre langage.
  Par exemple, nous chercherons à établir la validite de la formule :
  
  a>=0 & b>0 { r := a ; q := 0 ; TANTQUE r >= b INVARIANT a = b*q+r & r>=0 FAIRE r := r - b ; q := q + 1 FINTQ } a = b*q+r & r>=0 & r<b.
  
  Outre ces triplets, nous aurons besoin de "formules degénérées" qui seront simplement des assertions,
  énoncés de propriétés vraies ou fausses portant sur le domaine de calcul envisagé (en l'occurrence, les entiers).
  Nos conditions de vérification apparaîtront en effet dans l'arbre de preuve comme des formules de ce type,
  attachées aux feuilles de l'arbre de preuve.
2. Règles de déduction, première version
  Les différentes règles de déduction du système permettent de traiter les differentes configurations de programmes.
  La plus simple est sans aucun doute celle du programme vide, qui ne fait rien :
  
  Un triplet de la forme
  
                          Précondition { } Postcondition
  
  est manifestement valide si et seulement si la proposition
  
                          Précondition ==> Postcondition
  
  est vraie dans le domaine de calcul.
  
  On observera que cette proposition est une de nos "formules degénérées",
  ce qui nous permet d'ecrire la règle de déduction correspondante :
  
                           Précondition ==> Postcondition    (Règle 1)            ------------------------------                          Précondition { } Postcondition
  
  L'emploi de cette règle fera apparaître dans l'arbre de preuve une feuille portant une condition de vérification,
  comme annoncé.
  
  D'autre part, si le programme considéré n'est pas vide, il peut se decomposer en deux "sous-programmes"
  (l'un d'eux étant éventuellement vide), soit "P = P1 ; P2".
  Il suffit alors de trouver une assertion intermédiaire, à la fois postcondition pour P1 et précondition pour P2,
  donc telle que les deux triplets
  - "Précondition {P1} Intermédiaire"
  - "Intermédiaire {P2} Postcondition"
  soient simultanément valides, pour assurer que le triplet
  " Precondition {P1 ; P2 } Postcondition"
  est lui-même valide.
  Ce qui se formule par la règle de déduction suivante :
  
  Precond {P1} Interm , Interm {P2} Postcond (Règle 2) ------------------------------------------ Precond {P1 ; P2} Postcond
  
  L'application de cette règle suppose que l'on ait trouvé cette assertion intermédiaire...
  En fait, nous ne l'utiliserons que dans le cas particulier où
  le second sous-programme P2 ne contient qu'une seule instruction (la dernière instruction du programme),
  et nous allons immédiatement en dériver trois règles spécialisées pour les trois types d'instructions de MIL,
  à savoir les affectations, les boucles et les conditionnelles.
3. Traitement des affectations
  Nous considérons comme acquise l'observation suivante, que nous avons faite au cours des preuves par assertions :
  
  la précondition "Pre" la plus faible possible assurant la correction de l'affectation "Var := Exp"
  pour la postcondition "Post"
  s'obtient en substituant l'expression "Exp" à toutes les occurrences de la variable "Var"
  dans l'assertion "Post",
  
  ce que nous notons "Pre = Post[Exp/Var]".
  
  Cette observation est ici elevee au rang d'axiome du système, sous la forme du triplet générique :
  
  Axiome de l'affectation :
  
                      Post[Exp/Var] {Var := Exp} Post
  
  Nous avons maintenant assez de matériel pour un premier essai.
  Soit à prouver que le triplet suivant est valide (exemple de la "transposition arithmétique") :
  
            x=a & y=b { x := x+y ; y := x-y ; x := x-y } x=b & y=a.
  
  Avec P1 = "x := x+y ; y := x-y" et P2 = "x := x-y",
  nous allons appliquer la règle 2.
  L'assertion intermédiaire nous est fournie par l'axiome de l'affectation, qui sur P2 se réalise en prenant
  
                      Var = x, Exp = x-y, Post = (x=b & y=a),
  ce qui donne en substituant l'expression "x-y" a la variable "x" dans l'assertion "Post" le triplet valide
  
                      x-y = b & y=a {x := x-y} x=b & y=a.
  L'arbre de preuve commence donc ainsi :
  
                                                             Axiome                                                |----------------------------|    x=a&y=b {x := x+y ; y := x-y} x-y=b&y=a , x-y=b&y=a {x := x-y} x=b&y=a     ------------------------------------------------------------------------               x=a&y=b { x := x+y ; y := x-y ; x := x-y } x=b&y=a
  
  La prémisse gauche de la règle se traite de la même manière, en appliquant la règle 2
  et en trouvant l'assertion intermédiaire grâce à une nouvelle incarnation de l'axiome de l'affectation :
  
                x-(x-y) = b & x-y = a {y := x-y} x-y = b & y = a
  d'ou un fragment d'arbre de preuve :
                                                          Axiome                                         |------------------------------------|    x=a&y=b {x := x+y} x-(x-y)=b&x-y=a , x-(x-y)=b&x-y=a {y := x-y} x-y=b&y=a     -------------------------------------------------------------------------                    x=a&y=b {x := x+y ; y := x-y} x-y=b&y=a
  Le programme du triplet de gauche est certes réduit à une affectation, mais nous le décomposons en "P1 ; P2"
  avec P1 vide et P2 = "x := x+y", pour appliquer une troisième fois la règle 2, avec une troisième
  apparition de l'axiome de l'affectation :
  
     (x+y)-((x+y)-y) = b & (x+y)-y = a {x := x+y} x-(x-y) = b & x-y = a
  ce qui donne
  
     x=a&y=b {} (x+y)-((x+y)-y)=b&(x+y)-y=a ,         Axiome                      |-------------------------------------------------------|                       (x+y)-((x+y)-y)=b&(x+y)-y=a {x := x+y} x-(x-y)=b&x-y=a     -------------------------------------------------------------------------                       x=a&y=b {x := x+y} x-(x-y)=b&x-y=a
  
  Enfin, nous appliquons la règle 1 à la prémisse gauche :
  
                       x=a&y=b ==> (x+y)-((x+y)-y)=b&(x+y)-y=a                      ---------------------------------------                       x=a&y=b {} (x+y)-((x+y)-y)=b&(x+y)-y=a
  La prémisse unique est cette fois une "formule dégénérée", qui est la seule condition de vérification du programme.
  
  L'arbre de preuve complet s'établit donc comme suit :
  
            Condition de vérification |---------------------------------------|    x=a&y=b ==> (x+y)-((x+y)-y)=b&(x+y)-y=a    ---------------------------------------    x=a&y=b {} (x+y)-((x+y)-y)=b&(x+y)-y=a ,         Axiome                      |-------------------------------------------------------|                       (x+y)-((x+y)-y)=b&(x+y)-y=a {x := x+y} x-(x-y)=b&x-y=a     -------------------------------------------------------------------------                       |                                 Axiome                       |                 |------------------------------------|    x=a&y=b {x := x+y} x-(x-y)=b&x-y=a , x-(x-y)=b&x-y=a {y := x-y} x-y=b&y=a     -------------------------------------------------------------------------                       |                                  Axiome                       |                        |----------------------------|    x=a&y=b {x := x+y ; y := x-y} x-y=b&y=a , x-y=b&y=a {x := x-y} x=b&y=a     ------------------------------------------------------------------------               x=a&y=b { x := x+y ; y := x-y ; x := x-y } x=b&y=a
  
  On constate que la forme de cet arbre est essentiellement celle d'une chaîne de longueur 4
  (3 affectations + le programme vide à la fin),
  et que sa construction a fait appel systématiquement a la règle 2 couplée avec une instance de l'axiome de l'affectation. Manifestement, cette méthode permet de venir à bout d'une séquence d'affectations quelconque.
  Comme de telles séquence sont un ingrédient essentiel de la programmation MIL,
  il est utile de la résumer en une règle de déduction dérivée,
  "spécialiste" des situations où la dernière instruction est une affectation :
                        Precondition { P } Postcondition[Exp/Var]    (Regle 2a)    ------------------------------------------------                      Precondition { P ; Var := Exp } Postcondition
  Grâce à cette formulation plus ramassée, les redondances disparaissent de l'arbre de preuve,
  dont la structure linéaire apparaît clairement :
  
                           Condition de vérification                  |---------------------------------------|                   x=a&y=b ==> (x+y)-((x+y)-y)=b&(x+y)-y=a                   ---------------------------------------         (1)                    x=a&y=b {} (x+y)-((x+y)-y)=b&(x+y)-y=a                    --------------------------------------         (2a)                      x=a&y=b {x := x+y} x-(x-y)=b&x-y=a                   ---------------------------------------         (2a)                   x=a&y=b {x := x+y ; y := x-y} x-y=b&y=a               -------------------------------------------------- (2a)               x=a&y=b { x := x+y ; y := x-y ; x := x-y } x=b&y=a
  
  Comme prévu, il reste à s'assurer que la propriété énoncée par la condition de vérification
  est effectivement vraie pour les entiers...
4. Traitement des boucles
  Considérons un programme dont la dernière instruction est une boucle, accompagnée de son invariant,
  soit le triplet :
  
  Precond { P ; TANTQUE test INVARIANT inv FAIRE corps FINTQ } Postcond
  Sa validité se démontre en trois temps :
  1. L'invariant doit être vérifié à l'entrée dans la boucle ;
    ce qui se traduit par la validite du triplet : "Precond { P } inv"
  2. Sous la condition que le test de la boucle est VRAI, l'invariant doit rester vrai
    apres exécution du corps de la boucle, c'est-à-dire :
    
    inv & test { corps } inv
  3. À la sortie de la boucle, l'invariant et la fausseté du test doivent entrainer
    la vérification de la postcondition, en d'autres termes :
    
    inv & ~test ==> Postcond
    Cette dernière formule est dégénérée, c'est une condition de vérification.
  Le tout se réunit en une règle de déduction spécialiste des boucles :
  
             Precond {P} inv , inv&test {corps} inv , inv&~test ==> Postcond (Regle 2b) ------------------------------------------------------------------          Precond {P ; TANTQUE test INVARIANT inv FAIRE corps FINTQ} Postcond
  
     Exemple : la division entière.
  
           a>=0 & b>0 { r := a ; q := 0 ;                        TANTQUE r >= b INVARIANT a = b*q+r & r>=0                                FAIRE r := r - b ; q := q + 1                        FINTQ } a = b*q+r & r>=0 & r<b.
  
     La regle 2b s'applique, donnant le départ de l'arbre de preuve :
  
                                                         Cond. vérification                                                     |---------------------|        a>=0 & b>0     (a = b*q+r & r>=0) & r>=b    (a = b*q+r & r>=0)    {r := a ; q := 0}    {r := r-b ; q := q+1}        & ~(r>=b) ==>    a = b*q+r & r>=0       a = b*q+r & r>=0       a = b*q+r & r>=0 & r<b     ----------------------------------------------------------------------          a>=0 & b>0 { r := a ; q := 0 ;                        TANTQUE r >= b INVARIANT a = b*q+r & r>=0                                FAIRE r := r - b ; q := q + 1                        FINTQ } a = b*q+r & r>=0 & r<b.
  
  La branche droite donne immédiatement une feuille, portant une condition de vérification,
  les deux autres portent des séquences d'affectations du même modèle que celle que nous venons de traiter.
  
  La première se développe ainsi :
  
                            Condition de vérification                       |-------------------------------|                        a>=0 & b>0 ==> a = b*0+a & a>=0                        -------------------------------         (1)                        a>=0 & b>0 {} a = b*0+a & a>=0                     -------------------------------------      (2a)                     a>=0 & b>0 {r := a } a = b*0+r & r>=0                ---------------------------------------------   (2a)                a>=0 & b>0 {r := a ; q := 0} a = b*q+r & r>=0
  
  Et la deuxième de même :
  
                             Condition de verification            |----------------------------------------------------------|            (a = b*q+r & r>=0) & r>=b ==> a = b*(q+1)+(r-b) & (r-b)>=0             ----------------------------------------------------------    (1)            (a = b*q+r & r>=0) & r>=b {} a = b*(q+1)+(r-b) & (r-b)>=0             ---------------------------------------------------------     (2a)            (a = b*q+r & r>=0) & r>=b {r := r-b} a = b*(q+1)+r & r>=0          ---------------------------------------------------------------- (2a)         (a = b*q+r & r>=0) & r>=b {r := r-b ; q := q+1} a = b*q+r & r>=0
  Nous pouvons à présent contempler l'arbre de preuve tout entier, où apparaissent
  les trois conditions de vérification attendues.
  
                                   Cond. vérification                           |------------------------------|                           | (a = b*q+r & r>=0) & r>=b ==>    Cond. vérification   |   a=b*(q+1)+(r-b) & (r-b)>=0 |-------------------------|------------------------------ a>=0&b>0 ==> a=b*0+a&a>=0|(a = b*q+r & r>=0) & r>=b -------------------------|{} a=b*(q+1)+(r-b) & (r-b)>=0 a>=0&b>0 {} a=b*0+a&a>=0 |----------------------------- ------------------------ |(a = b*q+r & r>=0) & r>=b a>=0 & b>0 {r := a}    |     {r := r-b}    a = b*0+r & r>=0     | a=b*(q+1)+r & r>=0        Cond. vérification    -----------------    ------------------------- |---------------------|        a>=0 & b>0     (a = b*q+r & r>=0) & r>=b    (a = b*q+r & r>=0)    {r := a ; q := 0}    {r := r-b ; q := q+1}        & ~(r>=b) ==>    a = b*q+r & r>=0       a = b*q+r & r>=0       a = b*q+r & r>=0 & r<b     ----------------------------------------------------------------------          a>=0 & b>0 { r := a ; q := 0 ;                        TANTQUE r >= b INVARIANT a = b*q+r & r>=0                                FAIRE r := r - b ; q := q + 1                        FINTQ } a = b*q+r & r>=0 & r<b.
  
  Tout programme comportant seulement des affectations et une seule boucle donnera naissance
  à un arbre de preuve ayant cette forme, et portant donc trois conditions de vérification sur ses feuilles.
  
  Exercice : Determiner de cette maniere les conditions de vérification des triplets suivants :
  1. Calcul simple de 2^n (2 puissance n) :
    
    n >= 0 { x := n ; y := p ; TANTQUE x>0 INVARIANT x>=0 & y*2^x = p*2^n FAIRE y := 2*y ; x := x-1 FINTQ } y = p*2^n
  2. La racine carrée comme somme d'entiers impairs :
    
    n >= 0 { x := 0 ; y := 1 ; z := 1 ; TANTQUE y<=n INVARIANT y = (x+1)*(x+1) & z = 2*x+1 & x*x <= n FAIRE x := x+1 ; z := z+2 ; y := y+z FINTQ } x*x <= n & n < (x+1)*(x+1).
5. Traitement de la conditionnelle
  Considérons un programme dont la dernière instruction est une conditionnelle, donc un triplet de la forme :
  
  Precond { P ; SI test ALORS alt_vrai SINON alt_faux FINSI } Postcond
  
  Il sera certainement valide si nous disposons d'une assertion intermédiaire qui rende valide les trois triplets :
  1. Precond { P } Interm,
  2. Interm & test { alt_vrai } Postcond
  3. Interm & ~test { alt_faux } Postcond
  ce qui se résume en une règle de déduction
  
  Precond {P} Interm , Interm&test {alt_vrai} Postcond , Interm&~test { alt_faux } Postcond ------------------------------------------------------------------------- Precond { P ; SI test ALORS alt_vrai SINON alt_faux FINSI } Postcond
  Malheureusement, ce raisonnement simple ne nous dit pas comment trouver cette assertion intermediaire !
  Nous allons voir comment nous en passer.
  
  Observons d'abord que les alternants "vrai" et "faux" de la conditionnelle ont en général des structures bien différentes, et qu'on voit mal comment leur analyse pourrait conduire à une précondition intermédiaire commune.
  Nous séparons donc les deux branches, en faisant apparaître deux assertions intermédiaires,
  Inter_vrai et Inter_faux où le test intervient explicitement.
  
  Le triplet donné est certainement valide si les quatre triplets suivants le sont :
  1. Precond { P } (test ==> Inter_vrai)
  2. Precond { P } (~test ==> Inter_faux)
  3. Inter_vrai { alt_vrai } Postcond
  4. Inter_faux { alt_faux } Postcond
  Reste à synthétiser les assertions "Inter_vrai" et "Inter_faux".
  
  L'idée est de considérer qu'on peut les trouver en "faisant remonter" la postcondition a travers chacun des alternants.
  La chose est claire si les alternants ne comportent que des affectations.
  En présence d'une boucle, ce qui "remonte" est l'assertion assurant que l'invariant est bien vérifié à l'entrée dans la boucle. Pour une conditionnelle ... attendons un peu.
  
  Pratiquement, on va placer au début de chaque alternant une sorte de marque indiquant l'hypothèse faite , "test" ou "~test", et on lancera les deux calculs.
  Lorsque chacun d'eux arrivera à la marque, avec l'assertion synthétisée "Inter_vrai" ou "Inter_faux",
  on saura que le triplet correspondant   "Inter_vrai { alt_vrai } Postcond"
  (resp. "Inter_faux { alt_faux } Postcond") est valide,
  et on relancera le calcul pour P avec la postcondition "test ==> Inter_vrai { alt_vrai } Postcond"
  (resp. "~test ==> Inter_faux { alt_faux } Postcond").
  
  Comment placer   cette "marque" ? Nous aurons recours a une "pseudo-instruction"
  chargée exclusivement de porter l'assertion "test" ou "~test".
  Nous choisissons comme symbole de cette pseudo-instruction "?=" et comme syntaxe
  
                                ?= <assertion>
  
  (que l'on peut traduire par "affirmer <assertion>").
  
  Naturellement, il faut préciser le statut de cette pseudo-instruction dans le systeme déductif
  que nous sommes en train d'achever : il sera réglé en observant que le triplet
  
                  Precondition { ?= Assertion } Postcondition
  
  est valide si et seulement si
  
                  Precondition ==> (Assertion ==> Postcondition)
  La precondition la plus faible est donc l'implication (Assertion ==> Postcondition) elle-même,
  ce qui s'exprime par un schéma d'axiome de notre système :
  
     Axiome de l'assertion :
  
            (Assertion ==> Postcondition) { ?= Assertion } Postcondition
  Ceci nous garantit que la pseudo-instruction "?=" fonctionnera comme prévu
  et nous permet de formaliser notre démarche par la règle de déduction suivante :
  
     (Regle 2c)    Precond {P ; ?= test ; alt_vrai} Postcond ,                                    Precond {P ; ?= ~test ; alt_faux} Postcond     -------------------------------------------------------------------------       Precond { P ; SI test ALORS alt_vrai SINON alt_faux FINSI } Postcond
  
  Sa genèse un peu compliquée s'éclaircira lors de sa mise en œuvre.
  
  Exemple le plus simple possible :
  
     Vrai {x:=a ; y:=b ; SI y>x ALORS z:=x ; x:=y ; y:=z SINON FINSI} y<=x.
  
  L'application de la règle 2c lance l'arbre de preuve :
  
     Vrai {x:=a;y:=b; ?= y>x ; z:=x;x:=y;y:=z} y<=x,                                            Vrai {x:=a;y:=b; ?= ~(y>x)} y<=x     -----------------------------------------------------------------------     Vrai {x:=a ; y:=b ; SI y>x ALORS z:=x ; x:=y ; y:=z SINON FINSI} y<=x
  
  La prémisse droite se traite par la règle 2, avec une instance de l'axiome de l'assertion qui donne le triplet valide :
  
                      (~(y>x) ==> y<=x) {?= ~(y>x)} y<=x
  La suite est une séquence d'affectations que nous savons traiter, d'où l'arbre de preuve :
  
              Cond. vérification       |--------------------------|        Vrai ==> (~(b>a) ==> b<=a)        --------------------------        Vrai {} (~(b>a) ==> b<=a)      -----------------------------      Vrai {x:=a} (~(b>x) ==> b<=x)                      Axiome    ----------------------------------   |----------------------------------|    Vrai {x:=a;y:=b} (~(y>x) ==> y<=x) , (~(y>x) ==> y<=x) {?= ~(y>x)} y<=x     ------------------------------------------------------------------------                     Vrai {x:=a;y:=b; ?= ~(y>x)} y<=x
  Quant à la prémisse gauche, on a d'abord affaire a une séquence d'affectations
  avant d'appliquer la règle 2 et l'axiome de l'assertion comme ci-dessus :
  
              Cond. verification        |-----------------------|         Vrai ==> (b>a ==> a<=b)         -----------------------         Vrai {} (b>a ==> a<=b)       --------------------------       Vrai {x:=a} (b>x ==> x<=b)                      Axiome     -------------------------------       |----------------------------|    Vrai {x:=a;y:=b} (y>x ==> x<=y)   ,   (y>x ==> x<=y) {?= y>x} x<=y     ------------------------------------------------------------------------                        Vrai {x:=a;y:=b; ?= y>x} x<=y                    ------------------------------------                    Vrai {x:=a;y:=b; ?= y>x ; z:=x} z<=y                  -----------------------------------------                  Vrai {x:=a;y:=b; ?= y>x ; z:=x;x:=y} z<=x               ----------------------------------------------               Vrai {x:=a;y:=b; ?= y>x ; z:=x;x:=y;y:=z} y<=x
  On voit donc apparaître deux conditions de vérification, correspondant aux deux branches de la conditionnelle.
  
  Notons aussi que les arbres de preuve des deux branches sont ici essentiellement des chaînes.
  Pour le faire apparaitre plus clairement, nous proclamons une nouvelle règle dérivée, sur le modèle de la règle 2a,
  specialisée dans les configurations où la dernière instruction est une pseudo-instruction "?="
  et incorporant l'instance correspondante de l'axiome de l'assertion :
  
                      Precondition { P } Assertion ==> Postcondition    (Regle 2d)      -----------------------------------------------                     Precondition { P ; ?= Assertion } Postcondition
  
  Grâce a cette simplification, nous voyons nettement apparaitre la structure binaire de l'arbre de preuve :
                 Cond. verification            |-----------------------|            Vrai ==> (b>a ==> a<=b)             -----------------------              Vrai {} (b>a ==> a<=b)            --------------------------           Vrai {x:=a} (b>x ==> x<=b)                Cond. verification          -------------------------------        |--------------------------|         Vrai {x:=a;y:=b} (y>x ==> x<=y)         Vrai ==> (~(b>a) ==> b<=a)         ---------------------------------        --------------------------         Vrai {x:=a;y:=b; ?= y>x} x<=y            Vrai {} (~(b>a) ==> b<=a)       ------------------------------------      -----------------------------      Vrai {x:=a;y:=b; ?= y>x ; z:=x} z<=y     Vrai {x:=a} (~(b>x) ==> b<=x)    ----------------------------------------   -------------------------------    Vrai{x:=a;y:=b; ?= y>x ; z:=x;x:=y}z<=x     Vrai{x:=a;y:=b}(~(y>x)==>y<=x)    --------------------------------------------- ----------------------------    Vrai {x:=a;y:=b; ?= y>x ; z:=x;x:=y;y:=z} y<=x,            |                                            Vrai {x:=a;y:=b; ?= ~(y>x)} y<=x     -----------------------------------------------------------------------     Vrai {x:=a ; y:=b ; SI y>x ALORS z:=x ; x:=y ; y:=z SINON FINSI} y<=x
Récapitulation, mise en œuvre
1. Les règles "effectives"
  Finalement, nous sommes arrivés à éliminer complètement du calcul pratique la règle 2 et les axiomes (affectation et assertion) .
  Pour mémoire, voici réunies les 5 règles que nous utiliserons :
  
  Precondition ==> Postcondition (Règle 1) ------------------------------ Precondition { } Postcondition Precondition { P } Postcondition[Exp/Var] (Règle 2a) ------------------------------------------------ Precondition { P ; Var := Exp } Postcondition Precond {P} inv , inv&test {corps} inv , inv&~test ==> Postcond (Règle 2b) ------------------------------------------------------------------ Precond {P ; TANTQUE test INVARIANT inv FAIRE corps FINTQ} Postcond (Règle 2c) Precond {P ; ?= test ; alt_vrai} Postcond , Precond {P ; ?= ~test ; alt_faux} Postcond ------------------------------------------------------------------------- Precond { P ; SI test ALORS alt_vrai SINON alt_faux FINSI } Postcond Precondition { P } Assertion ==> Postcondition (Règle 2d) ----------------------------------------------- Precondition { P ; ?= Assertion } Postcondition
2. Mode d'emploi du système
  Naturellement, il n'est pas question de dessiner complètemet l'arbre de preuve d'un programme un tant soit peu compliqué !
  Ce qui nous intéresse, ce sont seulement ses feuilles.
  Il suffit donc de décrire cet arbre, dans un ordre quelconque, et d'énumérer les conditions de vérification au fur et à mesure qu'on les trouve.
  
  Le système impose de "remonter" le programme en partant de la dernière instruction.
  - Les séquences d'affectations ne laissent aucun choix.
  - Les boucles et les conditionnelles donnent lieu à des "appels récursifs" de
  la procédure de démonstration, qui peuvent être exécutés dans un ordre quelconque.
  
  Le programme opère strictement de droite à gauche.
  Il empile les conditions qu'il trouve de manière à les restituer dans l'ordre inverse de celui de leur génération.
  Le problème est ensuite de démontrer que ces conditions sont effectivement vérifiées !
3. Un exemple complet : le "ppcm"
  a>0 & b>0 { x := a ; y := b ; u := b ; v := a ;             TANTQUE x<>y INVARIANT P(x,y) = P(a,b) & x*u+y*v = 2*a*b             FAIRE SI x>y ALORS x := x-y ; v := u+v                          SINON y := y-x ; u := u+v                   FINSI             FINTQ } (x+y)/2 = P(a,b) & (u+v)/2 = M(a,b).
  Le texte MIL se terminant par une boucle, on applique d'abord la règle2b,
  qui d'une part donne une condition de vérification pour la sortie de boucle :
  
  (1) (P(x,y)=P(a,b) & x*u+y*v=2*a*b) & ~(x<>y) ==> (x+y)/2=P(a,b) & (u+v)/2=M(a,b)
  et d'autre part demande la validation des deux triplets :
  
  a>0 & b>0 {x:=a ; y:=b ; u:=b ; v:=a} (P(x,y)=P(a,b) & x*u+y*v=2*a*b) (P(x,y)=P(a,b) & x*u+y*v=2*a*b) & x<>y {SI x>y ALORS x:=x-y ; v:=u+v SINON y:=y-x ; u:=u+v FINSI} (P(x,y)=P(a,b) & x*u+y*v=2*a*b)
  Le premier comporte une séquence d'affectations sans histoire qui aboutit à la condition de vérification pour l'entrée dans la boucle :
  
  (2) a>0 & b>0 ==> P(a,b) = P(a,b) & a*b + b*a = 2*a*b
  
  Le second demande l'application de la règle 2c et se divise en deux branches.
  En appelant I l'invariant de boucle, il vient :
  
  I & x<>y { ?= x>y ; x:=x-y ; v:=u+v } I I & x<>y { ?= ~(x>y) ; y:=y-x ; u:=u+v } I
  Pour chaque branche, la "remontee" des deux affectations conduit au triplet :
  
  I & x<>y {?= x>y} P(x-y, y) = P(a,b) & (x-y)*u+y*(u+v) = 2*a*bpour l'une, et à
  
  I & x<>y {?= ~(x>y)} P(x, y-x) = P(a,b) & x*(u+v)+(y-x)*v = 2*a*b
  pour l'autre. L'application de la règle 2d à chacun donne alors
  
  I & x<>y {} x>y ==> P(x-y, y) = P(a,b) & (x-y)*u+y*(u+v) = 2*a*b I & x<>y {} ~(x>y) ==> P(x, y-x) = P(a,b) & x*(u+v)+(y-x)*v = 2*a*b
  Et la règle 1 nous livre les deux conditions de vérification attendues :
  
  (3) I & x<>y ==> (x>y ==> P(x-y, y) = P(a,b) & (x-y)*u+y*(u+v) = 2*a*b)
  
  (4) I & x<>y ==> (~(x>y) ==> P(x, y-x) = P(a,b) & x*(u+v)+(y-x)*v = 2*a*b)
  
  Exercice :
  Combien de conditions de vérifications seront-elles engendrées pour le triplet de la division dichotomique ?
  (Les assertions font appel à un "prédicat inconnu" Q(x,y) signifiant
  "y divise x et le quotient x/y est une puissance de 2".)
  
  a>=0 & b>=0 {t := b ;               TANTQUE t<=a INVARIANT 0<=a & Q(t,b)) FAIRE t := 2*t               FINTQ ;               q := 0 ; r := a ; d := t ;               TANTQUE d>b INVARIANT a = d*q+r & r<d & 0<=r & Q(d,b)               FAIRE d := d/2 ;                     SI r>=d ALORS r := r-d ; q := 2*q+1 SINON q := 2*q                     FINSI               FINTQ} a = b*q+r & r>=0 & r<b .
     Essayez de "deviner", puis faites le calcul...

EPITA

Introdution à Prolog, projet 2011

LOGIQUE DE HOARE, APPLICATION À MIL

Les règles "effectives"