Abstract
We present a shallow embedding of the weakest precondition semantics for a program refinement language. We use the Isabelle/ZF theorem prover for untyped set theory, and statements in our refinement language are represented as set transformers. Our representation is significant in making use of the expressiveness of Isabelle/ZF’s set theory to represent states as dependently-typed functions from variable names to their values. This lets us give a uniform treatment of statements such as variable assignment, framed specification statements, local blocks, and parameterisation. ZF set theory requires set comprehensions to be explicitly bounded. This requirement propagates to the definitions of statements in our refinement language, which have operands for the state type. We reduce the syntactic burden of repeatedly writing the state type by using Isabelle’s meta-logic to define a lifted set transformer language which implicitly passes the state type to statements.
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.
References
J. R. Abrial. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.
S. Agerholm. Mechanizing program verification in HOL. Master’s thesis, Computer Science Department, Aarhus University, April 1992.
R. J. R. Back. On the correctness of refinement steps in program development. Technical Report A-1978-4, 0Abo Akademi University, 1978.
R. J. R. Back. A calculus of refinements for program derivations. Acta Informatica, 25:593–624, 1988.
R. J. R. Back and J. von Wright. Refinement calculus, part I: Sequential nondeterministic programs. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of LNCS, pages 42–66. Springer-Verlag, 1989.
R. J. R. Back and J. von Wright. Refinement concepts formalized in higher order logic. Formal Aspects of Computing, 2(3):247–272, 1990.
Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, and John Herbert. Experience with embedding hardware description languages. In Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, volume A10 of IFIP Transactions, pages 129–156. North-Holland/Elsevier, June 1992.
D. Carrington, I. Hayes, R. Nickson, G. Watson, and J. Welsh. Refinement in Ergo. Technical Report 94-44, Software Verification Research Centre, The University of Queensland, July 1995.
E. W. Dijkstra. A Discipline of Programming Prentice Hall, 1976.
M. Gordon, R. Milner, and C. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of LNCS. Springer-Verlag, 1979.
M. J. C. Gordon and T. F. Melham, editors. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.
Thomas Kleymann. Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. PhD thesis, Laboratory for Foundations of Computer Science, The University of Edinburgh, September 1998.
J. Knappmann. A PVS based tool for developing programs in the refinement calculus. Master’s thesis, Christian-Albrechts-University of Kiel, October 1996.
R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. The MIT Press, 1990.
Carroll Morgan. Procedures, parameters, and abstraction: Separate concerns. Science of Computer Programming, 11(1):17–28, 1988.
Carroll Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3):403–419, July 1988.
Carroll Morgan. Programming from Specifications. Prentice-Hall International, 2nd edition, 1994.
J. M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9(3):287–306, December 1987.
R. G. Nickson and L. J. Groves. Metavariables and conditional refinements in the refinement calculus. Technical Report 93-12, Software Verification Research Centre, The University of Queensland, 1993.
L. C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of LNCS. Springer-Verlag, 1994.
H. Pfeifer, A. Dold, F. W. von Henke, and H. Rueff. Mechanised semantics of simple imperative programming constructs. Technical Report UIB-96-11, Universität Ulm, December 1996.
Chris H. Pratten. Refinement in a Language with Procedures and Modules. PhD thesis, Department of Engineering and Computer Science, University of Southampton, June 1996.
Mark Staples. Window inference in Isabelle. In L. Paulson, editor, Proceedings of the First Isabelle User’s Workshop, volume 379, pages 191–205. University of Cambridge Computer Laboratory Technical Report, September 1995.
Mark Staples. A Mechanised Theory of Refinement. PhD thesis, Computer Laboratory, University of Cambridge, November 1998. Submitted.
M. Utting and K. Whitwell. Ergo user manual. Technical Report 93-19, Software Verification Research Centre, The University of Queensland, February 1994.
J. von Wright. The lattice of data refinement. Acta Informatica, 31, 1994.
J. von Wright. Verifying modular programs in HOL. Technical Report 324, University of Cambridge Computer Laboratory, January 1994.
J. von Wright. A Mechanised Calculus of Refinement in HOL, January 27, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Staples, M. (1999). Representing WP Semantics in Isabelle/ZF. In: Bertot, Y., Dowek, G., Théry, L., Hirschowitz, A., Paulin, C. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1999. Lecture Notes in Computer Science, vol 1690. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48256-3_16
Download citation
DOI: https://doi.org/10.1007/3-540-48256-3_16
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66463-5
Online ISBN: 978-3-540-48256-7
eBook Packages: Springer Book Archive