Les variants de boucle

Un variant de boucle est un outil théorique clef pour démontrer qu'une boucle termine (c'est à dire ne tourne pas indéfiniment).

L'idée est la suivante: si une variable ne prend que des valeurs distinctes à chaque passage dans la boucle et ne peut prendre, par exemple, qu'au plus 10 valeurs alors il n'y aura qu'au plus 10 passages dans la boucle. La boucle ne peut donc pas être une boucle infinie.

Pour formaliser cette idée, on utilisera la définition suivante.

Définition

On appelle variant d'une boucle "tant que" toute quantité $v$ vérifiant:

• $v\in\mathbb{N}$ (dans la boucle)
• $v$ décroit strictement à chaque passage dans la boucle.

Dans les pages qui suivent, des algorithmes classiques vous sont donnés. L'objectif n'est pas de comprendre comment ils fonctionnent: vous n'aurez à vous concentrer ici que sur l'argumentation du fait que la boucle termine.
Vous constaterez ainsi (en prouvant que l'algorithme termine sans chercher à comprendre comment le calcul est mené à bien) que le problème de la terminaison est relativement "indépendant" du problème de la correction.

Remarque

Certains se demanderont pourquoi démontrer?
Les algorithmes que nous manipulons en première sont en effet suffisamment simples pour suivre leur logique sans outil théorique. Pire, certains d'entre vous trouveront les outils de preuve présentés ici bien plus obscurs que l'algorithme lui-même.

Mais plus vous irez loin dans la connaissance de l'informatique, plus vous rencontrerez d'algorithmes dont la logique est difficile, voire impossible à appréhender sans outil théorique. L'objectif en première est de s'initier à ces outils théoriques sur quelques exemples simples.