Proving the Equivalence of Logic Programs - Archive ouverte HAL Access content directly
Theses Year : 2004

Proving the Equivalence of Logic Programs

Vérification des programmes logiques.

(1)
1

Abstract

The goal of this work is to present a formal system that can be used to prove the success equivalence of logic programs. By proving success equivalence one can prove that a program representing the specification and another one representing the implementation are equivalent. This can be done by proving that the set of successes of each program is included in the corresponding set of the other one. The language studied is CLPforall which is the Constraint Logic Programming (CLP) language to which the universal quantifier was added. The set of finite success of a program is defined by the finite success semantics of the language. We define also the set of infinite success of a program by extending the definitions for finite success to take into account infinite (non-terminating) computations. This gives the infinite success semantics of the language. We prove that the sets of finite and infinite successes are given by the least and greatest fixed point of the same operator. In order to prove success inclusion we propose a proof system based of the first-order classical logic. The rules for logical operators and quantifiers are the same as in first-order logic. In order to reason about recursively defined predicates we add an induction rule and we prove the correctness of the system under certain conditions. This constitutes the main contribution of this work. The proof of other properties can be reduced to the proof of success inclusion. The same proof system can be used to prove infinite success inclusion by replacing the induction rule with a coinduction rule. We prove the correctness of the system under conditions analogous to those for finite successes. We also show that the two systems are equivalent under some conditions related to the existence of negated constraints. The implementation of a proof assistant written in Prolog is presented. The software assists the user in building proof and has a simple but effective proof-search procedure that reduces the user's work.
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.
Fichier principal
Vignette du fichier
Craciunescu.pdf (2.84 Mo) Télécharger le fichier

Dates and versions

pastel-00000864 , version 1 (29-07-2010)

Identifiers

  • HAL Id : pastel-00000864 , version 1

Cite

Sorin Craciunescu. Vérification des programmes logiques.. Informatique [cs]. Ecole Polytechnique X, 2004. Français. ⟨NNT : ⟩. ⟨pastel-00000864⟩
160 View
93 Download

Share

Gmail Facebook Twitter LinkedIn More