Abstract
This paper describes a deep embedding of a refinement calculus for logic programs in Isabelle/HOL. It extends a previous tool with support for procedures and recursion. The tool supports refinement in context, and a number of window-inference tactics that ease the burden on the user. In this paper, we also discuss the insights gained into the suitability of different logics for embedding refinement calculii (applicable to both declarative and imperative paradigms). In particular, we discuss the richness of the language, choice between typed and untyped logics, automated proof support, support for user-defined tactics, and representation of program states.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Isabelle home page. http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html.
Ralph Back, Jim Grundy, and Joakim von Wright. Structured calculational proof. Formal Aspects of Computing, 9(5–6):469–483, 1997.
D. Carrington, I. Hayes, R. Nickson, G. Watson, and J. Welsh. A review of existing refinement tools. Technical report 94-08, Software Verification Research Centre, The University of Queensland, Brisbane 4072. Australia, June 1994.
D. Carrington, I. Hayes, R. Nickson, G. Watson, and J. Welsh. A program refinement tool. Formal Aspects of Computing, 10:97–124, 1998.
R. Colvin, I. Hayes, R. Nickson, and P. Strooper. A tool for logic program refinement. In D. J. Duke and A. S. Evans, editors, Second BCS-FACS Northern Formal Methods Workshop, Electronic Workshops in Computing. Springer Verlag, 1997.
J. Grundy. A window inference tool for refinement. In C.B. Jones, R.C. Shaw, and T. Denvir, editors, Fifth Refinement Workshop, Workshops in Computing, pages 230–254. BCS FACS, Springer-Verlag, 1992.
I. Hayes, R. Nickson, and P. Strooper. Refining specifications to logic programs. In J. Gallagher, editor, Logic Program Synthesis and Transformation. Proceedings of the 6th International Workshop, LOPSTR’96, Stockholm, Sweden, August 1996, volume 1207 of Lecture Notes in Computer Science, pages 1–19. Springer Verlag, 1997.
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, October 2000.
D. Hemer. Building tool support for a refinement calculus for logic programming: A comparison of interactive theorem provers. Technical Report 00-06, Software Verification Research Centre, The University of Queensland, March 2000.
P. Homeier and D. Martin. Mechanical verification of mutually recursive procedures. In M.A. McRobbie and J.K. Slaney, editors, Proceedings of the 13th International Conference on Artificial Deduction (CADE-13), number 1104 in Lecture Notes in Artificial Intelligence, pages 201–215. Springer-Verlag, 1996.
Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of Z in Isabelle/HOL. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics — 9th International Conference, LNCS 1125, pages 283–298. Springer Verlag, 1996.
R. Nickson and I. Hayes. Supporting contexts in program refinement. Science of Computer Programming, 29:279–302, 1997.
L.C. Paulson. Isabelle-A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag, 1994.
P.J. Robinson and J. Staples. Formalising the hierarchical structure of practical mathematical reasoning. Journal of Logic and Computation, 3(1):47–61, February 1993.
J.M. Spivey. The Z Notation: a Reference Manual. Prentice-Hall, New York, 1989.
M. Staples. Window inference in Isabelle. In L. Paulson, editor, Proceedings of the First Isabelle User’s Workshop, volume 379 of University of Cambridge Computer Laboratory Technical Report, pages 191–205, September 1995.
M. Staples. A Mechanised Theory of Refinement. PhD thesis, Computer Laboratory, University of Cambridge, 1998.
M. Staples. Representing WP Semantics in Isabelle/ZF. In TPHOLs’ 99, volume 1690 of Lecture Notes in Computer Science, pages 239–254, September 1999.
M. Utting and K. Whitwell. Ergo user manual. Technical Report 93-19, Software Verification Research Centre, The University of Queensland, Brisbane, QLD 4072, Australia, March 1994. Describes Version 4.0 of Ergo.
Mark Utting. The Ergo 5 generic proof engine. Technical Report 97-44, Software Verification Research Centre, The University of Queensland, 1997.
J. von Wright. Program refinement by theorem proving. In D. Till, editor, Sixth Refinement Workshop, Workshops in Computing, pages 121–150. BCS FACS, Springer-Verlag, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hemer, D., Hayes, I., Strooper, P. (2001). Refinement Calculus for Logic Programming in Isabelle/HOL. In: Boulton, R.J., Jackson, P.B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2001. Lecture Notes in Computer Science, vol 2152. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44755-5_18
Download citation
DOI: https://doi.org/10.1007/3-540-44755-5_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42525-0
Online ISBN: 978-3-540-44755-9
eBook Packages: Springer Book Archive