Dans plusieurs rapports de l’épreuve d’informatique de l’X on trouve les phrases suivantes:
peu de candidats ont l’idée d’écrire des invariants de boucle avant de se lancer dans la programmation
l’écriture d’un invariant de boucle est une aide précieuse pour arriver à un programme correct
Et vous l’avez deviné, je n’ai absolument jamais rencontré ce terme! Si je comprends à peu prés de quoi il retourne (en gros une variable qui ne change pas sur un tour d’une boucle(?)), je ne vois pas trop en quoi ça peut aider à programmer.
Bref, merci de votre aide!
Petit exemple :
liafa.jussieu.fr/~gastin/DEU … Invariants
ça ne sert pas à grand chose… en tout cas moi je ne m’en suis jamais servi, et je vis très bien sans 
En gros c’est une propriété qui est vraie à l’entrée de la boucle, et qui est vraie à la sortie aussi. Et pour dire ça, tu dis qu’après chaque itération, si c’est vrai au début de l’itération, cela reste vrai à la fin de l’itération.
C’est un peu la manière standard de prouver qu’un truc fait ce que tu veux qu’il fasse.
Et puis après quand on regarde au niveau sémantique…
Ok merci! Pratique pour vérifier une procédure.
Les invariants de boucles prouvent qu’une boucle respecte quelque chose, ce qui souvent prouve que ce qui sort de la boucle répond bien au problème. Il y a aussi les variants de boucle, qui eux prouvent que l’on va bien sortir de la boucle.C’est la combinaison des deux qui permet de dire qu’un algorithme fonctionne.
Prenons l’exemple de l’algorithme d’Euclide : l’invariant de boucle, c’est que lorsqu’on l’applique, le pgcd de la paire d’entiers manipulée est fixe ; le variant de boucle, c’est que le maximum des valeurs absolues des entiers manipulés est strictement décroissant d’une itération à la suivante.
Avec un peu de chance, je n’ai pas été trop confus.