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.

Afficher la correction

1)

Cet algorithme calcul \(2^n\) où n est le paramètre.

2)

Le variant de boucle qui permet de montrer la terminaison de l’algorithme est \(i\).

Justification :

  • • \(i\) augmente strictement : à chaque tour de boucle \(i\) augmente de \(1\).
  • • \(i\) prend ses valeurs dans d’un ensemble borné (fini) : \(i\) est compris entre \(0\) (valeur initiale de \(i\)) et \(n-1\) (valeur au delà de laquelle on sort de la boucle).

Remarque : on peut aussi prendre \(i - n\) comme variant de boucle.

3)

◦ L’invariant de boucle qui permet de montrer la correction de l’algorithme est : \(resultat = 2^i\).

◦ Montrons que cette relation est bien un invariant de boucle, c’est-à-dire que si elle est vérifiée avant une itération, alors elle l’est encore après :

Hypothèse : \(resultat_{av} = 2 ^ {i_{av}}\)

D’après l’algorithme : \(i_{ap} = i_{av} + 1\) et \(resultat_{ap} = resultat_{av} * 2\)

D’où \(resultat_{ap} = 2 ^ {i_{av}} * 2\) soit \(resultat_{ap} = 2 ^ {(i_{av} + 1)}\) soit \(resultat_{ap} = 2 ^ {i_{ap}}\).

Donc la relation \(resultat = 2^i\) est bien un invariant de la boucle.

◦ Montrons que la relation est vraie avant l’entrée dans la boucle :

A l’initialisation \(résultat = 1\) et \(i = 0\). Or \(2^0 = 1\).

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 :

Afficher la correction

1)

def maxi(li:list[int])->int:
    maxi = li[0]
    i = 0
    while i < len(li):
        if li[i] > maxi:
            maxi = li[i]
        i = i + 1
    return maxi

assert maxi([5]) == 5
assert maxi([5, 10]) == 10
assert maxi([10, 5]) == 10
print('Les tests sont ok')

2.a) Preuve de la terminaison

Le variant de boucle est i.

En effet :

  • • i augmente structement à chaque itération (ligne 7) ;
  • • si i est supérieur ou égal à len(li), la boucle se termine (ligne 4).

2.b) Preuve de la correction de l'algorithme

L'invariant de boucle est la propriété suivante "maxi est la plus grande des valeurs de li de l'indice 0 à l'indice i".

Validité de l'invariant pour i = 0 :

Avant la boucle, pour \(i = 0\), comme maxi = li[0], on a bien que maxi et la plus grande valeur de li de l'indice 0 à l'indice 0.

Conservation de l'invariant lors de l'exécution du code de la boucle :

Hypothèse : l'invariant est vrai à l'indice i, soit maxii est la plus grande valeur de li de l'indice 0 à l'indice i.

On doit montrer qu'il est alors vrai à l'indice i+1, c'est-à-dire que maxii+1 est la plus grande valeur de li de l'indice 0 à l'indice i+1.

• Si li[i+1] > maxii, alors maxii+1 = li[i+1]. Or dans ce cas, la plus grande valeur de li de l'indice 0 à l'indice i+1 sera li[i+1]. CQFD.

• Si li[i+1] ≤ maxii, alors maxi est inchangé, soit maxii+1 = maxii. Or dans ce cas, la plus grande valeur de li de l'indice 0 à l'indice i+1 ne sera pas li[i+1], et maxii+1 restera bien la plus grande valeur de li de l'indice 0 à l'indice i+1. CQFD.

Conclusion :

L'invariant est vrai avant la boucle. Après chaque itération de la boucle, l'invariant reste vrai. Donc l'invariant est vrai après a boucle.

Or après la boucle i = len(li)-1. Donc, après la boucle, maxi est la plus grand valeur de li de l'indice 0 à l'indice len(li)-1. Autrement dit, après la boucle, maxi est la plus grande valeur de li.

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.
Afficher la correction

1)

◦ Le variant de boucle qui permet de montrer la terminaison de l’algorithme est \(b-a\).

◦ Montrons que \(b-a\) fait partie d’un ensemble fini :

\(b-a\) est plus petit que la taille de la liste

\(b-a\) est plus grand que 0 (car sinon on sort de la boucle et dans ce cas l’algorithme se termine bien)

◦ Montrons que \(b-a\) évolue strictement. Ici, on va montrer que \(b-a\) diminue à chaque itération d’au moins \(1\).

On part d’un état \(a_1\) et \(b_1\).

D’après l’algorithme \(m_1 = (a_1-b_1)//2\) Donc \(a_1 ≤ m_1 ≤ b_1\) (relation 1)

Cas n°1 : \(E = L[m_1]\) Dans ce cas l’algorithme sort de la boucle avec le return.

Cas n°2 : \(E < L[m_1]\) Dans ce cas \(a_2=a_1\) et \(b_2=m_1-1\)

Donc, d’après la relation 1, \(b_2 < b_1\)

Donc b-a a bien diminué d’au moins 1.

Cas n°3 : \(E > L[m_1]\) Dans ce cas \(b_2 = b_1\) et \(a_2 = m_1+1\)

Donc, d’après la relation 1, \(a_2 > a_1\).

Donc \(b - a\) a bien diminué d’au moins 1.

◦ Bilan : on a trouvé un invariant convergent de boucle, donc la boucle se termine bien.