Design of formal specifications by normal logic programs : merging formal text and good comments

Abstract : Formal specifications are a kind of art : they mixture formal text and informal comments in an unstructured manner. We present a method based on logic programming in which formal text and comments can be also formally related through proofs. The paper is focused on the description of the proofs system used in the design of such specifications. The specification language uses normal clauses (definite clauses with possibly negative literals in the body) for its formal part and is aimed at defining relations. The comments are expressed as logic formulas written with some of the specified relations and define some local properties that the relations must satify. They introduce some redundancy which helps to understand the specification. The proofs are partial and partly automatized. They are not aimed at complete validation of the specification, but rather at debuging it and improving the comments such that its understanding is facilitated. This approach is illustrated by the example of the design of draft standard Prolog on which this methodology is currently applied.
Type de document :
[Research Report] RR-1897, INRIA. 1993
Liste complète des métadonnées
Contributeur : Rapport de Recherche Inria <>
Soumis le : mercredi 24 mai 2006 - 16:16:55
Dernière modification le : vendredi 16 septembre 2016 - 15:19:38
Document(s) archivé(s) le : mardi 12 avril 2011 - 16:05:22



  • HAL Id : inria-00074774, version 1



Sophie Renault, Pierre Deransart. Design of formal specifications by normal logic programs : merging formal text and good comments. [Research Report] RR-1897, INRIA. 1993. 〈inria-00074774〉



Consultations de la notice


Téléchargements de fichiers