C7.7 : Preuve d'un algorithme

Rappels : qu'est-ce que la preuve d'un algorithme ?

Valider un algorithme

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ésultat attendu => C'est ce que l'on appelle la correction.
• - Est-ce qu'il donne le résultat en utilisant des ressources (principalement du processeur et de la mémoire...) raisonnables => C'est ce que l'on appelle la complexité.

Définitions

Terminaison d'un algorithme

Faire la preuve de 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.

Un variant de boucle est une grandeur (une variable) :

• - qui prend ses valeurs dans un ensemble borné,
• - qui évolue (diminue ou augmente) strictement à chaque itération de la boucle.

Propriété : l'existence d'un variant de boucle démontre la terminaison de la boucle.

Correction d'un algorithme

Faire la preuve de 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.

Un invariant de boucle est 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 encore vraie à la sortie de la boucle.

Applications

Application n° 1 : Un exemple pour bien comprendre

Considérons l'algorithme (rédigé en Pyhton) 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.

2) Trouver un variant de boucle pour cet algorithme.

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

Application n° 2 : Plus grande valeur d'une liste

1) Écrire une fonction qui prend une liste de nombres entiers positifs comme paramètre et renvoie la valeur maximale de la liste.

2) Faire la preuve de l'algorithme utilisé en trouvant :

• - un variant de boucle,
• - un invariant de boucle.

Application n° 3 : Recherche dichotomique dans une liste triée

Considérons la version ci-dessous de l'algorithme de recherche dichotomique d'une valeur dans une liste triée.

def recherche_dichotomique(E,L):
    '''
    param E: (int) un entier
    param L: (list) une liste d'entiers
    '''
    a = 0
    b = len(L)-1
    m = (a + b) //2
    while b - a > 0 and E != L[m]:
        if E < L[m]:
            b = m-1
        else:
            a = m+1
        m = (a + b) //2
    if E == L[m]:
        return m
    else :
        return -1

Faire la preuve de l'algorithme de recherche dichotomique dans une liste triée

1) Trouver un variant convergent de boucle pour montrer la terminaison de l'algorithme.

Remarque) La proposition ci-dessous est un invariant de boucle :

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