Livre_silo 30 août 2013 16:32 Page 101
¨
©
¨
©
¨
©
¨
©
C o p y r i g h t E y r o l l e s
101
4 – Instructions : langage minimal de l’algorithmique
SAVOIR-FAIRE Démontrer qu’une boucle se termine effectivement
On identifie un variant, autrement dit une expression (c’est souvent le simple contenu
d’une variable) :
• qui est un entier positif tout au long de la boucle,
• et qui diminue strictement après chaque itération.
On peut alors en conclure que la boucle se termine.
Exercice 4.20 Démontrer la terminaison du programme écrit à l’exercice 4.19.
4.3.4 Invariant de boucle
Lorsque l’on a écrit un programme, il reste à vérifier qu’il est correct, c’est-à-dire qu’il calcule bien ce qu’ on attend ; on peut tester quelques cas significatifs, mais il est beaucoup
plus satisfaisant de démontrer qu’il est correct dans tous les cas. Une des manières les plus
efficaces de le faire est d’établir un invariant de boucle, c’est-à-dire une propriété qui est
vérifiée tout au long de l’exécution d’une boucle. Cette démarche est à rapprocher du raisonnement par récurrence : en ne s’intéressant qu’aux valeurs initiales des variables et à leur
évolution au cours d’une seule itération, on peut en déduire des propriétés valides quel que
soit le nombre d’itérations.
SAVOIR-FAIRE Démontrer qu’une boucle produit l’effet attendu au moyen
d’un invariant
On utilise une invariant de boucle, c’est-à-dire une propriété qui :
• est vérifiée avant d’entrer dans la boucle,
• si elle est vérifiée avant une itération, est vérifiée après celle-ci,
• lorsqu’ elle est vérifiée en sortie de boucle permet d’en déduire que le programme
est correct.
Exercice 4.21 Démontrer que le programme de calcul de 2 n est correct, c’est-à-dire que lorsque l’exécution se termine, la variable p contient bien la valeur 2 n où n ⩾ 0 est la valeur initiale de la variable c.
Pour raisonner, on note c i et p i les valeurs des variables c et p après l’exécution de la i-ème itération.
L’état au moment de l’entrée dans la boucle est
c 0 = n
p 0 = 1
De plus, le corps de la boucle assure les relations suivantes pour toute itération i :
c i+1 = c i − 1
p i+1 = 2p i
On remarque alors que la propriété suivante est toujours vérifiée : pour toute itération i, on a p i = 2 n−c i
et c i ⩾ 0.
¨
©
¨
©
¨
©
¨
©
C o p y r i g h t E y r o l l e s
101
4 – Instructions : langage minimal de l’algorithmique
SAVOIR-FAIRE Démontrer qu’une boucle se termine effectivement
On identifie un variant, autrement dit une expression (c’est souvent le simple contenu
d’une variable) :
• qui est un entier positif tout au long de la boucle,
• et qui diminue strictement après chaque itération.
On peut alors en conclure que la boucle se termine.
Exercice 4.20 Démontrer la terminaison du programme écrit à l’exercice 4.19.
4.3.4 Invariant de boucle
Lorsque l’on a écrit un programme, il reste à vérifier qu’il est correct, c’est-à-dire qu’il calcule bien ce qu’ on attend ; on peut tester quelques cas significatifs, mais il est beaucoup
plus satisfaisant de démontrer qu’il est correct dans tous les cas. Une des manières les plus
efficaces de le faire est d’établir un invariant de boucle, c’est-à-dire une propriété qui est
vérifiée tout au long de l’exécution d’une boucle. Cette démarche est à rapprocher du raisonnement par récurrence : en ne s’intéressant qu’aux valeurs initiales des variables et à leur
évolution au cours d’une seule itération, on peut en déduire des propriétés valides quel que
soit le nombre d’itérations.
SAVOIR-FAIRE Démontrer qu’une boucle produit l’effet attendu au moyen
d’un invariant
On utilise une invariant de boucle, c’est-à-dire une propriété qui :
• est vérifiée avant d’entrer dans la boucle,
• si elle est vérifiée avant une itération, est vérifiée après celle-ci,
• lorsqu’ elle est vérifiée en sortie de boucle permet d’en déduire que le programme
est correct.
Exercice 4.21 Démontrer que le programme de calcul de 2 n est correct, c’est-à-dire que lorsque l’exécution se termine, la variable p contient bien la valeur 2 n où n ⩾ 0 est la valeur initiale de la variable c.
Pour raisonner, on note c i et p i les valeurs des variables c et p après l’exécution de la i-ème itération.
L’état au moment de l’entrée dans la boucle est
c 0 = n
p 0 = 1
De plus, le corps de la boucle assure les relations suivantes pour toute itération i :
c i+1 = c i − 1
p i+1 = 2p i
On remarque alors que la propriété suivante est toujours vérifiée : pour toute itération i, on a p i = 2 n−c i
et c i ⩾ 0.