Abstract FR:

Le formalisme des equations recurrentes affines est bien adapte a la synthese de materiel et de logiciel paralleles. Le langage alpha est derive de ce formalisme, et l'environnement associe procure des outils automatiques pour l'analyse et la transformation de programmes alpha. Ainsi une specification algorithmique de haut niveau peut etre transformee, par raffinements successifs, en une implementation fonctionnellement equivalente. Cette these presente des extensions au formalisme qui y apportent les avantages bien connus de la programmation structuree. Ces extensions sont de deux types : d'une part on definit des systemes d'equations parametres par un nombre quelconque de parametres de taille, d'autre part on introduit un nouvel operateur qui permet de construire des hierarchies de tels systemes parametres. La syntaxe et la semantique de ces deux extensions sont donnees dans le cadre de alpha, et validees par une implementation dans l'environnement. On montre en particulier que ces extensions n'enlevent rien a la puissance du formalisme en termes de raffinement de programmes. Ces extensions du langage alpha rendent egalement possibles de nouveaux outils de l'environnement. Deux applications en sont decrites en detail : un outil d'analyse statique de programmes structures dans un but de detection d'erreurs, et une transformation de programmes, pour la synthese d'architectures au niveau du bit a partir d'une specification sur des types de donnees abstraits.