Exemple :
// INVARIANTS
// exemple
d'invariant:
// r contient la somme
des élément de r à l-1
static int
somme(int[]t,int r, int l){
int s=0;
int i=r;
while(i<=l){
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 r jusqu'à i-1 (I):
On montre ainsi que le programme calcule la somme des éléments de r à l 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} où 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,
Dans l'exemple précédent, on aurait pu écrire:
{0<=r<=l<t.length} programme {s est la somme des éléments de t pour tous les indices dans [l,r]}
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}
où Programme
est de la forme :
while (b) Prog.
On peut procéder
comme suit:
Remarques :
Supposons que l'on veuille trier un tableau tab entre les indices r et l. On peut considérer l'invariant:[1]
(I1) tab[r,i[ est
trié : pour tout a,b dans [r,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 l sont supérieurs ou égaux à tous les éléments de tab entre l et i:
(I2) pour tout a dans [i,l] 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 l, 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,j);
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 j=i+1;j<=r;j++)
if(tab[j]<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[j]<tab[min])min=j;
{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] 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 sont mis à leur place définitive.
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;
}
}
[1] Il faut aussi ajouter que le tableau reste une permutation du tableau initial : cette partie de l’invariant est implicite.