Invariant de boucle
Pourquoi parler d'invariant ?
Lorsqu'on utilise une boucle (for ou while), on modifie souvent des variables à chaque itération. Mais certaines propriétés restent vraies tout au long de la boucle : ce sont les invariants.
Un invariant de boucle est une condition logique qui est vraie :
- avant la première itération de la boucle,
- à la fin de chaque itération.
Cela aide à comprendre et à prouver que l’algorithme fonctionne correctement.
Exemple : somme d’une liste
On souhaite calculer la somme des éléments d’une liste.
liste = [2, 5, 7, 3]
somme = 0
for valeur in liste:
somme += valeur
Pendant l’exécution, à chaque tour de boucle :
sommecontient la somme des éléments déjà parcourus de la liste.
Donc, invariant de boucle :
somme contient la somme des éléments de
listedéjà vus.
Autre exemple : chercher le plus grand élément
liste = [6, 4, 9, 1]
maximum = liste[0]
for element in liste[1:]:
if element > maximum:
maximum = element
Ici, l’invariant est :
maximumcontient la plus grande valeur parmi celles déjà parcourues.
Pourquoi c’est utile ?
- Pour raisonner sur le fonctionnement d’un programme.
- Pour vérifier qu’un algorithme est correct.
- Pour démontrer un résultat en maths ou en informatique (preuve de correction).
Les invariants sont souvent utilisés dans les démonstrations formelles, mais même sans entrer dans les preuves, ils aident à mieux comprendre le comportement d’un algorithme.
En résumé
| Terme | Signification |
|---|---|
| Invariant de boucle | Une propriété qui reste vraie à chaque tour de boucle |
| Avant la boucle | L’invariant est déjà vrai avant la première itération |
| Après chaque itération | L’invariant reste vrai, même si les variables changent |
| Utilité | Vérifier la logique, corriger un bug, ou prouver que l’algorithme fonctionne |