Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Logic-Based Program Synthesis and Transformation

LOPSTR 2002: Logic Based Program Synthesis and Transformation pp 126–143Cite as

Refinement of Higher-Order Logic Programs

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2664))

Abstract

A refinement calculus provides a method for transforming specifications to executable code, maintaining the correctness of the code with respect to its specification. In this paper we extend the refinement calculus for logic programs to include higher-order programming capabilities in specifications and programs, such as procedures as terms and lambda abstraction. We use a higher-order type and term system to describe programs, and provide a semantics for the higher-order language and refinement. The calculus is illustrated by refinement examples.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

    Google Scholar 

  2. Oege de Moor and Ganesh Sittampalam. Higher-order matching for program transformation. Theoretical Computer Science, 269(1–2):135–162, 2001.

    Article  MATH  MathSciNet  Google Scholar 

  3. Y. Deville and K.-K. Lau. Logic program synthesis. Journal of Logic Programming, 19,20:321–350, 1994. Special Issue: Ten Years of Logic Programming.

    Article  MathSciNet  Google Scholar 

  4. I. Hayes, R. Nickson, P. Strooper, and R. Colvin. A declarative semantics for logic program refinement. Technical Report 00-30, Software Verification Research Centre, The University of Queensland, 2000.

    Google Scholar 

  5. I. J. Hayes, R. Colvin, D. Hemer, R. Nickson, and P. A. Strooper. A refinement calculus for logic programs. Theory and Practice of Logic Programming, 2(4–5):425–460, July–September 2002.

    Article  MATH  MathSciNet  Google Scholar 

  6. David Lacey, Julian Richardson, and Alan Smaill. Logic program synthesis in a higher-order setting. In John W. Lloyd et al., editor, Computational Logic 2000, volume 1861 of LNAI, pages 87–100. Springer-Verlag, 2000.

    Google Scholar 

  7. Zohar Manna. Mathematical Theory of Computation. McGraw-Hill, 1974.

    Google Scholar 

  8. Carroll Morgan. Programming from Specifications. Prentice Hall, second edition, 1994.

    Google Scholar 

  9. G. Nadathur and D. Miller. An overview of Lambda-PROLOG. In Kenneth A. Bowen and Robert A. Kowalski, editors, Fifth International Logic Programming Conference, pages 810–827. MIT Press, 1988.

    Google Scholar 

  10. G. Nadathur and D. Miller. Higher-order logic programming. In Dov M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logics for Artificial Intelligence and Logic Programming, volume 5, chapter 8, pages 499–590. Clarendon Press, Oxford, 1998.

    Google Scholar 

  11. D. A. Naumann. Predicate transformer semantics of a higher order imperative language with record subtyping. Science of Computer Programming, 41(1):1–51, September 2001.

    Article  MATH  MathSciNet  Google Scholar 

  12. H. A. Partsch. Specification and Transformation of Programs. Springer-Verlag, 1990.

    Google Scholar 

  13. D. Sannella. Formal program development in Extended ML for the working programmer. In Proc. 3rd BCS/FACS Workshop on Refinement, Springer Workshops in Computing, pages 99–130. Springer, 1990.

    Google Scholar 

  14. S. Seres and M. Spivey. Higher-order transformation of logic programs. In K.-K. Lau, editor, Proceedings of the Tenth International Workshop on Logic-based Program Synthesis and Transformation (LOPSTR 2000), volume 2042 of LNCS, pages 57–68. Springer-Verlag, 2000.

    Google Scholar 

  15. Z. Somogyi, F.J. Henderson, and T.C. Conway. Mercury, an efficient purely declarative logic programming language. In R. Kotagiri, editor, Proceedings of the Eighteenth Australasian Computer Science Conference, pages 499–512, Glenelg, South Australia, 1995. Australian Computer Science Communications.

    Google Scholar 

  16. J. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, second edition, 1992.

    Google Scholar 

  17. Nigel Ward. A Refinement Calculus for Nondeterministic Expressions. PhD thesis, Department of Computer Science, University of Queensland, 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Verification Research Centre, Brisbane, Australia, 4072

    Robert Colvin & David Hemer

  2. School of Information Technology and Electrical Engineering, University of Queensland, Brisbane, Australia, 4072

    Ian Hayes & Paul Strooper

Authors
  1. Robert Colvin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ian Hayes
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. David Hemer
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Paul Strooper
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dept. of Electronics and Computer Science, University of Southampton, Highfield, Southampton, SO17 1BJ, UK

    Michael Leuschel

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Colvin, R., Hayes, I., Hemer, D., Strooper, P. (2003). Refinement of Higher-Order Logic Programs. In: Leuschel, M. (eds) Logic Based Program Synthesis and Transformation. LOPSTR 2002. Lecture Notes in Computer Science, vol 2664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45013-0_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-45013-0_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40438-5

  • Online ISBN: 978-3-540-45013-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation