1NSI : cours Correction d'un Algorithme⚓︎
La Correction d'un algorithme répond à la question suivante:
Cet algorithme fait-il vraiment ce qu'il est censé faire?
Correction d'un Algorithme
Un algorithme est dit
Comment savoir si un algorithme est correct?⚓︎
Cas simple de correction d'un algorithme:
Lorsque l'algorithme reproduit directement la spécification, on est sûr que celui-ci est correct.
Cas général, et de manière plus formelle:
C'est plus compliqué lorsque:
- la spécification est compliquée, ou bien,
- la spécification ne dit pas comment obtenir le résultat il est est plus compliqué de répondre instantanément,
On utilise alors la notion d'invariant de boucle qui est un outil pour démontrer la correction d'un algorithme.
Invariant de boucle⚓︎
Invariant de Boucle
Un
- cette propriété est vraie avant la première itération : on dit dans ce cas que \(P(0)\) est vraie
- Si cette propriété \(P\) est vraie en entrant dans la \(i^{ème}\) itération (on dit "si \(P(i)\) est vraie"), Alors \(P\) reste encore vraie en sortant de la \(i^{ème}\) itération, donc la propriété \(P\) est encore vraie en entrant dans la \((i+1)^{ème}\) itération (càd que \(P(i+1)\) est encore vraie)
En particulier et en pratique: un invariant de boucle restera vrai en sortant de la boucle (après sa dernière itération): et c'est cette dernière propriété qui doit démontrer la correction de l'algorithme.
Lien entre Existence d'une invariant de boucle et Correction
L'existence d'un invariant de boucle adapté au problème posé, prouve la correction de l'algorithme.
En pratique : comment démontrer qu'un algorithme est correct?⚓︎
Comment prouver la correction d'un algorithme ?
La démonstration de la correction d'un algorithme se fait en \(3\) étapes:
- Initialisation : Montrer que l'invariant de boucle est vrai en entrant dans la première itération
- Hérédité / Conservation : Montrer que Si l'invariant de boucle est vrai en entrant dans une itération, Alors il reste vrai en sortant de l'itération (donc encore vrai en entrant dans l'itération suivante)
- Terminaison : déduire de l'invariant de boucle final la propriété qui répond au problème posé
Exemple 1: Recherche d'un extremum dans un tableau
On se donne un tableau \(A\) de \(n\) éléments, noté \([A[0],A[1],...,A[n-1]]\), constitué de valeurs entières (ou flottants, ou plus généralement des p-uplets de tels nombres avec l'ordre lexicographique, voire des chaînes de caractères)
# Recherche du minimum des valeurs du tableau A
minimum prend la 1ère valeur du tableau A
Pour chaque nombre nb du tableau A
Si nb < minimum
Alors minimum prend la valeur nb
afficher minimum
- (Exercice) Implémenter cet algorithme en Python
- un invariant de boucle possible est la propriété:
"En entrant dans la \(i^{ème}\) itération, la variable minimum contient le minimum parmi les valeurs \(i\) premières valeurs du tableau", (c'est-à-dire le minimum du sous-tableau \([A[0],...,A[i-1]]\))
Démonstration de la Correction de l'algorithme:
- Initialisation : En entrant dans la 1ère itération, la variable minimum contient bien le minimum de l'unique première valeur du tableau
- Hérédité / Conservation : Si, en entrant dans la \(i^{ème}\) itération la variable minimum contient le minimum du sous-tableau \([A[0],...,A[i-1]]\), Alors :
- le nombre \(nb\) est en fait la \((i+1)^{ème}\) valeur notée \(A[i]\)
- Si \(nb\) est inférieur au plus petit des \(i\) premières valeurs du tableau \(A\), alors la variable minimum prend cette nouvelle valeur comme étant la plus petite, si bien que la variable minimum contiendra le minimum des \((i+1)\) premières valeurs du tableau \(A\), (et sinon, rien à faire)
- en sortant de la \(i^{ème}\) itération (donc aussi en entrant dans la \((i+1)^{ème}\) itération) la variable minimum contient donc bien le minimum des valeurs \([A[0],...,A[i]]\)
- Terminaison : La tableau étant de taille \(n\), en sortant de la dernière (la \(n^{ème}\)) itération la variable minimum contient donc le minimum du sous-tableau \([A[0],...,A[n-1]]\), qui est en fait exactement le tableau \(A\). Ceci prouve la correction de l'algorithme.
Exemple 2: Algorithme d'Euclide
# on suppose que a >= b
Saisir a, b
Tant que b n'est pas égal à 0
(a, b) <- (b, a mod b)
afficher a
Notons \(d\) le \(pgcd\) recherché (pour les valeurs de \(a\) et de \(b\) initiales). Un invariant de boucle possible est la propriété:
"\(d = pgcd\) de la valeur courante de \(a\) et de la valeur courante de \(b\)"
Preuve de la correction de l'algorithme d'Euclide
- Initialisation : trivial, car avant d'entrer dans la 1ère itération, les variables \(a\) et \(b\) contiennent leurs valeurs initiales, donc \(d = pgcd(a, b)\)
- Hérédité / Conservation : Quelles que soient les valeurs courantes prises par \(a\) et \(b\) en entrant dans une itération: Si \(d = pgcd(a, b)\) pour ces valeurs courantes \(a\) et \(b\), Alors puisque (propriété mathématique) \(d = pgcd(a,b) = pgcd (b, a \text{ mod } b)\), l'invariant de boucle est encore vrai en sortant de l'itération (donc encore en entrant dans la suivante itération)
- Terminaison : en sortant de la dernière itération, on sait que \(d=pgcd(a,b)\) pour les valeurs courantes de \(a\) et \(b\), et on sait aussi que \(b=0\) (car on est sorti de la boucle..), donc \(d=pgcd(a,0)=a\) (car \(0\) est divisible par tout entier). Donc l'algorithme retourne bien (la valeur courante de \(a\), qui est bien) le pgcd des valeurs initiales de \(a\) et \(b\). Ceci prouve la correction de l'algorithme.