Cours NSI-SNT

Preuve d’un algorithme

Préambule

Lorsqu’on écrit un algorithme, trois questions fondamentales se posent :

• Est-ce qu’il se termine ? => C’est ce que l’on appelle la terminaison.
• Est-ce qu’il donne le résultats attendu ? => C’est ce que l’on appelle la correction.
• Est-ce qu’il donne le résultat en utilisant des ressources (temps, mémoire…) raisonnables ? => C’est ce que l’on appel la complexité.

Remarque : Démontrer la terminaison et la correction d’un algorithme s’appelle faire la preuve de cet algorithme.

Définitions

Terminaison d'un algorithme
Vérifier la terminaison d'un algorithme est en particulier nécessaire lorsque celui-ci comporte des boucles.
Dans ce cas, cela peut se faire en déterminant un variant de boucle qui converge (ou parle également de variant convergent).
Un variant convergent de boucle est une quantité qui prend ses valeurs dans un ensemble bien déterminé et qui évolue dans le même sens strictement à chaque itération de la boucle.

Correction d'un algorithme
Vérifier la correction d'un algorithme est en particulier nécessaire lorsque celui-ci comporte des boucles.
Dans ce cas, cela peut se faire en utilisant un invariant de boucle.
On appelle invariant de boucle une propriété qui, si elle est vraie avant l’entrée dans une boucle, reste vraie après chaque passage dans la boucle, et donc est vraie aussi à la sortie de la boucle.

Mise en pratique

Considérons l’algorithme suivant :

def fonc(n):
    '''
    param n: (int) un entier positif ou nul
    return (int)
    '''
    resultat = 1
    i = 0
    while i < n:
        i = i + 1
        resultat = resultat * 2
    return resultat

🖊️ 1) Que fait cet algorithme (à trouver sans essayer l’algorithme) ? Compléter la docstring et changer le nom de cette fonction.

🖊️ 2) Quel est le variant convergeant de boucle pour cet algorithme.

🖊️ 3) Trouver un invariant de boucle. On pourra écrire une relation entre les différentes variables.

Application à l’algorithme de recherche dichotomique

Rappel de l’algorithme

def recherche_dicho(E,L):
    '''
    Recherche dichotomique d'un élément dans une liste d'entiers triée.
    Renvoie la position de l'élément s'il est présent dans la liste.
    Renvoie None si l'élément n'est pas présent dans la liste.
    param L : (list) une liste d'entiers triés par ordre croissant
    param E : (int) un entier
    return : (int) position de l'entier ou -1
    '''
    debut = 0
    fin = len(L)-1
    milieu = (debut + fin) // 2
    while (debut - fin) <= 0 :
        if E > L[milieu]:
            debut = milieu + 1
        elif E < L[milieu]:
            fin = milieu - 1
        else :
            return milieu
        milieu = ( debut + fin ) // 2
    return -1

Terminaison de l’algorithme

🖊️ Trouver un variant convergent de boucle pour montrer la terminaison de l’algorithme.

Correction de l’algorithme

Ici, il faut trouver un invariant de boucle, c’est à dire trouver une propriété qui est vraie avant la boucle et à la fin de chaque boucle.

Voici l’invariant :

• Formulation n°1 : si E est présent dans L, alors L[debut] ≤ E ≤ L[fin].
• Formulation n°2 : si E est présent dans L à une position pos, alors debut ≤ pos ≤ fin