Exos Algo

Identification

Infoforall

31 - Exos Preuve Terminaison


La partie 1 redonne un exemple (un peu plus complexe).

La partie 2 et 3 sont les exos.

Exercices liés à cette activité Algo

1 - Exemple de rappel

1 2 3
x = 3 while x < 8000: x = x * 5

Preuve de terminaison : (A et B) Arrêt

avec

  • Proposition A : les boucles s'expriment sous la forme TANT QUE VARIANT > 0
  • Proposition B : le VARIANT est une suite d'ENTIERS strictement décroissante.

1 - AVANT la boucle

(Ligne 1) On voit que x vaut 3 initialement.

2 - PENDANT la boucle

(Ligne 3) On multiplie x par 5 à chaque tour. On notera n le nombre de tours :

x = 3 * 5n

3 - Recherche du VARIANT

On part de la ligne 2 :

while x < 8000

while 3 * 5n < 8000

while 8000 > 3 * 5n

while 8000 - 3 * 5n > 0

Le VARIANT de boucle est donc 8000 - 3 * 5n.

Ce n'est ni une suite arithmétique, ni géométrique, ni arithmético-géométrique.

Par contre, 3*5n est une suite géométrique de raison q=5 donc croissante et la suite -3*5n est donc décroissante.

On a donc bien

  • une boucle de la forme while variant > 0 (A) et
  • ce variant est une suite d'entiers décroissante (B).

4 - Conclusion

Utilisons le théorème de la preuve de terminaison :

(A et B) Arrêt

A et B sont vraies au vu de la partie 3. Nous venons donc de prouver la terminaison de cette boucle.

2 - Exercice A

01° Prouver la terminaison (ou pas) du programme suivant. Respecter la méthode de rédaction ci-dessus.

1 2 3
x = 15 while x < 5000: x = x + 2

...CORRECTION...

Utilisons le théorème de la preuve de terminaison :

A et B Arrêt :

1 - AVANT le premier tour

(Ligne 1) x vaut 15.

2 - PENDANT un tour

(Ligne 8) On augmente x de 2 à chaque tour de boucle. Si n est le nombre de tours de boucle :

x = 15 + 2*n

3 - Recherche du VARIANT

On cherche à ramener la condition de boucle de la ligne 2 à une forme de ce type :

L2
while VARIANT > 0

On part de ceci :

L2
while x < 5000
L2
while 15 + 2*n < 5000
L2
while 5000 > 15 + 2*n
L2
while 5000 - 15 - 2*n > 0
L2
while 4985 - 2*n > 0

Nous obtenons donc bien la forme de boucle voulue (A) et le VARIANT est une suite de raison r = -2, elle est donc décroissante (B).

4 - Conclusion

Utilisons la preuve de terminaison : (A et B) Arrêt :

  1. on a bien while VARIANT > 0
  2. le VARIANT est bien une suite d'entiers strictement décroissante.

Les deux propriétés A et B prouvent la terminaison de cette boucle.

3 - Exercice B

02° Prouver la terminaison (ou pas) du programme suivant. Respecter la méthode de rédaction ci-dessus.

1 2 3
x = 150 while x > 12: x = x - 10

...CORRECTION...

Utilisons le théorème de la preuve de terminaison :

A et B Arrêt :

1 - AVANT le premier tour

(Ligne 1) x vaut 150.

2 - PENDANT un tour

(Ligne 8) On diminue x de 10 à chaque tour de boucle. Si n est le nombre de tours de boucle :

x = 150 - 10*n

3 - Recherche du VARIANT

On cherche à ramener la condition de boucle de la ligne 2 à une forme de ce type :

L2
while VARIANT > 0

On part de ceci :

L2
while x > 12
L2
while 150 - 10*n > 12
L2
while 150 - 10*n - 12 > 0
L2
while 138 - 10*n > 0

Nous obtenons donc bien la forme de boucle voulue (A) et le VARIANT est une suite de raison r = -10, elle est donc décroissante (B).

4 - Conclusion

Utilisons la preuve de terminaison : (A et B) Arrêt :

  1. on a bien while VARIANT > 0
  2. le VARIANT est bien une suite d'entiers strictement décroissante.

Les deux propriétés A et B prouvent la terminaison de cette boucle.

FIN

Activité publiée le 18 01 2021
Dernière modification : 18 01 2021
Auteur : ows. h.