Algo Insertion 2

Identification

Infoforall

8 - Preuve du tri par insertion


Une activité-leçon assez théorique et mathématique par certains côtés. Mais vous allez voir aujourd'hui une chose assez fabuleuse : on peut prouver qu'un algorithme répond toujours correctement, ou pas...

Quasiment toutes les questions sont munies de la correction.

Logiciel nécessaire pour l'activité : Python 3 : Thonny, IDLE ou le site repl.it ...

Prérequis : Algorithme : tri par insertion

Evaluation ✎ : questions 15-16-20

Résumé de cours : open document ou pdf

1 - Rappel visuel du tri et algorithme

Nous avons tout vu dans l'activité précédente. Si vous ne vous en souvenez plus trop, voici l'animation suivi de l'algorithme. Le tout est également disponible dans l'onglet FICHES de l'accueil de la partie ALGO.

Index 00 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19
Elément 90 60 20 50 80 10 90 99 30 90 70 10 20 70 98 30 40 90 90 60
Algorithme de tri par insertion

But : trier sur place un tableau initialement non trié.

(ici par odre croissant)

Description des entrées / sortie

  • ENTREES :
    • tableau : un tableau contenant au moins deux éléments.
    • (optionnelle selon les langages d'implémentation): longueur, le nombre d'éléments dans le tableau
  • SORTIE : aucune. Le tableau est trié sur place. On modifie directement tableau.

Exemple :

Prenons tableau = [13, 18, 89, 1024, 45, -12, 18]

Initialement le tableau contient donc cela :

Index 0 1 2 3 4 5 6
Elément 13 18 89 1024 45 -12 18

Après le tri, le tableau contiendra cela :

Index 0 1 2 3 4 5 6
Elément -12 13 18 18 45 89 1024

Algorithme de tri par insertion, commenté

    i est l'index (flèche en vert clair dans l'animation) de la clé-valeur qu'il faut placer

    POUR i variant de 1 à (longueur - 1)

      cletableau[i]

      on mémorise dans cle la valeur-clé car cette case risque d'être écrasée

      ji - 1

      La variable j contient initialement l'index juste à gauche de la clé (flèche verte dans l'animation)

      TANT QUE j ≥ 0 et que tableau[j] > cle

        tableau[j+1]tableau[j]

        On décale la valeur d'une case à droite

        jj - 1

        On passe à la case suivante à gauche

      Fin TANT QUE

      tableau[j+1]cle

      On place la valeur-clé à la place voulue pour obtenir un sous-tableau trié

    Fin POUR

    Renvoyer VIDE (∅)

Algorithme de tri par insertion, non commenté

    POUR i variant de 1 à (longueur - 1)

      cletableau[i]

      ji - 1

      TANT QUE j ≥ 0 et que tableau[j] > cle

        tableau[j+1]tableau[j]

        jj - 1

      Fin TANT QUE

      tableau[j+1]cle

    Fin POUR

    Renvoyer VIDE (∅)

2 - Preuve de terminaison

Pour rappel :

Variant de boucle

Pour prouver qu'une boucle non bornée (Tant que) s'arrête, il faut montrer

  • que la condition de poursuite de la boucle est de type while un > 0 et
  • que la suite un est une suite à valeurs
    • entières
    • strictement décroissante (on est certain que la valeur diminue à chaque boucle)
    • positives (on a bien une valeur supérieure à 0 au début) si on veut savoir si elle s'effectue au moins une fois

Cette suite un est ce qu'on nomme le variant de boucle.

Dans ce cas, le variant va nécessairement décroitre et devenir à un moment négatif ou nul. Par contre, si on veut que la boucle soit parcourue au moins une fois, le variant doit bien être initialement positif.

L'arrêt est donc obligatoire au bout d'un certain nombre de bouclages si on peut écrire la condition sous une forme semblable à :

1
while un > 0 :

Prouver la terminaison d'un algorithme revient donc à dire qu'on est certain que l'algorithme va s'arrêter quelque soit l'entrée (pourvu que l'entrée respecte les préconditions bien entendu).

01° Je vous donne ci-dessous trois façons de faire la même chose. Analysez bien les trois façons de faire pour vous persuader que ces actions provoquent le même comportement de boucle.

Montrer alors la terminaison de la boucle en utilisant la version TANT QUE.

Version avec une boucle bornée POUR

    POUR i variant de 45 à 199 par incrémentation de 10

      Faire un truc (qui ne modifie pas la valeur de i !)

    Fin POUR

Version avec une boucle non bornée TANT QUE

    i45

    TANT QUE i < 200

      Faire un truc (qui ne modifie pas la valeur de i !)

      ii + 10

    Fin TANT QUE

Version Python avec la boucle bornée FOR

1 2
for i in range(45,200,10) : faire_un_truc()

...CORRECTION...

Je vais travailler avec la forme TANT QUE.

On voit que i a pour valeur initiale 45 et augmente de 10 à chaque tour de boucle.

On peut donc représenter les valeurs successives que va prendre la variable i par une suite entière arithmétique de valeur intiale 45 et de raison 10.

in = 45 + 10*n

On peut donc écrire de cette façon la condition de la boucle TANT QUE :

On part de la condition de départ :

    TANT QUE in < 200

On remplace la suite in par son expression :

    TANT QUE (45 + 10*n) < 200

On fait tout passer dans le membre de droite :

    TANT QUE 0 < (200 - 45 - 10*n)

On simplifie :

    TANT QUE 0 < (155 - 10*n)

