Le but de ce travail est de proposer un système formel pour prouver que l'ensemble des succès d'un programme logique est inclus dans l'ensemble correspondant d'un autre programme. Cela permet de prouver que deux programmes logiques, un qui représente la spécification et un représentant l'implantation sont équivalents. Le langage logique considéré est CLPforall qui est le langage le langage de programmation logique avec contraintes (CLP) auquel est ajouté le quantificateur universel. Nous présentons les sémantiques des succès finis et infinis et montrons qu'elles sont données par le plus petit et le plus grand point fixe du même opérateur. Un système de preuve pour l'inclusion des succès finis est présenté. Le système utilise pour les opérateurs et les quantificateurs logiques les mêmes règles que la logique du premier ordre. Pour raisonner sur les prédicats récursifs le système contient une règle d'induction. Nous prouvons la correction du système sous certains conditions. Un système analogue pour l'inclusion des succès infinis est présenté. La règle d'induction est remplacée par une règle de coinduction. La correction est démontrée sous conditions analogues. Les deux systèmes sont équivalents sous certains conditions. Une implantation a été réalisée sous la forme d'assistant de preuve écrit en Prolog. Le programme a environ 4000 lignes et contient des procédures simples mais efficaces de recherche de preuves. Nous présentons des exemples de preuves réalises avec ce programme parmi lesquels la preuve de correction de quicksort.
| Identifer | oai:union.ndltd.org:CCSD/oai:pastel.archives-ouvertes.fr:pastel-00000864 |
| Date | 24 March 2004 |
| Creators | Craciunescu, Sorin |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | French |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0015 seconds