Next Contents

1   Rappels sur la logique de Hoare

1.1   Conditionnelle

La règle pour la conditionnelle en logique de Hoare est :
{f Ù C}P{y}       {f Ù ¬ C}Q{y}
{f}if C then P else Q end{y}
Donner la règle permettant d'établir : {f}if C then P end{y}

Correction :
{f Ù C}P{y}       f Ù ¬ C Þ y
{f}if C then P end{y}

1.2   Affectation

Trouver f tel que {f}a:=a+b{a=b}

Correction : La règle pour l'affectation est {yx:=t}x:=t{y} on trouve donc fº (a=b)a:=a+b soit a+b=b qui est vérifié lorsque a=0

1.3   Échange de valeurs

Soit le programme P suivant d'échange des valeurs des variables x et y :
z:= x; x:= y; y:= z
  1. Écrire une spécification de ce programme exprimant l'échange de valeurs.
  2. Prouver la correction de ce programme.
Correction : La spécification utilise deux variables auxilliaires pour mémoriser les valeurs de x et de y avant l'exécution du programme : {x=x0 Ù y=y0}P{x=y0 Ù y=x0} On a : {x=y0 Ù z=x0}y:=z{x=y0 Ù y=x0}
{y=y0 Ù z=x0}x:=y{x=y0 Ù z=x0}
{y=y0 Ù x=x0}z:=x{y=y0 Ù z=x0}
et on conclut car (x=x0 Ù y=y0) Þ (y=y0 Ù x=x0)

1.4   Boucle

Soit le programme P suivant qui calcule 2n dans la variable x :
x:=0; y:=n; while y>0 do y:=y-1;x:=x+2 end
  1. Écrire la spécification de ce programme.
  2. Écrire l'invariant de boucle.
  3. Prouver la correction du programme en justifiant si la terminaison est partielle ou totale.
Correction : La spécification du programme est {n>0}P{x=2n}. L'invariant de boucle est :y³ 0 Ù x=2(n-y). On a bien {n>0}x:=0; y:=n{y³ 0 Ù x=2(n-y)} et {y³ 0 Ù x=2(n-y) Ù y>0}y:=y-1;x:=x+2{y³ 0 x=2(n-y)} À la sortie de boucle on a : y £ 0 Ù y³ 0 Ù x=2(n-y) ie y=0 Ù x=2(n-y) et donc x=2n. Pour justifier la correction totale, il faut montrer la décroissance d'un variant. Ici, y convient; la précondition n>0 est essentielle à la terminaison et à la correction du calcul.
Next Contents