Abstract FR:

Le sujet de cette these est le developpement d'une methode formelle de mise en Œuvre sequentielle des programmes gamma. Le langage gamma est un langage de haut niveau qui permet de decrire des algorithmes a un niveau d'abstraction tres eleve: la seule structure de donnees est le multi-ensemble et le calcul consiste en une succession d'applications de regles de reaction. Chaque regle selectionne un sous-ensemble d'elements du multi-ensemble verifiant une condition de reaction, et les remplace par de nouveaux elements. Le calcul s'arrete quand aucune regle ne peut plus s'appliquer. Les reactions peuvent s'executer dans n'importe quel ordre, et meme en parallele si elles agissent sur des sous-ensembles disjoints d'elements. Dans une premiere etape, nous developpons un schema general de mise en Œuvre qui est base sur la generation systematique de toutes les combinaisons d'elements. Nous montrons ensuite qu'en detectant certaines proprietes dans le programme a mettre en Œuvre, il est possible d'optimiser le schema. Une premiere optimisation permet de diminuer le nombre de combinaisons et une deuxieme vise a imposer un ordre sur les reactions de facon a terminer le calcul le plus rapidement possible. Enfin dans une derniere etape nous nous attachons a raffiner les multi-ensembles en des structures de donnees de plus bas niveau et plus efficaces