On écrit la comparaison dans l'autre sens 

    TANT QUE (155 - 10*n) > 0

On pose

un = 155 - 10*n

En utilisant notre variant, la condition devient alors :

    TANT QUE un > 0

On en déduit que la boucle se termine puisque le variant un est bien

  • une suite d'entiers
  • initialement positive (155)
  • strictement décroissante (puisque sa raison est r = - 10)

Regardons maintenant notre algorithme de tri.

    POUR i variant de 1 à (longueur - 1)

      cletableau[i]

      ji - 1

      TANT QUE j ≥ 0 et que tableau[j] > cle

        tableau[j+1]tableau[j]

        jj - 1

      Fin TANT QUE

      tableau[j+1]cle

    Fin POUR

    Renvoyer VIDE (∅)

On voit qu'il y a une boucle (TANT QUE) à l'intérieur d'une autre boucle (POUR).

Prouver la terminaison de l'algorithme demande donc de prouver la terminaison de chacune de ces boucles.

Commençons par la boucle TANT QUE interne.

02° On ne tiendra compte ici que d'une des façons de sortir de la boucle : si la boucle se termine avec une condition, elle se terminera aussi avec deux conditions associées par un ET.

La variable cle contient elle une valeur entière quelconque.

Première question : à partir du vrai algorithme, montrer que la variable j fait initialement référence à un entier supérieur ou égal à 0.

Deuxième question : montrer alors la terminaison de la boucle TANT QUE simplifiée.

      TANT QUE j ≥ 0

        tableau[j+1]tableau[j]

        jj - 1

      Fin TANT QUE

...CORRECTION...

Question 1

Pour trouver les valeurs prises par j, il faut regarder le début de l'algorithme.

    POUR i variant de 1 à (longueur - 1)

      ...

      ji - 1

      ...

    Fin POUR

On voit donc que j vaut i moins 1.

i valant au moins 1, j vaut au moins 0.

Question 2

Pour prouver qu'une boucle non bornée (Tant que) s'arrête, il faut montrer

  • que la condition de poursuite de la boucle est de type while un > 0 et
  • que la suite un est une suite à valeurs
    • entières
    • positives (on a bien une valeur supérieure à 0 au début)
    • strictement décroissante (on est certain que la valeur diminue à chaque boucle)

Ici, nous avons ceci :

      TANT QUE j ≥ 0

        tableau[j+1]tableau[j]

        jj - 1

      Fin TANT QUE

On voit donc qu'on a une suite arithmérique de raison -1 avec une valeur initiale jO supérieure ou égale à 0.

On peut donc écrire que jn = jO - n.

Ce variant est donc bien une suite entière strictement décroissante.

La condition de notre TANT QUE pouvant s'écrire TANT QUE jn ≥ 0, on en déduit que cette boucle TANT QUE se termine.

Il nous reste à gérer le cas de la boucle FOR externe. Comme il s'agit d'une boucle FOR, il s'agit juste de vérifier que la valeur de fin est bien atteignable et qu'on ne modifie pas de façon maladroite la valeur de boucle en dehors de l'incrémentation.

03° Montrer la terminaison de la boucle FOR ci-dessous (vous pourriez transformer la boucle FOR en TANT QUE et trouver un variant qui soit une suite d'entiers strictement décroissante).

    POUR i variant de 1 à (longueur - 1)

      cletableau[i]

      ji - 1

      ...

      tableau[j+1]cle

    Fin POUR

...CORRECTION...

Comme on ne précise pas la variation de la variable de boucle, c'est qu'on utilise la valeur par défaut : on augmente de 1 à chaque tour.

On peut donc écrire la variable de boucle sous la forme suivante :

in = 1 + n.

On peut écrire la boucle FOR sous la forme d'une boucle TANT QUE :

    i1

    TANT QUE i < longueur

      ...

      ii + 1

      ...

    Fin POUR

Cela revient à écrire :

TANT QUE in < longueur

TANT QUE 1 + n < longueur puisque in = 1 + n.

TANT QUE 0 < ( longueur - n - 1 )

TANT QUE ( longueur - n - 1 ) > 0

TANT QUE un > 0

Comment conclure ? Simplement en disant que le variant un = longueur - n - 1 est une suite d'entiers initialement positive (puisque longueur - 1 est positive) et strictement décroissante (puisque la raison de la suite arithmétique est -1).

Et voilà.

Ici, on vous demandait la démonstration pour l'exercice mais, habituellement, on peut valider beaucoup plus vite la terminaison d'un FOR ! C'est même l'un de ses avantages sur le WHILE. Il suffit de vérifier qu'on ne touche pas à la variable de boucle dans la boucle (avec certains langages, c'est possible) et que les bornes soient bonnes :

  • Boucle FOR croissante : vérifier que la valeur finale est bien supérieure à la valeur initiale.
  • Boucle FOR décroissante : vérifier que la valeur finale est bien inférieure à la valeur initiale.

Nous venons de prouver que les deux boucles de notre algorithme se terminent. L'algorithme se termine donc également.

Oui, mais... Est-il rapide ?

3 - Coût du tri par insertion

Nous allons maintenant étudier la complexité de notre algorithme dans le meilleur des cas et dans le pire des cas.

Pour cela, nous allons regarder le nombre de comparaisons à effectuer lorsque notre tableau possède n éléments.

Dans le meilleur des cas

Pour cet algorithme, c'est quand le tableau est déjà trié dans le bon ordre !

04° Utiliser l'animation ci-dessous qui correspond au tri par insertion d'une liste déjà triée en ordre croissant.

