Cours 6 du 13 mars

 

Boucles et invariants, applications aux tris

(Suite)

(a) Invariants (suite)

Exemple :

 

    // INVARIANTS

    // exemple d'invariant:

    // s contient la somme des élément de l à i-1

    static int somme(int[]t,int l, int r){

        int s=0;

        int i=r;    

        while(i<=r){

           s+=t[i];

           i+=1;

        }

        return s;

    }

 

Au début de chaque itération on a : 

s contient la somme des éléments du tableau de l jusqu'à i-1 (I):

 

On montre ainsi que le programme calcule la somme des éléments de l à r du tableau t.

 

Ce procédé consiste donc à trouver un invariant pour la boucle et à partir de là de vérifier que le programme calcule bien ce qu'il doit. En fait, quand on a écrit la boucle en question ce que l'on a fait c'est très exactement déterminer un invariant de boucle (même si ce processus n'était pas formalisé en tant que tel!).

 

Plus généralement, on peut spécifier un programme par {Pre} Prog {Post}Pre est une précondition, Post une Postcondition. et Prog une morceau de programme. Cette spécification s'interprète comme suit:

Si avant d'exécuter Prog, la condition Pre est vraie alors après l'exécution de Prog la condition Post est vraie.

 

Dans l'exemple précédent, on aurait pu écrire:

{0<=l<=r<t.length} programme {s est la somme des éléments de t pour tous les indices dans [r,l]}

 

Il faut noter que le choix de Pre et de Prog n'est pas unique on a par exemple:

 

On peut étudier pour chaque construction du programme (affectation, conditionnelle, boucle etc.) quelle en est l'effet pour les pré et post-conditions. Nous ne le ferons pas ici de façon exhaustive et on ne s'intéressera qu'aux boucles (en se restreignant à des boucles « while » simples).

 

Pour une boucle on a:

si :

{I et b} Prog {I}

alors

{I} while (b) Prog {I et non b}

 

En clair, {I et b} Prog {I} signifie que I est un invariant pour la boucle: si I est vraie avant l'itération, si la condition de l'itération est vraie, alors après une itération I reste vraie. Si I est un invariant alors, quand la boucle termine, I et  la négation de la condition de boucle (non b) sont vraies.

On notera que l’on suppose ici que la boucle termine: plus précisément la propriété précédente est si la boucle termine alors {I} while (b) Prog {I et non b}. La terminaison de la boucle doit être traitée à part.

 

Il n'y a pas bien sûr un seul invariant possible pour une boucle (par exemple la propriété est toujours vraie (TRUE) est toujours un invariant!), il s'agit de déterminer un invariant qui correspond à ce que l'on veut obtenir comme couple précondition et postcondition.

 

R1:

Si l'on veut vérifier:

{Pre} Programme {Post}

Programme est de la forme :

while (b) Prog.

