Abstract FR:

Ce travail s'inscrit dans le cadre du développement formel de programmes. Ces programmes sont obtenus par transformation de spécifications formelles (algébriques) en appliquant des règles de base du système fold/unfold ou des tactiques de développement les combinant. A cet effet un langage de développement par transformation a été défini. Il est supporté par un système de types d'ordre supérieur appelé DEVA développé dans le cadre du projet ESPRIT-TOOL'USE. Les développements sont exprimés dans ce langage. L'isomorphisme de Curry-Howard établissant la correspondance entre type et proposition garantit la correction des développements. Un des objectifs principaux a été la prise en compte des propriétés non fonctionnelles durant les phases du développement. Nous nous sommes particulièrement intéressés à la complexité en temps et à la précision des programmes numériques. L'interprétation abstraite étendue aux développements formels de programmes a permis l'évaluation et la vérification de ces propriétés et donc l'utilisation de celles-ci pour diriger les transformations. Le contrôle d'une propriété permet la sélection d'une tactique de transformation ou le choix de représentation de données. Les schémas de programmes de Huet & Lang ont été étendus aux schémas de développement. Ceci a permis d'envisager la réutilisation des programmes obtenus mais aussi des développements grâce au filtrage (matching) des spécifications. Une analyse des développements pour détecter les propriétés pertinentes a été développée: elle permet l'extraction des propriétés à vérifier lors de la réutilisation.