Prouver un algorithme

On devait pour aujourd’hui implémenter l’algorithme de recherche dichotomique sur un tableau trié :

def recherche_dichotomique(tab, val):
    """ Recherche val dans un tableau tab
        tab est supposé trié """

    # initialisation
    gauche = 0
    droite = len(tab) - 1
    
    while gauche <= droite:
        milieu = (gauche + droite) // 2
        if tab[milieu] == val:
            # on a trouvé val dans le tableau,
            # à la position milieu
            return milieu
        elif tab[milieu] > val:
            # on cherche entre gauche et milieu - 1
            droite = milieu - 1
        else:             # on a tab[milieu] < val
            # on cherche entre milieu + 1 et droite
            gauche = milieu + 1

    # on est sorti de la boucle sans trouver val
    return -1


#tests

liste = [1, 3, 5, 7, 9]
print(liste)
for truc in [0, 42, 5 , 3, 7, 2, 8, 9, 1, -52]:
    print("Pour", truc, "on obtient",
          recherche_dichotomique(liste, truc))
[1, 3, 5, 7, 9]
Pour 0 on obtient -1
Pour 42 on obtient -1
Pour 5 on obtient 2
Pour 3 on obtient 1
Pour 7 on obtient 3
Pour 2 on obtient -1
Pour 8 on obtient -1
Pour 9 on obtient 4
Pour 1 on obtient 0
Pour -52 on obtient -1
>>>

C’est sans difficulté, puisqu’on vous avait donné ce document institutionnel (à comprendre jusqu’au milieu de la troisième page) et que ce code figurait au milieu de la deuxième page.


Prouver un algorithme – en deux temps (à savoir) :

  • Il faut prouver qu’il se termine : On parle de terminaison.

    On utilise ici un variant de boucle, en général

    • soit une variable qui augmente et ne peut pas dépasser un « plafond »
    • soit une variable qui diminue et ne peut pas passer sous un « plancher »
  • Il faut prouver qu’il fait bien ce que l’on attend de lui : On parle de correction.

    Pour cela, on va chercher un un invariant de boucle.

    C’est quoi un « invariant de boucle ? »

    C’est une propriété qui est vérifiée avant l’entrée dans la boucle,
    qui est vérifiée à chaque itération de la boucle et qui amène au résultat escompté à la sortie de la boucle.


Exemple facile pour commencer

Soit l’algorithme

def deux_puissance(n):

    assert n >=0

    #initialisation
    i = 0
    reponse = 1
    
    # traitement :
    while i < n : 
        i += 1
        reponse *= 2

    # terminé :
    return reponse

# tests
assert deux_puissance(0) == 1
assert deux_puissance(1) == 2
assert deux_puissance(2) == 4
assert deux_puissance(8) == 256

Cette fonction passe sans encombres les tests caractérisés par

  • les quatre assert en fin de code qui testent quatre valeurs de retour,
  • le assert en début de fonction qui teste les préconditions « n positif ou nul ».

Mais nous voulons prouver cet algorithme !

  • Terminaison :

    Le variant de boucle est clairement ici i qui augmente forcément avec l’incrémentation i += 1 dans la boucle while. Quand i atteint n, qui est forcément positif ou nul, l’algorithme termine. La terminaison est donc assurée.

  • Correction :

    On veut que le programme renvoie 2 ** n quel que soit n positif ou nul.
    L’invariant de boucle est par exemple ici la propriété

    « reponse vaut 2 ** i »

    • Avant la boucle, i vaut zéro et reponse vaut 1 soit 2 ** 0. OK
    • Si l’invariant « reponse vaut 2 ** i » est vraie à la fin d’un passage de la boucle, au passage suivant
      • i passera à i + 1
      • reponse vaudra reponse * 2 soit 2 ** i * 2 soit 2 ** (i +1). OK
    • Au sortir de la boucle, l’invariant est donc encore respecté et la dernière valeur de i est n donc « reponse vaut 2 ** n » et c’est bien la bonne valeur qu’on renvoie.
    • La correction est donc assurée.

Prouver notre algorithme de dichotomie

On s’appuie sur ce document institutionnel où il est prouvé.

Commentaires.


Et nos tris ?

Et bien pour les deux tris par sélection ou par insertion étudiés :

  • Un variant de boucle est rang initialisée à zéro puis incrémentée et qui ne dépassera pas len(tab). Ceci prouve la terminaison.
  • Un invariant de boucle est

    « les éléments sont triés jusqu’à rang »

    Souvenons-nous que nous l’avions bien souligné (et même encadré en vert). Ceci permet de prouver la correction.

N'hésitez-pas à poser une question, ou faire avancer le schmilblick

Entrez vos coordonnées ci-dessous ou cliquez sur une icône pour vous connecter:

Logo WordPress.com

Vous commentez à l’aide de votre compte WordPress.com. Déconnexion /  Changer )

Photo Google

Vous commentez à l’aide de votre compte Google. Déconnexion /  Changer )

Image Twitter

Vous commentez à l’aide de votre compte Twitter. Déconnexion /  Changer )

Photo Facebook

Vous commentez à l’aide de votre compte Facebook. Déconnexion /  Changer )

Connexion à %s

Ce site utilise Akismet pour réduire les indésirables. En savoir plus sur la façon dont les données de vos commentaires sont traitées.