Un invariant de boucle

Exercice supplémentaire · niveau 3 (difficile) · sciences numériques et technologie (seconde), chapitre 4 — Les boucles · Du langage naturel à Python

Énoncé

On considère le programme ci-dessous, qui calcule $x^{n}$ .

resultat = 1
base = x
exposant = n
while exposant > 0:
    resultat = resultat * base
    exposant = exposant - 1

Vérifier qu'à chaque passage, la quantité $resultat \times base^{exposant}$ garde la même valeur. À quoi sert cette observation ?

Corrigé

Vérification. Avant le premier tour, la quantité vaut $1 \times x^{n} = x^{n}$ . À chaque tour, resultat est multiplié par base tandis que exposant diminue de $1$ , donc base**exposant est divisé par base : le produit est inchangé.

À la sortie, exposant vaut $0$ , donc la quantité vaut $resultat \times base^{0} = resultat$ . Comme elle valait $x^{n}$ au départ et n'a jamais changé, resultat contient $x^{n}$ .

C'est une démonstration de correction, et non un simple test. Un jeu d'essais montre qu'un programme marche sur les cas essayés ; un invariant montre qu'il marche toujours. La méthode est générale : trouver une quantité que la boucle préserve, puis regarder ce qu'elle devient à la sortie.

Prolongement. Le même invariant permet l'exponentiation rapide : quand exposant est pair, on peut mettre base au carré et diviser exposant par $2$ — le produit reste inchangé, mais on va deux fois plus vite.

Les autres exercices de ce chapitre Le cours du chapitre

Un blocage sur cet exercice ? Le tuteur d'Adloun guide par questions, sans donner la réponse.