Correction d'un algorithme

Raisonnement par récurrence

Pour comprendre le cours d'aujourd'hui il peut être intéressant de commencer par évoquer le raisonnement par récurrence.

1) Imaginons que vous devez faire tomber une ligne de 10000 dominos mais que vous ne savez pas à quelle distance les placer les uns des autres. Comment aller-vous procéder pour trouver la bonne distance entre les dominos qui permet de tous les faire tomber ?

Invariant de boucle

On dit qu’un algorithme est correct s’il fonctionne quelque soient les éléments en entrée. Malheureusement un algorithme peut fonctionner sur de nombreux exemples et ne pas être correct. Voici par exmeple des fonctions qui de l'extérieur peuvent parraitre correctes mais ne le sont pas :

def carre(n):
	""" Fonction qui renvoie le carré de n """
	if n == 5423695421546975:
		return 1
	else:
		return n**2

def premier(n):
	""" Fonction qui renvoie des nombres premiers """
	return n**2 + n + 41

On essaie alors de prouver la correction d’un algorithme par un raisonnement logique.

Il est courant d’utiliser ce qu’on appelle un invariant de boucle pour démontrer la correction d’un algorithme. Un invariant de boucle est une propriété logique qui est vraie au début et aussi à la fin de la boucle.

La méthode est toujours la même :

initialisation

on montre que l’invariant de boucle est vrai au début du programme ;

conservation

on montre que si l’invariant de boucle est vrai avant un passage dans la boucle, il reste vrai après le passage dans la boucle ;

terminaison

on montre que l’invariant de boucle en sortie de boucle entraîne la correction de l’algorithme.

Tri par insertion

Nous allons montrer la correction du tri par insertion avec un invariant de boucle. Voici l’algorithme du tri par insertion :

VARIABLE
t : tableau d'entiers
i : nombre entier
j : nombre entier
k : nombre entier
DEBUT
i←2
tant que i<=longueur(t):   // boucle 1
  j←i-1
  k←t[i]
  tant que j>0 et que t[j]>k:   // boucle 2
    t[j+1]←t[j]
    j←j-1
  fin tant que
  t[j+1]←k
  i←i+1
fin tant que
FIN

2) Trouvez un invariant de boucle qui permettrait de montrer la correction du tri par insertion.

3) Montrez la correction du tri par insertion en utilisant un invariant de boucle.

Tri par sélection

Voici l’algorithme du tri par sélection :

VARIABLE
t : tableau d'entiers
i : nombre entier
min : nombre entier
j : nombre entier
DEBUT
i←1
tant que i<longueur(t):   //boucle 1
  j←i+1
  min←i
  tant que j<=longueur(t):   //boucle 2
    si t[j]<t[min]:
      min←j
    fin si
    j←j+1
  fin tant que
  si min≠i :
    échanger t[i] et t[min]
  fin si
  i←i+1
fin tant que
FIN

4) Trouvez un invariant de boucle pour montrer la correction de cet algorithme.

5) Prouvez alors la correction de cet algorithme.