Six questions courtes sur la terminaison et la correction.
1.Un algorithme qui, sur une entrée valide, ne s’arrête jamais est :
2.Un variant de boucle est :
3.Un invariant de boucle sert à établir :
4.Les trois étapes d’une preuve par invariant sont :
5.Dans une boucle de condition i⩽n où i augmente de 1 à chaque tour et où n ne change pas, quel variant convient ?
6.La correction totale, c’est :
Pour chacune des affirmations suivantes, dire ce qu’elle établit exactement : la terminaison, la correction partielle, la correction totale, ou rien de tout cela. Justifier en une phrase.
Affirmation : « La fonction a été essayée sur quarante jeux de tests, et renvoie à chaque fois la valeur attendue. »
Rien de tout cela. Un jeu de tests porte sur un nombre fini d’entrées et ne dit rien des autres : il peut révéler une erreur, jamais garantir qu’il n’en reste aucune.
Affirmation : « Si la fonction s’arrête, alors la valeur renvoyée vérifie la postcondition. »
La correction partielle, qui est exactement cet énoncé conditionnel. Rien n’est dit du cas où la fonction ne s’arrête pas.
Affirmation : « La quantité n−i est un entier naturel tant que la boucle tourne, et elle diminue de 1 à chaque tour. »
La terminaison. C’est la définition d’un variant de boucle, et un variant entraîne la terminaison : le nombre de tours est majoré par la valeur initiale du variant augmentée de 1.
Affirmation : « La propriété I est un invariant de la boucle, la négation de la condition d’arrêt jointe à I donne la postcondition, et n−i est un variant. »
La correction totale. L’invariant donne la correction partielle par initialisation, conservation et finalisation, le variant donne la terminaison, et la correction totale est la conjonction des deux.
Reprendre les définitions de correction partielle et de correction totale, et regarder laquelle des deux mentionne la terminaison.
Pour chacune des boucles suivantes, proposer un variant et vérifier les deux conditions de la définition : rester dans N tant que la boucle tourne, et décroître strictement d’un tour au suivant.
k est un entier naturel, et la boucle s’écrit while k > 0: k = k - 3.
Le variant v=k convient. Tant que la condition est vérifiée, k est un entier strictement positif, donc un entier naturel, et chaque tour remplace k par k−3, strictement plus petit. La boucle termine donc, même si k peut devenir négatif au dernier tour : la définition n’exige la positivité qu’au début des tours effectivement exécutés.
x est un entier supérieur ou égal à 1, et la boucle remplace x par le quotient de la division entière de x par 2, tant que x>1.
Le variant v=x convient : tant que x>1, c’est un entier naturel, et la division entière donne une nouvelle valeur au plus égale à x/2, donc strictement inférieure à x. La boucle termine.
Pour x=100, combien de tours la boucle de la question b effectue-t-elle ?
Les valeurs successives de x au début de chaque tour sont 100, 50, 25, 12, 6 puis 3, et la condition devient fausse lorsque x vaut 1. Six tours sont donc exécutés.
l est une liste, et la boucle retire son premier élément tant qu’elle n’est pas vide.
Le variant v=len(l) convient : c’est un entier naturel, et supprimer le premier élément d’une liste non vide diminue sa longueur de 1 exactement.
5 blocs de plus : les autres énoncés et tous les corrigés, rédigés en entier. Le reste du programme est écrit de la même main, avec les figures interactives et votre progression.