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 :
- on a bien while VARIANT > 0
- 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 :
- on a bien while VARIANT > 0
- 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.