Skip to Main content Skip to Navigation

Vérification des programmes logiques.

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.
Document type :
Complete list of metadata
Contributor : Ecole Polytechnique Connect in order to contact the contributor
Submitted on : Thursday, July 29, 2010 - 3:13:00 PM
Last modification on : Monday, January 31, 2022 - 2:36:41 PM
Long-term archiving on: : Thursday, November 4, 2010 - 10:03:15 AM


  • HAL Id : pastel-00000864, version 1



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



Record views


Files downloads