6.1. Preuve d’un algorithme

Prouver un algorithme signifie démontrer qu’un algorithme effectue bien la tâche qui lui est demandée.

6.1.1. Terminaison

Il s’agit de montrer que l’algorithme se termine bien. La question se pose notamment lorsque l’algorithme comporte une boucle conditionnelle while. La plupart du temps, cela revient à montrer qu’une quantité entière positive décroît strictement à chaque itération de la boucle (une suite d’entiers naturels strictement décroissante est nécessairement finie). Cette quantité est généralement appelé le variant.

On peut par exemple étudier l’algorithme d’Euclide pour le calcul du pgcd.

def pgcd(a, b):
  while b!= 0:
      a, b = b, a % b
  return a

On suppose que l’argument b est un entier naturel. En notant \(b_k\) la valeur de b à la fin de la \(k^\text{ème}\) itération (\(b_0\) désigne la valeur de b avant d’entrer dans la boucle), on a \(0\leq b_{k+1}<b_k\) si \(b_k>0\). La suite \((b_k)\) est donc une suite strictement décroissante d’entiers naturels : elle est finie et la boucle se termine.

6.1.2. Correction

Il s’agit de savoir si l’algorithme fournit bien la réponse attendue. Si l’algorithme comporte une boucle, on recherche généralement une quantité ou une propriété qui ne change pas au cours des itérations : on parle d\”invariant de boucle.

A nouveau, on peut étudier l’algorithme d’Euclide.

def pgcd(a, b):
  while b!= 0:
      a, b = b, a % b
  return a

On note \(a_k\) et \(b_k\) les valeurs de a et b à la fin de la \(k^\text{ème}\) itération (\(a_0\) et \(b_0\) désignent les valeurs de a et b avant d’entrer dans la boucle). Or, si \(a=bq+r\), il est clair que tout diviseur commun de \(a\) et \(b\) est un diviseur commun de \(b\) et \(r\) et réciproquement. Notamment, \(a\wedge b=b\wedge r\). Ceci prouve que \(a_k\wedge b_k=a_{k+1}\wedge b_{k+1}\). La quantité \(a_k\wedge b_k\) est donc bien un invariant de boucle. En particulier, à la fin de la dernière itération (numérotée \(N\)), \(b_N=0\) de sorte que \(a_0\wedge b_0=a_N\wedge b_N=a_N\wedge0=a_N\). La fonction pgcd renvoie donc bien le pgcd de a et b.