Among the various tasks involved in SE & KE, requirements engineering, specification, prototyping, and validation are regarded as crucial since they decide whether a software system fulfills the users’ expectations. Formal methods provide a rigorous framework to guaranteed. Logic Programming has been recently shown as a promising candidate support these tasks and some relevant features can be in that way captured and formally regarding these concerns. Nevertheless, formalism does need some explanation to let it be more readable and understandable. This paper focuses on a specification design method which mixes formal text (represented by a logic program) and comments (using either formal or informal assertions). By the design of a specification we refer to the intertwined tasks of describing the specification and improving it by the investigation of proofs. These proofs aim to verify the link between the specification and the comments, and are partly automated. Then we present our practical experience in the use of an interacti ve proof system. As an example, we show how this methodology is currently applied to the draft of standard Prolog.

This paper illustrates the possibility to prove correctness of a compiler defined by semantic attributes. Source language and object code are first described. The source language corresponds to LISP compilable functions and the object code to an abstract machine. Then the translation between them is defined and the proof technique is described and illustrated by some examples. The interest of this technique is the modularity of the proof. Cet article montre comment il est possible de prouver la correction d'un compilateur décrit par attributs sémantiques. Le language source et le code objet sont introduits en premier lieu. Le premier correspond aux fonctions LISP compilables et le second à une machine abstraite. La traduction de l'un dans l'autre est ensuite définie et la méthode de preuve est exposée. L'intérêt de cette méthode repose sur l'extrême modularité de ce type de preuve.