Construction de programmes logiques par synthèse de propriétés - Université de Lorraine Accéder directement au contenu
Thèse Année : 1993

The Construction of logic programs by synthesising properties

Construction de programmes logiques par synthèse de propriétés

Khaled Bsaïes

Résumé

Not available
Ce travail a pour propos la synthèse de propriétés de programmes logiques pour la transformation par pliage et dépliage. L'objectif général est l'amélioration de l'efficacité des programmes logiques par application des transformations. Le domaine de notre étude est celui des méthodes de développement formel de programmes. L'expérience et l'étude rigoureuse d'exemples montrent que les transformations par pliage et dépliage ne suffisent pas pour obtenir de manière systématique des programmes plus efficaces: il est utile de disposer et d'appliquer des propriétés qui sont des formules logiques particulières pouvant être déduites des clauses formant le programme. Le travail que nous avons réalisé s'articule autour de ces axes: 1) l'intégration de l'application de propriétés en tant que stratégies; 2) l'étude des techniques qui permettent de construire automatiquement des propriétés; en effet la découverte de propriétés est un point crucial qui marque souvent la limite de l'automatisation d'un système; 3) la preuve des propriétés découvertes. Nous avons montré que la découverte des propriétés peut être partiellement automatisé. La démarche générale consiste à mettre en évidence des classes particulières de programmes caractérisées par des modes entrée-sortie et des types. Les modes permettent d'orienter les spécifications en distinguant les données des résultats. Des techniques heuristiques ont été développées à partir de ces caractérisations. Elles permettent dans de nombreux cas de découvrir des propriétés intéressantes. Plus précisément, la stratégie proposée est basée sur l'analyse statique du programme transformé et utilise un mécanisme de projection. Nous avons étudié le problème de dépliage, ce problème est lié à la transformation de programmes logiques guidée par des schémas d'induction. Nous présentons quelques résultats théoriques liés à ce problème.
Fichier non déposé

Dates et versions

tel-01753654 , version 1 (29-03-2018)

Identifiants

  • HAL Id : tel-01753654 , version 1

Accès intranet

Citer

Khaled Bsaïes. Construction de programmes logiques par synthèse de propriétés. Autre. Université Henri Poincaré - Nancy 1, 1993. Français. ⟨NNT : 1993NAN10295⟩. ⟨tel-01753654⟩
8 Consultations
0 Téléchargements

Partager

Gmail Facebook X LinkedIn More