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

Projet CHLOEFormal 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