d ' une propriété qui reste vra ie à chaque
tour de boucle du programme. On appelle
ce la un invariant de boucle. Plus préc isément , on indique que la propriété
r x pe = x" doi t être vérifiée chaque fo is
q ue le progra mm e a tte int la li g ne 5
(que l que so it le rés ultat du teste> 0).
L' in variant de bouc le est un peu l'analog ue de l' hypothèse de récurre nce en
mathématiques .
L'outil Why3 ne prend pas cet in variant
de bo uc le po ur a rge nt co mptant. Au
contraire , il va ex iger de no us de montrer qu ' il s'agit bien là d ' une pro priété
vra ie à chaque tour de bouc le, en supplé ment de la propriété fin ale que no us
cherchons à montrer. Plus préc isément,
l'outil Why3 va nous demander de prouve r les trois pro priétés s ui vantes :
• que l' in vari ant de boucle est vrai ini -
tialement , c'est-à-dire quand on atteint
la li gne 5 du programme pour la prem iè re fo is. Cec i revie nt à mo ntrer
J X X
1
= X
1
, Ce qui est immédi at.
• que l' invariant de boucle est maintenu
par une exécution du corps de la boucle.
Cela revient à supposer e > 0 (le test
de la boucle est positif puisque le corps
est exécuté) et l' invariant r X pe = x'' et
à montrer que l'invariant est toujours vrai
après l'exécution des trois instructions
lignes 6, 7 et 8 . Il y a là deux cas de
fig ure, selon que le test e mod 2 = 1
est ou non positi f. Si oui ,c'est-à-dire si
e est impair, il fa ut montrer :
r X p X (p X p ) (e- J)/ 2 = X
1 (car e div 2
désigne ici la partie entière de la di vision de e par 2).
Sinon, c ' est-à-dire si e est pair, il fa ut
montrer r x (p x p )'
12
= x'. Dans les deux
cas, un petit pe u d 'algèbre suffit.
• enfi n, que la post-cond itio n est sati sfai te quand on atteint l' instruction renvoyer à la fin du programme, c'est-à-dire
que r = x". Vu que e = 0 à la sortie de
la bouc le, l' in vari ant r x p• = x" se
simplifie en la propriété voulue.
POUR LES MATHS
le programme expo calculant x"
fonction expo(x, n) =
r +-1
p +-X
e +-n
tant que e > 0 faire
si (e mod 2) = 1 alors r +- r x p
p+-p x p
e +-e div 2
renvoyer r
L'outil Why3 produit ces divers énoncés dans le form at d 'entrée des o uti ls
Coq et Alt-Ergo, qui peuvent alors être
uti lisés pour obteni r une preuve compl ète me nt mécani sée de la correcti on
du programme expo . Une fracti on de
seconde suffit po ur rejo ue r un e te l le
preuve .
li convient enfin de montrer que notre
programme s'exécute en un temps fin i.
Pour cela , on majore le nombre de tours
de la boucle tant que , par exemp le par
l' entier e. L' outil Why3 ex ige alors de
nous de montrer que la quantité e reste
to uj o urs pos iti ve o u nu lle e t qu 'e ll e
décroît stri cte me nt à c haque to ur de
boucle, ce qui ne pose aucune di ffic ulté.
C'est bie n entendu un majorant grossier du nombre de tours de bouc le de ce
programme, mais cela suffit à en garantir la terminaison .
J.-C. F.
Références
On trouvera plu s de déta il s sur les out ils Coq, Alt-Ergo et Why3
sur les sites suivants :
• http://coq.inri a.fr
• http://alt-ergo. lri .fr
• http://why3 .l ri .fr
Hors-série n ° 52. Mathématiques & informatique Tangente
7
tour de boucle du programme. On appelle
ce la un invariant de boucle. Plus préc isément , on indique que la propriété
r x pe = x" doi t être vérifiée chaque fo is
q ue le progra mm e a tte int la li g ne 5
(que l que so it le rés ultat du teste> 0).
L' in variant de bouc le est un peu l'analog ue de l' hypothèse de récurre nce en
mathématiques .
L'outil Why3 ne prend pas cet in variant
de bo uc le po ur a rge nt co mptant. Au
contraire , il va ex iger de no us de montrer qu ' il s'agit bien là d ' une pro priété
vra ie à chaque tour de bouc le, en supplé ment de la propriété fin ale que no us
cherchons à montrer. Plus préc isément,
l'outil Why3 va nous demander de prouve r les trois pro priétés s ui vantes :
• que l' in vari ant de boucle est vrai ini -
tialement , c'est-à-dire quand on atteint
la li gne 5 du programme pour la prem iè re fo is. Cec i revie nt à mo ntrer
J X X
1
= X
1
, Ce qui est immédi at.
• que l' invariant de boucle est maintenu
par une exécution du corps de la boucle.
Cela revient à supposer e > 0 (le test
de la boucle est positif puisque le corps
est exécuté) et l' invariant r X pe = x'' et
à montrer que l'invariant est toujours vrai
après l'exécution des trois instructions
lignes 6, 7 et 8 . Il y a là deux cas de
fig ure, selon que le test e mod 2 = 1
est ou non positi f. Si oui ,c'est-à-dire si
e est impair, il fa ut montrer :
r X p X (p X p ) (e- J)/ 2 = X
1 (car e div 2
désigne ici la partie entière de la di vision de e par 2).
Sinon, c ' est-à-dire si e est pair, il fa ut
montrer r x (p x p )'
12
= x'. Dans les deux
cas, un petit pe u d 'algèbre suffit.
• enfi n, que la post-cond itio n est sati sfai te quand on atteint l' instruction renvoyer à la fin du programme, c'est-à-dire
que r = x". Vu que e = 0 à la sortie de
la bouc le, l' in vari ant r x p• = x" se
simplifie en la propriété voulue.
POUR LES MATHS
le programme expo calculant x"
fonction expo(x, n) =
r +-1
p +-X
e +-n
tant que e > 0 faire
si (e mod 2) = 1 alors r +- r x p
p+-p x p
e +-e div 2
renvoyer r
L'outil Why3 produit ces divers énoncés dans le form at d 'entrée des o uti ls
Coq et Alt-Ergo, qui peuvent alors être
uti lisés pour obteni r une preuve compl ète me nt mécani sée de la correcti on
du programme expo . Une fracti on de
seconde suffit po ur rejo ue r un e te l le
preuve .
li convient enfin de montrer que notre
programme s'exécute en un temps fin i.
Pour cela , on majore le nombre de tours
de la boucle tant que , par exemp le par
l' entier e. L' outil Why3 ex ige alors de
nous de montrer que la quantité e reste
to uj o urs pos iti ve o u nu lle e t qu 'e ll e
décroît stri cte me nt à c haque to ur de
boucle, ce qui ne pose aucune di ffic ulté.
C'est bie n entendu un majorant grossier du nombre de tours de bouc le de ce
programme, mais cela suffit à en garantir la terminaison .
J.-C. F.
Références
On trouvera plu s de déta il s sur les out ils Coq, Alt-Ergo et Why3
sur les sites suivants :
• http://coq.inri a.fr
• http://alt-ergo. lri .fr
• http://why3 .l ri .fr
Hors-série n ° 52. Mathématiques & informatique Tangente
7