Skip to Main content Skip to Navigation
Reports

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 :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00074774
Contributor : Rapport de Recherche Inria <>
Submitted on : Wednesday, May 24, 2006 - 4:16:55 PM
Last modification on : Thursday, February 11, 2021 - 2:50:07 PM
Long-term archiving on: : Tuesday, April 12, 2011 - 4:05:22 PM

Identifiers

  • HAL Id : inria-00074774, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

170

Files downloads

66