C17.4 : 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.

🖊️ 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_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

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 :