Pour caractériser la complexité (le coût) de cet algorithme, on choisit d'étudier le nombre de comparaisons qu'il effectue.

Répondre à la question suivante :

QCM : Dans le meilleur des cas, que peut-on écrire de la complexité du tri par insertion ?

  • A : Elle est logarithmique (Θ(lg n) ), c'est à dire que la complexité évolue moins vite que le nombre n de données (par exemple : si on multiplie le nombres de données n par 100, le temps d'exécution n'est multiplié que par 8)
  • B : Elle est linéaire ( Θ(n) ), c'est à dire que la complexité évolue comme le nombre n de données (par exemple : si on multiplie le nombres de données n par 100, le temps d'exécution est multiplié par 100)
  • C : Elle est quadratique ( Θ(n2) ), c'est à dire que la complexité évolue comme le carré du nombre n de données (par exemple : si on multiplie le nombres de données n par 100, le temps d'exécution est multiplié par 10000, 100*100)
  • D : Elle est exponentielle ( Θ(xn) ), c'est à dire que la complexité évolue à terme beaucoup plus vite que n'importe quelle fonction polynomiale du nombre n de données (par exemple : si on multiplie le nombres de données n par 100, le temps d'exécution est multiplié par 2100, soit 1267650600228229401496703205376)

Index 00 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19
Elément 21 22 27 28 33 35 36 37 38 42 44 45 46 50 51 59 66 82 87 96

...CORRECTION...

On remarque sur l'animation qu'il faut 19 comparaisons pour finir l'algorithme de tri des 20 éléments.

Avec 1000 éléments, nous aurions 9999 comparaisons à faire.

Le nombre de comparaisons est donc une fonction f(n) telle que f(n) = n - 1

Pour les grandes valeurs de n, le 1 devient totalement négligeable.

On voit donc que la complexité dans le meilleur des cas est linéaire.

On répondra donc

  • B : Elle est linéaire ( Θ(n)), c'est à dire que la complexité évolue comme le nombre n de données (par exemple : si on multiplie le nombres de données n par 100, le temps d'exécution est multiplié par 100)

Regardons maintenant le pire des cas pour cet algorithme.

La boucle POUR ne pose pas de problème : dans tous les cas, on doit effecuter chacune de ses boucles.

C'est la boucle TANT QUE qui peut poser problème :

    TANT QUE j ≥ 0 et que tableau[j] > cle

      tableau[j+1]tableau[j]

      jj - 1

    Fin TANT QUE

Le TANT QUE possède deux conditions : si la clé est systématiquement plus petite que les éléments du sous-tableau, on va devoir lire un à un tous les éléments du sous-tableau. Jusqu'à atteindre l'élément d'index 0. C'est le cas le plus défavorable en terme de temps d'exécution.

Si on réflechit un peu, ce cas correspond à un tableau trié mais en sens inverse du sens voulu !

Voici un exemple du pire des cas :

Index 00 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19
Elément 96 87 82 66 58 51 50 46 45 44 42 38 37 36 35 33 28 27 22 21

Sur ce tableau de 20 éléments, la clé va prendre 19 positions successives, de l'index 1 jusqu'à l'index 19.

Sur un tableau de n éléments, la clé va prendre n-1 positions successives, de l'index 1 jusqu'à l'index n-1.

05° Utiliser l'animation pour répondre à ces questions : dans le pire des cas

  • combien de comparaisons à l'étape 1 (lorsque la clé est l'index 1)
  • combien de comparaisons à l'étape 2 (lorsque la clé est l'index 2)
  • combien de comparaisons à l'étape 3 (lorsque la clé est l'index 3)
  • combien de comparaisons à l'étape n-1 (lorsque la clé est l'index n-1)

...CORRECTION...

On voit qu'à l'étape 1, il y aura 1 comparaison à faire.

On voit qu'à l'étape 2, il y aura 2 comparaisons à faire.

On voit qu'à l'étape 3, il y aura 3 comparaisons à faire.

On voit qu'à l'étape n-1, il y aura n-1 comparaisons à faire.

Facile non ?

Du coup, dans le pire des cas, combien doit-on faire de comparaisons pour trier le tableau de n éléments.

Sur un tableau de n = 6 éléments, on devra donc calculer le nombre de comparaisons C6 en faisant la somme de 5 nombres :

C6 = 1 + 2 + 3 + 4 + 5

Sur un tableau de n éléments, on devra donc calculer le nombre Cn de comparaisons en faisant la somme de (n-1) éléments variant de 1 à (n-1) :

Cn = 1 + 2 + 3 + 4 + 5 + ... + (n-5) + (n-4) + (n-3) + (n-2) + (n-1)

La somme Cn est ce qu'on nomme une série.

Que vaut-elle ?

