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}
{f Ù C}P{y} f Ù
¬ C Þ y
{f}if C then P end{y}
A.2 Affectation
Trouver f tel que {f}a:=a+b{a=b}
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
A.3 Échange de valeurs
Soit le programme P suivant d'échange des valeurs des variables x et y :
z:= x; x:= y; y:= z
Écrire une spécification de ce programme exprimant l'échange de valeurs.
Prouver la correction de ce programme.
La spécification utilise deux variables auxiliaires 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)
A.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
Écrire la spécification de ce programme.
Écrire l'invariant de boucle.
Prouver la correction du programme en justifiant si la
terminaison est partielle ou totale.
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.