On peut procéder comme suit:

 

  1. trouver un invariant I pour la boucle while (b) Prog : (c'est-à-dire que tel que {I et b} Prog {I})
  2. I doit en plus vérifier :
  3. Pre => I (la précondition doit être suffisamment forte pour assurer I)
  4. (I et non b) => Post (ce qui est assurée à la sortie de la boucle doit être suffisant pour assurer la postcondition
  5. Vérifier que la boucle termine.

 

Remarques :

 

(b) application à quelques tris

(a) tri par sélection et tri-bulle

Supposons que l'on veuille trier un tableau tab entre les indices l et r. On peut considérer l'invariant:[1]

(I1) tab[l,i[  est trié  : pour tout a,b  dans [l,i[ a<b => tab[a] ≤ tab[b]

 

 

Si donc on arrive à construire une boucle telle que (I1) soit un invariant, par la règle R1, on aura un programme qui trie le tableau tab entre les indices r et l.

 

Pour cela on peut renforcer (I1) en considérant (I1 et I2)  où I2 assure que tous les éléments du tableau entre i et r sont supérieurs ou égaux à tous les éléments de tab entre l et i:

(I2) pour tout a dans [i,r] pour tout b dans [l,i[ tab[b] ≤ tab[a]

 

Pour assurer l'invariant (I1 et I2) il suffit de déterminer l'élément minimal de tab entre i et r, et de l'échanger avec tab[i]: ainsi (I1 et I2) seront assurées jusqu'à l'indice i+1.

 

Plus précisément:

 

si x=Min(tab,i,j):

1.      x appartient à [i,j]

2. pour tout k dans [i,j] tab[x] ≤ tab[k]

 

{tab[i]=x et tab[j]=y} echanger(tab,i,j) {tab[i]=y et tab[j]=x et aucun autre élément de tab n'a changé}

 

Le programme sera:

          int i=l;

          while(i<=r) {

              int min=Min(tab,i,r);

              echanger(tab,i,min);

              i=i+1;   

        }

 

On peut vérifier que (I1 et I2) est bien un invariant de la boucle:

 

Maintenant si on suppose que tab est bien défini pour toutes les valeurs d'indice de [l,r], on  a  après exécution de int i=l; la propriété i=l qui est vraie. Comme dans ce cas [l,i[ est vide I1 et I2 sont trivialement vérifiés.

 

Ensuite (I1 et I2 et i>r) entraîne ici (I1 et i=r) et donc que le tableau est trié pour les valeurs de [l,r].

 

Enfin, la boucle termine toujours puisqu'il y aura au plus l-r itérations.

 

Il reste à écrire les codes correspondant à Min(tab,i,j) et echanger(tab,i,min):

             int min=i;

     for(int k=i+1;k<=j;k++)

         if(tab[k]<tab[min])min=j;

On a:

       {le tableau tab est défini pour les valeurs d'indices dans [i,j]}

             int min=i;

     for(int j=i+1;j<=r;j++)

         if(tab[k]<tab[min])min=k;

        {k=Min(tab,i,j)}

(Exercice donner un invariant pour cette boucle!)

 

int tmp=tab[i];

tab[i]=tab[min];

tab[min]=tmp;

 

 

 

Le programme complet (après remplacement de la boucle while par une boucle for) devient:

     public static void triselection(int[] tab,int l,int r){

        for(int i=l;i<=r;i++){

            int min=i;

            for(int j=i+1;j<=r;j++)

                if(tab[j]<tab[min])min=j;

            int tmp=tab[i];

            tab[i]=tab[min];

            tab[min]=tmp;

        }

    }

 

Il s’agit du tri par sélection.

 

On peut aussi, au lieu de chercher l’indice du minimum de tab[i…j] (en notant tab[i…j] la partie du tableau tab entre les indices i et j)et ensuite échanger avec tab[i], directement placer ce minimum dans tab[i] par des échanges successifs. La boucle suivante mettra dans t[i] du tableau t[i,r]. Plus précisément, le programme suivant assure la précondition TAB[i,r]=tab[i,r]   et la postcondtion: tab[i]=Min{TAB[j]| i <= j <=r} et tab[i,r] est une permutation de TAB[i,r] :

/* Pre : TAB[i,r]=tab[i,r]*/

for(int j=r;j>i;j--)

      if(t[j]<t[j-1])echange(t,j-1,j);

     /* Post : tab[i]=Min{TAB[j]| i <= j <=r} et tab[i,r] est une permutation de TAB[i,r]

    

Exercice:   Trouver un invariant de la boucle.

 

     Il est ensuite facile de vérifier que cette boucle assurera (I1 et I2) dans le programme (tri bulle) :

 

    public static void tribulle(int[]t, int l,int r){

        for(int i=l;i<=r;i++)

            for(int j=r;j>i;j--)

                if(t[j]<t[j-1])echange(t,j-1,j);

    }

 

Remarque :

Si TAB[l,r]est le tableau tab[l,r] trié, on peut remarquer que dans les deux tris précédents on a l’invariant : tab[l,i-1]=TAB[l,i-1]qui signifie que les éléments sélectionnés pour être déplacés sont mis à leur place définitive.

 

(b) Tri par insertion

Le tri par insertion on ne fait que maintenir (I1) et dans le tableau partiellement trié tab[l,i-1] les éléments ne sont pas à leur place définitive. Pour cela à chaque itération il insère tab[i] dans tab[l,i] à sa bonne place (c’est-à-dire de façon à ce que tab[l,i] reste trié).

 

    // tri par insertion

    // invariant de la boucle

    // t est trié sur [l,i[

    // l'élement t[i] est inséré à sa bonne place pour maintenir l’invariant

    public static void triinsertion(int t[],int l,int r){

        int i;

        for(i=l;i<=r;i++)

            for(int j=i;j>l;j--)

                if(t[j]<t[j-1])echange(t,j-1,j);

    }

 

On peut ensuite améliorer (un peu) cet algorithme :

    // version améliorée: une sentinelle évite le test de débordement

    // les échanges s'arrêtent dès que l'élément à insérer est à sa place

    // simplification des échanges

    public static void triinsertionbis(int []t,int l, int r){

        int i;

        for(i=r;i>l;i--)if(t[i]<t[i-1])echange(t,i-1,i);

        for(i=l+2;i <=r;i++){

            int j=i; int tmp=t[i];

            while(tmp<t[j-1]){

                t[j]=t[j-1];j--;

            }

            t[j]=tmp;

        }

    }

 

 

 

Complexité du tri par sélection

Rappelons le tri par sélection :

 

     public static void triselection(int[] tab,int l,int r){

        for(int i=l;i<=r;i++){

            int min=i;

            for(int j=i+1;j<=r;j++)

                if(tab[j]<tab[min])min=j;

            int tmp=tab[i];

            tab[i]=tab[min];

            tab[min]=tmp;

        }

    }

 

Remarquons d’abord que dans tous les cas le nombre d’itérations est le même : le pire cas , le meilleur cas et aussi le cas moyen sont donc tous égaux en ce qui concerne le nombre de comparaisons.

 

Soit  à l’itération  la boucle interne fait  itérations le nombre de comparaisons est donc :

Le nombre de comparaison est donc pour le meilleur, le pire cas et le ca moyen  c’est donc un .

Si l’on veut compter le nombre de déplacements, à chaque itération  de la boucle centrale 2 cases du tableau sont modifiées, on fait donc  écritures.

 

Complexité du tri par insertion

Rappelons le tri par insertion :

 

    // tri par insertion

    // invariant de la boucle

    // t est trié sur [l,i[

    // l'élement t[i] est inséré à sa bonne place

    public static void triinsertion(int t[],int l,int r){

        int i;

        for(i=l;i<=r;i++)

            for(int j=i;j>l;j--)

                if(t[j]<t[j-1])echange(t,j-1,j);

    }

 

Dans la boucle interne, on remonte toujours jusqu’au début du tableau alors que comme le tableau est déjà trié si le test n’est pas vrai on peut arrêter l’iétération, on obtient alors (le programme peut être amélioré !) :

 

    // tri par insertion

    // invariant de la boucle

    // t est trié sur [l,i[

    // l'élement t[i] est inséré à sa bonne place

    public static void triinsertion(int t[],int l,int r){

        int i;

        for(i=l;i<=r;i++)

            for(int j=i;j>l;j--)

                if(t[j]<t[j-1])echange(t,j-1,j) ;

                     else break;

    }

 

Dans le pire cas, on  remonte dans la boucle interne jusqu’au début du tableau (exercice trouver une entrée correspondant  au pire cas) et on aura dans ce cas comme dans le cas précédent   « tours » de boucle et donc le même nombre de comparaisons.

 

Dans le meilleur cas, le tableau est trié et on sort immédiatement de la boucle interne ce qui correspond à  comparaisons.

 

Pour le cas moyen, intuitivement, quand on veut insérer le -ème élément, on peut être amené à remonter de  positions en moyenne et donc faire   comparaisons, le nombre de comparaison sera donc en moyenne  mais c’est aussi un .

 

 

On peut améliorer le programme (comme on peut le vérifier cela ne change pas l’ordre de grandeur de la complexité) :

    // version améliorée: une sentinelle évite le test de débordement

    // les échanges s'arrêtent dès que l'élément à insérer est à sa place

    // simplification des échanges

    public static void triinsertionbis(int []t,int l, int r){

        int i;

        for(i=r;i>l;i--)if(t[i]<t[i-1])echange(t,i-1,i);

        for(i=l+2;i <=r;i++){

            int j=i; int tmp=t[i];

            while(tmp<t[j-1]){

                t[j]=t[j-1];j--;

            }

            t[j]=tmp;

        }

    }

Complexité du tri bulle

 

    public static void tribulle(int[]t, int l,int r){

        for(int i=l;i<=r;i++)

            for(int j=r;j>i;j--)

                if(t[j]<t[j-1])echange(t,j-1,j);

    }

 

Ce tri fera  comparaisons dans le pire cas, le meilleur cas et dans le cas moyen.

 

Comme on le voit tous les tris que l’on a vus jusqu’ici sont en . On verra dans les chapitres des tris plus rapides qui peuvent être en

 



[1] Il faut aussi ajouter que le tableau reste une permutation du tableau initial : cette partie de l’invariant est implicite.