Terminaison

La correction partielle n'est pas suffisante, il faut aussi vérifier que le programme termine.

Exemple: Le programme suivant:

 P:    
  \tt    m:=a;
  \tt    n:=b;
   \tt   while m != n do
   \tt       if m > n then m <- m - n fi
   \tt   od

On vérifie aisément que $\{ a,b \in \mathcal{N}\} P \{ m=pgcd(a,b) \}$ (car $pgcd(a,b)=pgcd(m,n)$ est un invariant, mais ce programme ne termine pas toujours.

La seule instruction pour laquelle le problème de la terminaison se pose est la boucle.

Il n'existe pas de moyen ``automatique'' de prouver la terminaison d'une boucle (en fait, il s'agit d'un problème indécidable), on peut procéder de la façon suivante: définir une expression $e$ à valeur entière dépendant des variables qui décroît à chaque itération et telle que si $e$ devient nulle alors la condition de test de boucle est faux. On vérifie alors aisément qu'alors le nombre d'itérations de la boucle est borné. (toute suite décroissante d'entiers est finie).

Exemple: Dans le programme du PGCD, à chaque itération, $m$ ou $n$ décroît: on peut prendre $e=\vert m-n\vert$ dans ce cas, on a si $e'$ est la valeur de $e$ après l'itération, on vérifie aisément que $e'<e$ et d'autre part si $e=0$ alors $m=n$ ce qui assure que la terminaison.

Pour montrer que la terminaison est un problème difficile on peut considérer le problème suivant: Une Conjecture: On considère la fonction $f :\mathcal{N}^*\to \mathcal{N}^*$ définie par

$$f(n)=n/2 \mbox{ if } n \mbox{ est pair } 3n+1 \mbox{ sinon}$$

On conjecture que si on itère cette fonction à partir d'un entier $n>0$, on finit toujours par atteindre la valeur 1. Cette conjecture, vérifiée expérimentalement jusqu'à $32\times 10^{15}$, n'a pas encore été démontrée.