Introduction
Lorsque l'on écrit un programme informatique, il est souvent bienvenu de prouver que ce programme termine toujours.
En effet, si l'on prend l'exemple de la conduite autonome, il est bon de savoir que notre voiture ne va pas rentrer dans une boucle infinie lorsqu'elle repère un obstacle.
On va donc ici s'intéresser à la terminaison des algorithmes et des boucles.