Skip to Main content Skip to Navigation

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.
Document type :
Complete list of metadata
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Wednesday, May 24, 2006 - 4:16:55 PM
Last modification on : Friday, February 4, 2022 - 3:15:07 AM
Long-term archiving on: : Tuesday, April 12, 2011 - 4:05:22 PM


  • 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⟩



Record views


Files downloads