Forms of logic specifications: A preliminary study

  • Kung-Kiu Lau
  • Mario Ornaghi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1207)


There is no universal agreement on exactly what form a specification should take, what part it should play in synthesis, and what its precise relationship with the specified program should be. In logic programming, the role of specification is all the more unclear since logic programs are often used as executable specifications. In this paper we take the view that specifications should be set in the context of the problem domain, which we call a framework. We conduct a preliminary study of two useful forms of logic specifications: if-and-only-if and partial specifications. First we set up a three-tier formalism for synthesis, the top-tier being a framework. Then within this formalism we define these two forms of specifications, and discuss their roles in synthesis.


Logic Program Logic Programming Horn Clause Relation Symbol Conditional Specification 
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.
    J.L. Bates and R.L. Constable. Proofs as programs. ACM TOPLAS 7(1):113–136, 1985.CrossRefGoogle Scholar
  2. 2.
    A. Bundy, A. Smaill and G. Wiggins. The synthesis of logic programs from inductive proofs. In J.W. Lloyd, editor, Proc. Esprit Symposium on Computational Logic, pages 135–149, Springer-Verlag, 1990.Google Scholar
  3. 3.
    C.C. Chang and H.J. Keisler. Model Theory. North-Holland, 1973.Google Scholar
  4. 4.
    K.L. Clark. Predicate Logic as a Computational Formalism. Tech. Rep. 79/59, Imperial College, 1979.Google Scholar
  5. 5.
    K.L. Clark. The Synthesis and Verification of Logic Programs. Tech. Rep. 81/36, Imperial College, 1981.Google Scholar
  6. 6.
    Y. Deville and K.K. Lau. Logic program synthesis. J. Logic Programming 19, 20:321–350, 1994. Special issue: Ten years of logic programming.Google Scholar
  7. 7.
    L. Fribourg. Extracting logic programs from proofs that use extended Prolog execution and induction. In D.H.D. Warren and P. Szeredi, editors, Proc. 7 th Int. Conf. on Logic Programming, pages 685–699, MIT Press, 1990.Google Scholar
  8. 8.
    J. Goguen and J. Meseguer. Unifying functional, object-oriented and relational programming with logical semantics. In B. Shriver and P. Wegner, editors, Research Directions in Object-Oriented Programming, pages 417–477, MIT Press, 1987.Google Scholar
  9. 9.
    Å. Hansson and S.-Å. Tärnlund. A natural programming calculus. In Proc. IJCAI 79, pages 348–355, 1979.Google Scholar
  10. 10.
    P.M. Hill and J.W. Lloyd. The Gödel Programming Language. MIT Press, 1994.Google Scholar
  11. 11.
    W. Hodges. Logical features of Horn clauses. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, Vol 1, pages 449–503, Oxford University Press, 1993.Google Scholar
  12. 12.
    C.J. Hogger. Derivation of logic programs. J. ACM, 28(2):372–392, April 1981.Google Scholar
  13. 13.
    C.J. Hogger. Introduction to Logic Programming. Academic Press, 1984.Google Scholar
  14. 14.
    C.B. Jones. Systematic Software Development Using VDM. Prentice Hall, 2nd edition, 1990.Google Scholar
  15. 15.
    T. Kanamori and H. Seki. Verification of Prolog programs using an extension of execution. In E. Shapiro, editor, Proc. 3 rd Int. Conf. on Logic Programming, Lecture Notes in Computer Science 225, pages 475–489, 1986.Google Scholar
  16. 16.
    K.K. Lau and M. Ornaghi. On specification frameworks and deductive synthesis of logic programs. In L. Fribourg and F. Turini, editors, Proc. LOPSTR 94 and META 94, Lecture Notes in Computer Science 883, pages 104–121, Springer-Verlag, 1994.Google Scholar
  17. 17.
    K.K. Lau, M. Ornaghi and S.-Å. Tärnlund. The halting problem for deductive synthesis of logic programs. In P. van Hentenryck, editor, Proc. 11 th Int. Conf. on Logic Programming, pages 665–683, MIT Press, 1994.Google Scholar
  18. 18.
    K.K. Lau and M. Ornaghi. A formal approach to deductive synthesis of constraint logic programs. In J.W. Lloyd, editor, Proc. 1995 Int. Logic Programming Symp., pages 543–557, MIT Press, 1995.Google Scholar
  19. 19.
    K.K. Lau and M. Ornaghi. The relationship between logic programs and specifications — the subset example revisited. To appear in J. Logic Programming.Google Scholar
  20. 20.
    Z. Manna and R. Waldinger. Fundamentals of deductive program synthesis. IEEE Trans. on Soft. Eng. 18(8):53–79, 1992.Google Scholar
  21. 21.
    P. Miglioli, U. Moscato and M. Ornaghi. Abstract parametric classes and abstract data types defined by classical and constructive logical methods. J. Symb. Comp. 18:41–81, 1994.Google Scholar
  22. 22.
    R.A. O'Keefe. What does subset mean? ALP Newsletter 8(3):10, August 1995.Google Scholar
  23. 23.
    J.M. Spivey. Understanding Z. Cambridge University Press, 1988.Google Scholar
  24. 24.
    M. Wirsing. Algebraic specification. In J. Van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 675–788. Elsevier, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Kung-Kiu Lau
    • 1
  • Mario Ornaghi
    • 2
  1. 1.Department of Computer ScienceUniversity of ManchesterManchesterUK
  2. 2.Dipartimento di Scienze dell'InformazioneUniversita' degli studi di MilanoMilanoItaly

Personalised recommendations