Specification and Proof in Membership Equational Logic

Adel Bouhoula 1 Jean-Pierre Jouannaud José Meseguer
1 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : This paper is part of a long-term effort to increase expressiveness of algebraic specification languages while at the same time having a simple semantic foundation on which efficient execution by rewriting and powerful theorem-proving tools can be based. In particular, our rewriting techniques provide semantic foundations for Maude's functional sublanguage, where they have been efficiently implemented. This effort started in the late seventies, led by the ADJ group, who promoted equational logic and universal algebra as the semantic basis of program specification languages. An important later milestone was the work around order-sorted algebras and the OBJ family of languages developed at SRI-International in the eighties. This effort has been substantially advanced in the mid-nineties with the development of Maude, a language based on membership equational logic. Membership equational logic is quite simple, and yet quite powerful. Its atomic formulae are equations and sort membership assertions, and its sentences are Horn clauses. It extends in a conservative way both (a version of) order-sorted equational logic and partial algebra approaches, while Horn logic with equality can be very easily encoded. After introducing the basic concepts of the logic, we give conditions and proof rules with which efficient equational deduction by rewriting can be achieved. We also give completion techniques to transform a specification into one meeting these conditions. We address the important issue of proving that a specification protects a subspecification, a property generalizing the usual notion of sufficient completeness. Using tree-automata techniques, we develop a test-set based approach for proving inductive theorems about a parameterized specification. We briefly discuss the extension of our techniques in presence of associative-commutative axioms and of extra variables in conditions, as well as solving goals by narrowing. Finally, we discuss the generality of our approach and how it extends several previous approaches.
Type de document :
Article dans une revue
Theoretical Computer Science, Elsevier, 2000, 236 (1-2), pp.35-132
Liste complète des métadonnées

https://hal.inria.fr/inria-00099079
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 08:50:47
Dernière modification le : mardi 17 avril 2018 - 11:48:04

Identifiants

  • HAL Id : inria-00099079, version 1

Collections

Citation

Adel Bouhoula, Jean-Pierre Jouannaud, José Meseguer. Specification and Proof in Membership Equational Logic. Theoretical Computer Science, Elsevier, 2000, 236 (1-2), pp.35-132. 〈inria-00099079〉

Partager

Métriques

Consultations de la notice

89