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 :

Nous allons reprendre plus en détail la notion de preuve d'un algorithme qui se décline en deux notions :

  • - la preuve de correction ;
  • - la preuve de terminaison.

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) :

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) En utilisant la boucle whlie, écrire une fonction qui prend une liste non vide de nombres entiers en paramètre et renvoie la valeur maximale de la liste.

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

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

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

Remarque :

La démonstration de l'invariant est fastidieuse, elle n'est donc pas demandée.

Pour information l'invariant de boucle peut se formuler de la façon suivante :

  • - 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.