Refining specifications to logic programs

  • I. J. Hayes
  • R. G. Nickson
  • P. A. Strooper
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1207)


The refinement calculus provides a framework for the stepwise development of imperative programs from specifications. In this paper we study a refinement calculus for deriving logic programs. Dealing with logic programs rather than imperative programs has the dual advantages that, due to the expressive power of logic programs, the final program is closer to the original specification, and each refinement step can achieve more. Together these reduce the overall number of derivation steps.

We present a logic programming language extended with specification constructs (including general predicates, assertions, and types and invariants) to form a wide-spectrum language. General predicates allow non-executable properties to be included in specifications. Assertions, types and invariants make assumptions about the intended inputs of a procedure explicit, and can be used during refinement to optimize the constructed logic program. We provide a semantics for the extended logic programming language and derive a set of refinement laws. Finally we apply these to an example derivation.


Logic Program Logic Programming General Predicate Recursive Call Horn Clause 
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.
    K. R. Apt. Program verification and Prolog. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995.Google Scholar
  2. 2.
    W. Bibel. Syntax-directed, semantics-supported program synthesis. Artificial Intelligence, 14:243–261, 1980.Google Scholar
  3. 3.
    R.-J. Back. Correctness preserving program refinements: Proof theory and applications. Tract 131, Mathematisch Centrum, Amsterdam, 1980.Google Scholar
  4. 4.
    K. Clark. The synthesis and verification of logic programs. Research report, Imperial College, 1978.Google Scholar
  5. 5.
    Yves Deville. Logic Programming: Systematic Program Development. Addison-Wesley, 1990.Google Scholar
  6. 6.
    Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.Google Scholar
  7. 7.
    I. J. Hayes and P. A. Strooper. Refining specifications to logic programs. Fifth Australasian Refinement Workshop. Software Verification Research Centre, Department of Computer Science, The University of Queensland, April 1996.Google Scholar
  8. 8.
    C. J. Hogger. Derivation of logic programs. Journal of the ACM, 2:372–392, 1981.Google Scholar
  9. 9.
    J.-M. Jacquet. Constructing logic programs. John Wiley & Sons, 1993.Google Scholar
  10. 10.
    Cliff B. Jones. Systematic Software Development using VDM. Second edition. Prentice-Hall International, 1990.Google Scholar
  11. 11.
    Joost N. Kok. On logic programming and the refinement calculus: semantics based program transformations. Technical Report RUU-CS-90-39, Department of Computer Science, Utrecht University, 1990.Google Scholar
  12. 12.
    Carroll Morgan. Programming from Specifications. Prentice Hall, 1990. Second edition 1994.Google Scholar
  13. 13.
    C. C. Morgan and K. A. Robinson. Specification statements and refinement. IBM Jnl. Res. Dev., 31(5), September 1987.Google Scholar
  14. 14.
    J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287–306, December 1987.CrossRefGoogle Scholar
  15. 15.
    L. Naish. Specification = program + types. In Proc. Seventh Conf. on the Foundations of Software Technology and Theoretical Computer Science, Pune, India, volume 287 of Lecture Notes in Computer Science. Springer Verlag, 1987.Google Scholar
  16. 16.
    L. Naish. Types and the intended meaning of logic programs. In F. Pfenning, editor, Types in Logic Programming, pages 189–216. MIT Press, 1992.Google Scholar
  17. 17.
    L. Naish. Verification of logic programs and imperative programs. In J.-M. Jacquet, editor, Constructing Logic Programs. John Wiley & Sons, 1993.Google Scholar
  18. 18.
    Ray Nickson and Ian Hayes. Supporting contexts in program refinement. Technical Report 96-29, Software Verification Research Centre, Department of Computer Science, The University of Queensland, 1996.Google Scholar
  19. 19.
    F. Pfenning. Types in logic programming. MIT Press, 1992.Google Scholar
  20. 20.
    M. G. Read and E. A. Kazmierczak. Formal program development in modular Prolog: A case study. In T.P. Clement and K.-K. Lau, editors, Proc. of LOPSTR'91, 1991.Google Scholar
  21. 21.
    D. R. Smith. KIDS: A semi-automatic program development system. IEEE Transactions on Software Engineering, 16(9):1024–1043, 1990.Google Scholar
  22. 22.
    Leon Sterling and Ehud Shapiro. The Art of Prolog. MIT Press, 1986. Second edition 1994.Google Scholar
  23. 23.
    Mark Utting, Anthony Bloesch and Ray Nickson. Ergo 4.1 Reference Manual. Technical Report, Software Verification Research Centre, Department of Computer Science, The University of Queensland. In preparation.Google Scholar
  24. 24.
    Nigel Ward. A Refinement Calculus for Nondeterministic Expressions. PhD thesis, The University of Queensland, 1994.Google Scholar
  25. 25.
    J. B. Wordsworth. Software Development with Z: A Practical Approach to Formal Methods. Addison-Wesley, 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • I. J. Hayes
    • 1
  • R. G. Nickson
    • 1
  • P. A. Strooper
    • 1
  1. 1.Department of Computer ScienceThe University of QueenslandBrisbaneAustralia

Personalised recommendations