Software formal specification by logic programming: The example of standard Prolog

  • AbdelAli Ed-DbaliEmail author
  • Pierre DeransartEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 636)


The aim of this presentation is to show how logic programming can be used to make formal specifications. This approach is illustrated by the project of standard Prolog, as discussed in the ISO working group, which has been completely described by a formal specification.


Logic Programming Error Category Validation Tool Partial Correctness Proof Method 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Apt, K. R., Blair, H., Walker, A.: Toward a theory of declarative Knowledge. LITP, RR 86-10 (Fed. 1986)Google Scholar
  2. 2.
    Deransart, P.: Proof Methods of Declarative Properties of Definite Programs. RR 1248, INRIA-Rocquencourt, (June 1990) 64p (to appear in TCS).Google Scholar
  3. 3.
    Deransart, P., Ferrand, G.: Proof Method of Partial Correctness and Partial Completeness for Normal Logic Programs. RR 92-4, LIFO, University of Orléans, (April 1992) 12p. To appear in ICLP'92 proceedings (Washington DC, Nov 1992).Google Scholar
  4. 4.
    Deransart, P., Ferrand, G.: An Operational Formal Definition of Prolog: A Specification Method and its Application. New Generation Computing 10 (1992) 121–171.Google Scholar
  5. 5.
    Ed-Dbali, A., Deransart, P., Scowen, R. (ed.): Prolog, A guide to the executable specification. ISO/IEC JTC1 SC22 WG17 N71, (Jan 1991)Google Scholar
  6. 6.
    Lloyd, J. W.: Foundations of logic programming (First ed.). Springer-Verlag, Berlin, (1984)Google Scholar
  7. 7.
    Renault, S.: Logic Programs Validation (in French). DEA Repport, University of Paris 7, (September 1991) 65p.Google Scholar
  8. 8.
    Scowen, R. (ed.): Prolog Part 1 — General Core. ISO/IEC JTC1 SC22 WG17 N92 (March 1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  1. 1.LIFOUniversité d'OrléansOrleans Cedex 2France
  2. 2.Projet ChLoÉ Domaine de VoluceauINRIALe Chesnay Cedex

Personalised recommendations