| Attributes | Values |
|---|
| type
| |
| Thesis advisor
| |
| Author
| |
| alternative label
| - Application of abstract interpretation techniques to formal program developments
|
| dc:subject
| - Thèses et écrits académiques
- Génie logiciel
- Langages de programmation fonctionnelle
- Ordinateurs -- Programmation
- Ordinateurs -- Fiabilité
- Interprétation abstraite
- Transformations de programmes
- Développements formels de programmes
- Propriétés fonctionnelles et non fonctionnelles
- Systèmes de type d'ordre supérieur
|
| preferred label
| - Application des techniques d'interprétation abstraite aux développements formels de programmes
|
| Language
| |
| Subject
| |
| dc:title
| - Application des techniques d'interprétation abstraite aux développements formels de programmes
|
| Degree granting institution
| |
| note
| - 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.
|
| dc:type
| |
| http://iflastandar...bd/elements/P1001
| |
| rdaw:P10219
| |
| has content type
| |
| is primary topic
of | |
| is rdam:P30135
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