Le mathématicien / astronome / physicien allemand Gauss, surnommé le Prince des Mathématiciens, avait trouvé (en 1786, alors qu'il avait 9 ans dit-on) une méthode séduisante de résolution.

Portrait de Carl Friedrich Gauss
Portrait de Carl Friedrich Gauss, image libre de droit
Recherche d'une formule associée à notre série 1+2+3+4...+n-2 +n-1

Notre série Cn est la somme de (n-1) éléments :

Cn = 1 + 2 + 3 + 4 + ... + (n - 4) + (n - 3) + (n - 2) + (n - 1)

Nous voudrions associer les éléments deux par deux, mais il est possible qu'ils soient en nombre impair. Comment faire ? Multiplier chacun des membres par deux !

2 * Cn = 1 + 1 + 2 + 2 + 3 + 3 + 4 + 4 + ... + (n - 4) + (n - 4) + (n - 3) + (n - 3) + (n - 2) + (n - 2) + (n - 1) + (n - 1)

Du coup, le membre de droite comporte maintenant le double d'éléments, soit 2(n-1) éléments. Nous sommes certain qu'il y a un nombre pair d'éléments.

Associons alors les 2(n-1) éléments deux par deux, par complément du type 3 + (n - 3).

Cela nous permettra d'obtenir (n-1) couples.

2 * Cn = 1 + (n - 1) + 1 + (n - 1) + 2 + (n - 2) + 2 + (n - 2) + 3 + (n - 3) + 3 + (n - 3) + 4 + (n - 4) + 4 + (n - 4) + ...

2 * Cn = (1 + n - 1) + (1 + n - 1) + (2 + n - 2) + (2 + n - 2) + (3 + n - 3) + (3 + n - 3) + (4 + n - 4) + (4 + n - 4) + ...

Nous voyons donc que nous obtenons (n-1) couples qui valent tous n.

2 * Cn = (n) + (n) + (n) + (n) + (n) + (n) + (n) + (n) + ...

On peut donc écrire

2*Cn = (n-1)n

Au final, cela donne donc :

Formule de la série

Comme cette somme est aussi longue à écrire, on utilise parfois la notation ci-dessous qui veut dire exactement la même chose :

Formule de la série formule 1

06° Utiliser le programme Python ci-dessous pour vérifier que la formule est bien valide.

1 2 3 4 5 6 7 8 9 10 11 12 13
def somme(n) : '''Renvoie 1 + 2 + 3 + ... + n-1''' addition = 0 for x in range(n) : addition = addition + x return addition def formule(n) : '''Renvoie n(n-1)/2''' return n*(n-1)//2 for n in range(1,101,1) : print(f"Calcul direct : {somme(n)} contre Formule : {formule(n)}")

07° Nous venons de voir que le nombre de comparaisons nécessaires au tri d'un tableau de n éléments était ceci dans le pire des cas :

Formule de la série formule 1

Question : la complexité du tri par insertion est (dans le pire des cas) :

  • A : logarithmique (Θ(lg n) ), c'est à dire que la complexité évolue moins vite que le nombre n de données (par exemple : si on multiplie le nombres de données n par 100, le temps d'exécution n'est multiplié que par 8)
  • B : linéaire ( Θ(n) ), c'est à dire que la complexité évolue comme le nombre n de données (par exemple : si on multiplie le nombres de données n par 100, le temps d'exécution est multiplié par 100)
  • C : quadratique ( Θ(n2) ), c'est à dire que la complexité évolue comme le carré du nombre n de données (par exemple : si on multiplie le nombres de données n par 100, le temps d'exécution est multiplié par 10000, 100*100)
  • D : exponentielle ( Θ(xn) ), c'est à dire que la complexité évolue à terme beaucoup plus vite que n'importe quelle fonction polynomiale du nombre n de données (par exemple : si on multiplie le nombres de données n par 100, le temps d'exécution est multiplié par 2100, soit 1267650600228229401496703205376)

...CORRECTION...

Démonstration de la complexité du pire des cas

Quelques explications si ce n'est pas suffisant.

On cherche à voir uniquement le comportement global de cet algorithme lorsqu'on augmente les données qu'il doit traiter.

On va donc simplifier notre formule : le but est de savoir à quelle type de fonction se rapproche le coût de notre algorithme, pas la formule exacte de cette fonction (nous l'avons déjà !).

On omet donc d'abord les facteurs multiplicateurs ou diviseurs. Ici, le facteur 2.

Pourquoi ? Voyons un exemple : un algorithme a un coût en n2*5.

Cas 1 : on tient compte du facteur 5 pour nos comparaisons sur le même algorithme.

Pour n = 2 données, on obtient un coût de 2*2*5 = 20.

Pour n = 4 données, on obtient un coût de 4*4*5 = 80.

On voit donc que lorsqu'on double les données (on passe de 2 à 4), le coût est lui multiplié par 4 (on passe de 20 à 80).

Cas 2 : on ne tient pas compte du facteur 5 pour nos comparaisons sur le même algorithme.

Pour n = 2 données, on obtient un coût de 2*2 = 4.

Pour n = 4 données, on obtient un coût de 4*4 = 16.

On voit donc que lorsqu'on double les données (on passe de 2 à 4), le coût est lui multiplié par 4 (on passe de 4 à 16).

Conclusion : inutile de tenir compte des facteurs multiplicateurs lorsqu'il s'agit de trouver le comportement d'un même algorithme lorsqu'on change la taille de ses données.

Il nous reste donc (n-1)*n.

Pour les grands nombres, on peut omettre le -1 du n-1. En terme d'évolution globale, il n'y a pas vraiment de différence entre 1 milliard et 1 milliard moins 1...

On voit donc qu'on obtient n*n, soit n2.

Le coût est donc quadratique.

Complexité du tri par insertion

On retiendra donc que :

  • Dans le meilleur des cas, la complexité du tri par insertion est Θ(n) : le coût est linéaire.
  • Dans le pire des cas, la complexité du tri par insertion est Θ(n2) : le coût est quadratique.

Ce que nous ne verrons pas cette année est le cas moyen. Pour l'instant, on ne peut pas dire grand chose du cas moyen. Et on ne sait pas si le pire des cas arrive souvent, ou pas...

D'où la grande contribution des mathématiques à cette partie du programme.

Ceux qui ont pris la spécialité Math ont surement rencontré la notion de série.

Pour faire le lien avec cette autre spécialité (et ne pas vous demander pourquoi "c'est presque la même formule mais pas vraiment"), remarquez bien qu'ici notre série des comparaisons n'arrive qu'à n-1. La formule qui vous avez vu en math va jusqu'à n.

Voici ce que vous avez certainement rencontré en mathématiques ( et ça peut également servir à ceux qu'y n'ont pas cette spécialité) :

Série arithmétique des nombres de 1 à n

Formule de la série
Formule de la série formule 1'

Cela correspond bien à notre formule 1 avec un changement de variable n = n' -1.

Série arithmétique des carrés de 12 à n2

Formule de la série des carrés
Formule de la série des carrés formule 2

Série arithmétique des cubes de 13 à n3

Formule de la série des cubes
Formule de la série des cubes formule 3

Série géométrique (un exemple avec x différent de 0)

Formule de la série géométrique de l'exemple
Formule de la série des cubes formule 4

4 - Preuve de correction

Nous avons donc démontré

  • la terminaison du tri par insertion : nous sommes maintenant certain qu'il va s'arrêter pourvu qu'on lui en laisse le temps
  • le coût quadratique dans le pire des cas : nous savons que si on multiplie la taille des données par 10, le temps d'exécution va approximativement être multiplié par 100.

Oui mais... Est-ce que notre algorithme marche à chaque fois. Après tout, nous avons fait quelques essais, rajouté quelques doctests. Mais il y a peut-être des cas (même rares) qui risquent de créer un raté. Non ?

Imaginez : vous avez la responsabilité d'un grand nombre de vie en travaillant sur un algorithme de pilotage automatique. L'un des processus que vous avez créé utilise un tri par insertion. S'il disfonctionne, c'est la perte de contrôle de l'appareil. Vous avez fait des tests. Vous savez que ça marche. Mais... Laisseriez-vous l'appareil décoller sans être certain que ça fonctionne toujours ?

Tests

Nous avons vu qu'on peut vérifier automatiquement qu'une fonction fournit pas les réponses attendues sur un ensemble de de tests. Le nom générique de ces tests est tests unitaires. Nous avons utilisé pour l'instant une version simplifiée de ces systèmes avec le doctest de Python.

A toujours avoir en tête : on ne peut pas prouver la correction d'un algorithme (et de la fonction programmée correspondante) en réalisant juste un très grand nombre de tests : nous ne parviendrions qu'à prouver que l'algortihme fonctionne dans tous les cas testés.

Cela n'est pas équivalent à affirmer qu'il est réellement correct dans tous les cas.

Attention, tous les cas veut dire : tous les cas dont les entrées vérifient bien les spécifications d'entrée.

Nous allons donc maintenant voir qu'on peut fournir la preuve de correction d'un algorithme : on peut démontrer mathématiquement qu'il renvoie une réponse correcte ou réalise l'action attendue dans tous les cas. Cela revient à dire que l'algorithme est juste.

Remarque spécial confinement : aucune question à rédiger, toutes les réponses sont fournies car c'est plutôt une partie à suivre en cours et à comprendre. A l'oral ça passe bien. J'ai fait ce que j'ai pu pour fournir toutes les explications écrites. N'hésitez à m'envoyer des questions ou à participer au live.

Preuve de correction et invariant

Pour prouver que l'algorithme est correct, nous allons devoir trouver un invariant : il s'agit du nom qu'on donne à une propriété vérifiable et qui permettra de prouver que le résultat final après exécution est bien le résultat attendu.

La démonstration se fait en trois temps.

L'initialisation

On montre que l'invariant est vrai avant le passage dans une boucle.

Si on note la propriété invariante P, on montre donc que P0 est vraie.

Le plus souvent, cette partie est triviale. Mais pas toujours...

La conservation

On montre que l'invariant reste vrai après chaque passage dans une boucle.

Cela revient à montrer que si l'invariant est vrai avec k (Pk), il reste vrai avec un tour de boucle en plus avec k+1 (Pk+1) :

Pk Pk+1

La terminaison

On exploite les deux phases précédentes pour montrer qu'une fois toutes les boucles effectuées, l'invariant reste vrai et que l'algorithme a bien répondu à son objectif en s'arrêtant losqu'il a traité toutes les données.

Le problème est qu'il n'existe pas de méthode automatique pour trouver le bon invariant. Il faut chercher à chaque nouveau problème qui se pose...

Regardons le cas du tri par insertion.

Le principe est simple : on décompose le problème en un sous-tableau trié et un sous-tableau non-trié.

On amène un élément à la fois du sous-tableau non trié vers le sous-tableau trié. Et on le place au bon endroit.

Invariant du tri par insertion

Initialement, le sous-tableau trié ne contient qu'une valeur. A chaque tour de boucle, on va rajouter un élément à ce sous-tableau.

On considère que notre invariant pourrait être la propriété Pk suivante  : après k tours de boucle, k+1 éléments sont triés dans le sous-tableau [0;k] de gauche.

Dans le sous-tableau trié (par ordre croissant ici), on doit donc avoir tableau[x] < tableau[x+1].

08° Travaillons sur l'initialisation.

Avant de rentrer dans la boucle (k=0), notre sous-tableau trié ne contient que la première valeur.

Peut-on considérer que l'invariant Pk est vérifié pour k = 0 ?

...CORRECTION...

On peut sans peine se convaincre qu'un sous-tableau ne contenant qu'un élément unique est bien trié.

La propriété P0 est donc vérifiée.

On peut donc dire que l'invariant est vrai avant l'exécution de la première boucle FOR.

Passons maintenant à la conservation. Pour rappel, voici l'algorithme :

Algorithme du tri par insertion

    POUR i variant de 1 à (longueur - 1)

      cletableau[i]

      ji - 1

      TANT QUE j ≥ 0 et que tableau[j] > cle

        tableau[j+1]tableau[j]

        jj - 1

      Fin TANT QUE

      tableau[j+1]cle

    Fin POUR

    Renvoyer VIDE (∅)

09° Quelle va être la première valeur prise par i lors du premier tour de boucle ? Que vaut j avant de rentrer dans le TANT QUE ?

Quelle est la relation entre le nombre de tours de boucle k et la valeur de la variable de boucle i ?

...CORRECTION...

    POUR i variant de 1 à (longueur - 1)

Lors du premier tour, i vaut donc 1 et j vaut 0 puisqu'on retire un.

On voit donc qu'on peut écrire k = i.

Considérons que la propriété Pk est vrai : à la fin des k tours de boucle, le sous-tableau [0;k] est trié et contient donc k+1 éléments. i vaut k lors du dernier tour.

Au tout début du tour de boucle suivant, on dispose donc d'un sous-tableau [0;k] trié mais i augmente est vaut maintenant k+1.

Cas étudié n°1 : la clé d'index i = k+1 est inférieure à tous les éléments du sous-tableau trié [0 ; k]. Le sous-tableau [k+1 ; n-1] est non-trié à priori.

Exemple : [10, 20, 30, 40, 5, 70, 60, 80]

Sur ce cas, on travaillera lors de cette boucle sur [10, 20, 30, 40, 5] puisqu'on rajoutera la valeur non triée suivante, celle d'index k+1.

10° Regarder l'algorithme. Que va-t-il faire des éléments du sous-tableau trié [0; k] si la clé d'index k+1 (le 5 en rouge ici) est plus petite que les valeurs du sous-tableau trié ? Les éléments [0; k] étant initialement triés, est-il possible qu'ils ne soient plus triés entre eux après ce traitement ?

...CORRECTION...

La lecture du TANT QUE permet de voir qu'on décale alors juste tous les éléments d'une case vers la droite.

Comme on les décale tous d'une case uniquement, cela ne change rien à leur ordre relatif : ils restent triés entre eux.

On pourra encore écrire tableau[x] < tableau[x+1]

11° On considère encore le cas d'une clé d'index k+1 inférieure à tous les éléments du sous-tableau [0;k]. Quelle va être la valeur de j en sortant du TANT QUE ? A quel index va alors être stockée la clé ? Puisque les anciens éléments en [0;k] ont été déplacé en [1;k+1] qu'est-ce qui permet d'affirmer que le sous-tableau [0; k+1] est bien trié à la fin de cette nouvelle boucle ?

...CORRECTION...

On va modifier j jusqu'à ne plus respecter la condition j ≥ 0 du TANT QUE.

Puisqu'on décroit de un, on sortira lorsque j vaudra -1.

Le placement de la clé se faisant avec tableau[j+1]cle, on voit qu'on placera la clé à l'index 0.

Nous avons montré que les anciens éléments triés par ordre croissant [0;k] avaient été déplacés en [1;k+1].

La clé (plus petite que tous les autres éléments) vient d'être placée en index 0.

On peut donc écrire que le tableau [0;k+1] est maintenant trié en ordre croissant.

Nous venons donc de montrer que sur le cas particulier d'une clé inférieure à tous les éléments, Pk implique bien Pk+1 après un tour de boucle en plus.

Cas étudié n°2 : la clé d'index k+1 est supérieure à tous les éléments du sous-tableau trié [0 ; k]. Le sous-tableau [k+1 ; n-1] est le sous-tableau des éléments non-triés.

Exemple : [10, 20, 30, 40, 50, 70, 60, 80]

Sur ce cas, on travaillera alors sur [10, 20, 30, 40, 50] par exemple.

12° Sur le même principe de raisonnement que les questions précédentes, montrer la conservation de la propriété sous-tableau trié si la clé d'index k+1 est supérieure à tous les éléments du sous-tableau [0, k].

...CORRECTION...

C'est encore plus simple :

On ne rentre même pas dans le TANT QUE puisque l'une des condition n'est pas bonne  :

TANT QUE j ≥ 0 et que tableau[j] > cle

Si j vaut i-1 mais qu'on place la clé avec tableau[j+1]cle, on voit qu'on laisse la clé au même index i.

Le sous-tableau [0, k] était trié et on ne le transforme pas.

On rajoute un élément plus grand que les autres à l'index k+1.

On obtient donc bien un sous-tableau [0; k+1] trié après application d'un tour de boucle POUR supplémentaire.

Nous venons donc de montrer que sur le cas particulier d'une clé supérieure à tous les éléments du sous-tableau trié, Pk implique bien Pk+1 après un tour de boucle en plus.

Il reste à expliquer ce que se passe lorsque la clé est inférieure à certains éléments à sa gauche, mais pas tous.

Cas étudié n°3 : la clé d'index k+1 est inférieure à certains éléments du sous-tableau trié [0 ; k]. Le sous-tableau [k+1 ; n-1] est le sous-tableau des éléments non-triés.

Exemple : [10, 20, 30, 40, 25, 70, 60, 80]

Sur cet cas, on travaillera alors sur [10, 20, 30, 40, 25] par exemple.

Revoici l'algorithme.

    POUR i variant de 1 à (longueur - 1)

      cletableau[i]

      ji - 1

      TANT QUE j ≥ 0 et que tableau[j] > cle

        tableau[j+1]tableau[j]

        jj - 1

      Fin TANT QUE

      tableau[j+1]cle

    Fin POUR

    Renvoyer VIDE (∅)

13° On considère que

  • Tous les éléments d'index [m; k] sont supérieurs à la clé.
  • Tous les éléments d'index [0; m-1] sont inférieurs ou égaux à la clé.

Questions

  • Quels sont les éléments du sous-tableau [0, k] qui auront bougés une fois sorti du TANT QUE ?
  • Ces éléments sont-ils encore triés ?

...CORRECTION...

Le sous-tableau va être divisé en deux parties : les éléments qui n'auront pas bougé et les éléments qui auront bougé.

Regardons d'abord la partie qui a bougé.

TANT QUE j ≥ 0 et que tableau[j] > cle

La seconde condition ne sera vraie que jusqu'à tableau[m] > cle.

On va donc déplacer d'une case à droite les éléments [m; k] qui vont se retrouver en [m+1; k+1].

Le sous-tableau [0;m-1] ne sera lui pas modifié.

Comme les éléments sont tous décalés d'une case, on garde leur tri relatif.

14° A quel index va alors être placée la clé ?

Peut-on encore dire que le sous-tableau [0; k] est trié, sachant que :

  • Le sous-tableau [0; m-1] est toujours trié et ses éléments inférieurs ou égaux à la clé.
  • Le sous-tableau [m+1;k+1] est toujours trié et ses éléments supérieurs ou égaux à la clé.

...CORRECTION...

tableau[j+1]cle

Puisque j contient m-1, on va placer la clé à l'index m-1+1, soit m.

  • Le sous-tableau [0; m-1] est trié et inférieur ou égal à la clé.
  • La clé est à l'index m.
  • Le sous-tableau [m+1;k+1] est trié et supérieur ou égal à la clé.

Nous pouvons donc affirmer que le sous-tableau [0; k] est bien trié après avoir appliqué la boucle POUR avec i = k.

Nous avons fait les trois cas possibles pour la comparaison de la clé d'index k+1 par rapport aux éléments du sous-tableau [0;k].

Dans les trois cas, nous avons pu affirmer que :

  • si le sous-tableau [0; k] est bien trié
  • le sous-tableau [0; k+1] est trié après avoir appliqué un nouveau tour de boucle avec i = k+1

Nous avons donc montré la conservation de l'invariant : Pk Pk+1

La dernière étape est ici assez rapide :

Terminaison

Nous avons montré que k correspondait à la valeur de la variable de boucle i sur cet algorithme de tri : k = i (1)

En regardant la boucle, on voit que i vaut longueur - 1 (2) lors du dernier tour de boucle.

On en déduit avec (1) + (2) que k vaut longueur - 1 également.

Or Pk est la propriété selon laquelle le sous-tableau trié contient k+1 élément.

On en déduit donc qu'à la fin du dernier tour de boucle, le sous-tableau trié contient k + 1 élements, soit longueur - 1 + 1. Et ça tombe bien : le sous-tableau trié contient donc longueur éléments. Soit tout le tableau ! Nous avons donc montré que l'algorithme agissait bien sur toutes les données.

Les réflexions ci-dessus permettent donc de prouver la correction de l'algorithme du tri par insertion.

Cet algorithme fonctionne donc dans tous les cas valides, c'est à dire tous les cas où l'ENTREE (le tableau) respecte bien les préconditions fournies.

5 - Exemple avec Python

Pour finir, nous allons montrer comment faire planter un programme si on ne respecte pas une condition qui devrait être respectée !

C'est le principe de la programmation défensive : on ne donne pas simplement les préconditions, on empêche la fonction d'agir si les préconditions ne sont pas correctes.

✎ 15° Utiliser le programme ci-dessous.

Quelle est la valeur maximale qu'on veut imposer à a et b ?

1 2 3 4 5 6 7
def addition(a, b) : '''Additionne a et b pourvu que a et b ne soient pas strictement supérieure à 10 :: param a(int) : un nombre entre 0 et 10 :: param b(int) : un nombre entre 0 et 10 :: return (int) : la somme de a et b ''' return a + b

Que donnent les instructions suivantes ? Est-ce un problème de ne pas respecter les préconditions sur a et b ?

>>> addition(5,10) >>> addition(5,25)

Comme vous l'avez vu, les préconditions ne sont ici que de la documentation. Si la personne qui utilise la fonction ne veut pas la respecter, elle peut le faire.

Oui mais... si l'addition vise à créer une note sur 20 à partir de deux notes sur 10. Ca va renvoyer n'importe quoi.

Et bien, nous pourrions faire "planter" le programme en créant une exception si les valeurs de a et b ne sont pas bonnes.

Pour cela, nous allons créer des assertions, c'est à dire des expressions qui devraient être évaluées à True.

Si ce n'est pas le cas, ça stoppe le programme en lançant une exception et affiche le message d'erreur voulu par l'utilisateur.

✎ 16° Utiliser le programme ci-dessous.

Quelle est la valeur maximale qu'on veut imposer à a et b ?

1 2 3 4 5 6 7 8 9
def addition2(a, b) : '''Additionne a et b pourvu que a et b ne soient pas strictement supérieure à 10 :: param a(int) : un nombre entre 0 et 10 :: param b(int) : un nombre entre 0 et 10 :: return (int) : la somme de a et b ''' assert a <= 10, "a est trop grand ! On avait dit 10 au maximum dans la documentation !" assert b <= 10, "b est trop grand ! On avait dit 10 au maximum dans la documentation !" return a + b

Que donnent les instructions suivantes ? Est-ce un problème de ne pas respecter les préconditions sur a et b ?

>>> addition2(5,10) >>> addition2(5,25)

Cette fois, la seconde addition a provoqué un message d'erreur à cause du non-respect de l'assertion. Un truc du genre :

assert b <= 10, "b est trop grand ! On avait dit 10 au maximum dans la documentation !" AssertionError: b est trop grand ! On avait dit 10 au maximum dans la documentation !

Vu comme ça, ça à l'air un peu bête de faire planter volontairement son programme. Deux raisons d'utilser néanmoins des assertions :

  • Vous êtes en debugage : le code n'est pas en production (destiné aux utilisateurs finaux) et vous voulez savoir ce qui fonctionne ou pas.
  • On peut intercepter les exceptions et simplement créer par exemple un fichier log contenant toutes les erreurs rencontrées en cours d'utilisation.

Aujourd'hui, nous allons simplement finir en utilisant ces assertions pour vérifier que notre invariant est bien un invariant sur quelques exemples.

Comme l'invariant est la propriété d'un sous-tableau d'être trié, nous allons créer une fonction est_trie qui vérifie cela.

On remarque bien la présence, ligne 25, d'une assertion à la fin de la boucle POUR de façon à vérifier si l'invariant est toujours vérifié.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
def tri_par_insertion(tableau) : '''Tri en ordre croissant le tableau en utilisation le tri par insertion :: param tableau(list) :: un tableau d'éléments de même type :: return (None) :: procédure (renvoie donc None en Python) .. Effet de bord :: modifie le tableau en permutant les éléments :: precondition :: tableau doit contenir au moins deux éléments :: precondition :: les éléments de tableau doivent pouvoir être comparés entre eux :: exemple :: >>> numeros = [5, 8, 1, 20, 15] >>> tri_par_insertion(numeros) >>> numeros [1, 5, 8, 15, 20] ''' for i in range(1, len(tableau)) : cle = tableau[i] j = i - 1 # On commence par l'élément juste à gauche de la clé while j >= 0 and tableau[j] > cle : tableau[j+1] = tableau[j] # On décale l'élément vers la droite j = j - 1 # On passe à l'élément encore à gauche tableau[j+1] = cle assert est_trie(tableau, i), "L'invariant n'est pas vérifié : le sous-tableau n'est pas trié" def est_trie(tableau,k) : '''Renvoie True si le sous-tableau [0;k] est trié dans l'ordre croissant''' if len(tableau) < 2 : return True for index in range(k) : if tableau[index] > tableau[index+1] : return False return True if __name__ == '__main__' : import doctest doctest.testmod()

17° Testons la fonction est_trie : elle renvoie True si le tableau est bien trié par ordre croissant de l'index 0 à l'index k inclus.

>>> est_trie([10,20,30,40],2) >>> est_trie([10,20,40,30],2) >>> est_trie([20,10,30,40],2)

...CORRECTION...

A chaque fois, on transmet un index 2. Cela veut dire qu'on observe les index 0, 1 et 2, soit les trois premiers nombres.

>>> est_trie([10,20,30,40],2) True >>> est_trie([10,20,40,30],2) True >>> est_trie([20,10,30,40],2) False

18° Tester l'assertion à l'aide de la commande suivante. Si l'invariant est toujours vraie, vous n'aurez jamais d'erreur !

>>> import random >>> donnees = [random.randint(1,1000) for x in range(100)] >>> tri_par_insertion(donnees)

Mais attention, ce n'est pas une démonstration. Ici, on montre que ça fonctionne parfois. La vraie démonstration a été faite dans la partie précédente.

En utilisant les flèches HAUT et BAS de votre clavier, vous pouvez retrouver les anciennes instructions pour les exécuter plusieurs fois.

Ca devrait marcher à tous les cas : l'invariant "le sous-tableau [0;i] est trié" est un vrai invariant.

19° Si on considère le pire des cas, quel devrait être le rapport entre le temps d'exécution du tri par insertion avec 1000 éléments et 10000 éléments ?

Et dans le meilleur des cas ?

...CORRECTION...

Nous avions vu que le coût dans le pire des cas était quadratique (en n2).

Si on multiplie la taille des données par 10 en passant de 1000 à 10000, nous allons donc multiplier le temps d'exécution théorique par 100.

Dans le meilleur des cas, le coût était linéaire. Si on multiplie la taille des données par 10, on multiplie le temps d'exécution théorique par 10.

✎ 20° Si on considère le pire des cas, quel devrait être le rapport entre le temps d'exécution du tri par insertion avec 1000 éléments et 4000 éléments ?

Et dans le meilleur des cas ?

6 - FAQ

Pourquoi justifiez la terminaison d'une boucle FOR ?

Un peu pour l'exercice. Il existe deux cas où une boucle POUR peut mal tourner :

  • On demande par exemple de commencer à 1, de s'arrêter à 10 et de décrémenter de 1 à chaque tour. Ca donne 1, 0, -1 ... et ça ne s'arrêtera jamais...
  • On touche à la variable de boucle dans la boucle.

Ici, vous n'avez ni l'un ni l'autre mais ça vous permettra de vous souvenir qu'il faut un peu surveiller les boucles POUR quand même.

Activité publiée le 07 05 2020
Dernière modification : 07 05 2020
Auteur : ows. h.