23 - Exos Preuve Terminaison
Attention, ces exercices vont être assez pénibles à rédiger en markdown. Autant passer par le papier, vous irez plus vite !
La partie 1 donne un exemple.
La partie 2 et 3 sont les exos.
1 - Exemple de rappel
1
2
3 | x = 15
while x < 80:
x = x + 5
|
Etape 1 : avant de rentrer dans la boucle
Ligne 1 : on voit que x vaut 3 initialement.
1 | x = 15
|
Comme nous avons fait 0 tour de boucle TANT QUE, nous noterons ceci :
x0 = 15 |
(1) |
Etape 2 : que se passe-t-il à chaque tour de boucle ?
Ligne 3 : on voit qu'on augmente x de 5 à chaque tour de boucle. La raison vaut donc +5.
3 | x = x + 5
|
On peut donc écrire que x après n+1 tours de boucles vaut x après n tours plus 5.
xN+1 = xN + 5
Nous avons donc affaire à une suite xN arithmétique de raison r = +5 et de valeur initiale x0 = 15 (voir (1)).
xN = x0 + r*n
xN = 15 + 5*n
On obtient donc :
xN = 15 + 5*n |
(2) |
Etape 3 : recherche du VARIANT
On cherche à voir si la condition de boucle de la ligne 2 peut s'écrire sous cette forme :
L2 | while un > 0:
|
On commence la démonstration en récupérant la condition de boucle réelle et on tente de la ramener à la forme attendue pour prouver la terminaison :
L2 | while x < 80:
|
On remplace donc x par xN et on en tente de revenir à la forme attendue.
L2 | while xN < 80:
|
On remplace xN en utilisant (2) :
L2 | while (15 + 5*n) < 80:
|
Pour revenir à la forme attendue, on écrit b > a plutôt que a < b :
L2 | while (15 + 5*n) < 80:
|
L2 | while 80 > (15 + 5*n):
|
Pour revenir à la forme attendue, on doit passer les termes de droite à gauche :
L2 | while 80 > ( + 15 + (5*n) ):
|
L2 | while ( 80 - 15 - (5*n) ) > 0:
|
L2 | while (65 - 5*n) > 0:
|
Nous obtenons alors le VARIANT de boucle uN exprimé de cette façon :
L2 | while uN > 0: avec uN = (65 - 5*n)
|
Etape 4 : conclusion
On voit que le variant est une suite d'entiers dont la raison est r = -5 : on perd 5 à chaque fois. La suite est donc décroissante.
Nous obtenons donc bien
- une condition du type
while uN > 0 - avec
uN = 65 - 5*nune suite d'entiers strictement décroissante.
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
|
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
|
Activité publiée le 18 01 2021
Dernière modification : 18 01 2021
Auteur : ows. h.