Etude du fonctionnment d'un programme

- Démonstration d'un programme.
- Étude des Algorithmes : TRI - les boucles - le traitement conditionnelle.
    
    
1 Étude du fonctionnement d’un programme

1.1 "Démontrer" qu'un programme a l'effet souhaité 

Pour démontrer qu’un programme à l’effet souhaité, on peut :

  
  • Ajouter des " assertions" valables à différents points du programme, certaines évidentes et d’autres des conséquences de celles déjà connues, etc.
  • Vérifier que les conditions désirées sur le résultat du programme sont aussi des conséquences de certaines assertions.
  
Pour une suite d'instructions sans boucles c'est simple, même avec instructions conditionnelles, ...

1.1.1 Exemple: échanger deux variables 
 
Soit le code t:=x; x:=y; y:=t;
  
On peut fractionner le fonctionnement du programme de la manière suivante :
 
  • Au début x=x0  et  y=y0
  • après la première affectation: t=x0  et  y=y0
  • et la deuxième: t=x0  et  x=y0
  • et à la fin: y=x0  et  x=y0
 
Règle de déduction : après l'affectation x:=E, assertion A(x) est vraie si A(E) était vraie avant
 
1.1.2 Exemple: échange conditionnelle 
   
Soit le code si x>y alors début t:=x; x:=y; y:=t;fin
  
On peut en déduire le déroulement suivant :
 
  • après le début on a une nouvelle assertion garantie vraie: x > y
  • d'où on peut déduire que avant le fin on a y > x
  • implicitement sinon ; ne rien faire
  • après le sinon on a x < =y 
  
Donc x < =y est vrai à la fin de chaque branche et x < =y est vrai à la fin de l'instruction conditionnelle.

1.1.3 Les boucles 
   
Pour vérifier le bon fonctionnement des boucles, il faut prévoir et vérifier :
  
  • Un ensemble d'assertions connues avant la boucle (la précondition)
  • Un ensemble d'assertions souhaitées après la boucle (la postcondition)
  • Ajouter d'autres assertions vraies à chaque itération 
  
L'astuce est de trouver les bonnes nouvelles assertions

1.2 Démontrer qu'une condition est vraie après une boucle 
  
Prendre l'exemple d'une boucle :
  
tant que ExpressionBooleenne faire
BlocInstruction
fintantque;

Trouver une assertion ``invariante'' telle que 
   
  • La pré-condition doit entraîner l'invariant au début de la première itération ;
  • Et l'invariant Plus la ExpressionBooleenne entraînent que l'invariant est vrai à la fin de l'itération ;
  • Et l'invariant Plus la négation de ExpressionBooleenne entraînent la post-condition .
  
1.2.1 Un exemple très simple 
 
la somme des éléments d'un tableau T[1..n]: 

i:=1;
s:=0;
tant que i<=n faire
s:=s+T[i];
i:=i+1;
fintantque;

L’étude de cette boucle se fait ainsi :
 
  • L'invariant? s= somme des éléments de T de T[1] jusqu'à T[i-1]
  • vraie chaque fois qu'on calcule l'expression booléenne (mais pas juste après la première affectation!)
  • pré-condition i=1 et s=0
  • pour déduire la post-condition souhaitée, ajouter à l'invariant i <= n+1
  
1.2.2 Terminaison des boucles 
   
  • La méthode donnée peut démontrer que la post-condition est vraie quand et si l'exécution d'une boucle termine.
  • Il faut aussi démontrer la terminaison.
  • définition d'une mesure du calcul qui reste à faire (p. ex. n+1-i)
  • Qui diminue à chaque itération ?
  • La boucle termine dès qu'elle est nulle (ou négative)
  • une valeur entière !
    
1.2.3 Un (mauvais) algorithme de tri 
  
Le code suivant est un mauvais algorithme de tri :
  
i:=1;
tant que i<n faire
si T[i]>T[i+1]
alors debut ???;i:=1; fin
sinon i:=i+1;
finsi
fintantque

On peut démontrer qu’il s’agit d’un mauvais algorithme de tri :
  
  • si on démontre que le ??? ne change ni l'ensemble des valeurs de T (mettons val(T)), ni i, on prend pour invariant val(T)=val(T0)  et   T[1..i] trié; et démontre que la boucle trie T (si elle termine)
  • et si ??? échange T[i] et T[i+1], on peut démontrer aussi que la boucle termine
  • mesure: n×nombre d¢inversions+n-i
   
1.2.4 Autres exemples 
    
  • recherche linéaire
  • recherche dichotomique dans un tableau trié
  • calcul des puissances
  • pgcd (généralisé)
   
1.3 Des cas ou le bon invariant aide à concevoir l'algorithme? 
   
  • recherche d'une valeur dans un tableau de deux dimensions où chaque ligne et chaque colonne est triée
  • recherche dichotomique dans chaque ligne prendrait temps n log(n);
  • comparer la valeur cherchée avec un élément au milieu du tableau n'aide pas
  • comparer avec un élément dans un coin permet de supprimer une ligne ou une colonne 
  
Un invariant peut servir à concevoir, expliquer, documenter, comprendre, tester, un algorithme
  
1.3.1 Exemple : Trouver le vainqueur d'une élection 
   
  • Un tableau V (unidimensionnel) contient des votes; étant donné que quelqu'un a une majorité absolue, trouver qui dans une lecture du tableau!
  • Invariant: Dans la section V[1..x], personne n'a pas de majorité absolue; dans la section V[x+1..i], candidat c a m votes de plus que tous les autres candidats (m > 0);
  • facile à trouver le code qui maintient l'invariant
  • ajouter une dernière phase de vérification si besoin
   
1.3.2 Les procédures et fonctions 
  
Démontrer le bon fonctionnement d’une procédure ou d’une fonction consiste à :
   
  • Démontrer pour chaque fonction () qu'elle produit le résultat souhaitée ;
  • En utilisant ce même fait pour les autres fonctions déjà prouvées ;
  • Pour les fonctions récursives, un raisonnement par récurrence (qui nécessite souvent une description minutieuse du résultat dans tous les cas).
  
-------------------------------------------------------------------------------------------------------
Précédent : Complexité des algorithmes
  
                  Suivant : Le problème de Fusion-Recherche 
               

Article plus récent Article plus ancien

Leave a Reply

Telechargement