Exos Algo

Identification

Infoforall

17 - 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

  1. une condition du type  while uN > 0 
  2. avec  uN = 65 - 5*n  une 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

J'espère que ca commence à rentrer.

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