Abstract
Tools for a specification language can be implemented directly (by building a special purpose theorem prover) or by a conservative embedding into a typed meta-logic, which allows their safe and logically consistent implementation and the reuse of existing theorem prover engines. For being useful, the conservative extension approach must provide derivations for several thousand “folklore” theorems.
In this paper, we present an approach for deriving the mass of these theorems mechanically from an existing library of the meta-logic. The approach presupposes a structured theory morphism mapping library datatypes and library functions to new functions of the specification language while uniformly modifying some semantic properties; for example, new functions may have a different treatment of undefinedness compared to old ones.
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
Winskel, G.: The Formal Semantics of Programming Languages. MIT Press (1993)
Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing 10 (1998) 171–186
Spivey, J.M.: The Z Notation: A Reference Manual. 2nd edn. Prentice Hall International Series in Computer Science (1992)
Kolyang, Santen, T., Wolff, B.: A structure preserving encoding of Z in Isabelle/HOL. In von Wright, J., Grundy, J., Harrison, J., eds.: TPHOLs. LNCS 1125, Springer (1996)
Gordon, M.J.C., Melham, T.F.: Introduction to HOL. Cambridge Press (1993)
Nipkow, T., von Oheimb, D., Pusch, C.: μJava: Embedding a programming language in a theorem prover. In Bauer, F.L., Steinbrüggen, R., eds.: Foundations of Secure Computation. Volume 175 of NATO Science Series F: Computer and Systems Sciences., IOS Press (2000) 117–144
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Volume 2283 of LNCS. Springer (2002)
Reetz, R.: Deep Embedding VHDL. In E.T. Schubert, P.J. Windley, J. Alves-Foss, eds.: 8th International Workshop on Higher Order Logic Theorem Proving and its Applications. Volume 971 of Lecture Notes in Computer Science., Springer (1995) 277–292
Ozols, M.A., Eastaughffe, K.A., Cant, A., Collignon, S.: DOVE: A tool for design modelling and verification in safety critical systems. In: 16th International System Safety Conference. (1998)
Brucker, A.D., Rittinger, F., Wolff, B.: HOL-Z 2.0: A proof environment for Z-specifications. Journal of Universal Computer Science 9 (2003)
Brucker, A.D., Wolff, B.: A proposal for a formal OCL semantics in Isabelle/HOL. In Muñoz, C., Tahar, S., Carreño, V., eds.: Theorem Proving in Higher Order Logics. Number 2410 in LNCS. Springer (2002) 99–114
Brucker, A.D., Wolff, B.: HOL-OCL: Experiences, consequences and design choices. In Jezequel, J.M., Hussmann, H., Cook, S., eds.: UML 2002: Model Engineering, Concepts and Tools. Number 2460 in LNCS. Springer (2002)
OMG: Object Constraint Language Specification. [22] chapter 6
Warmer, J., Kleppe, A.: The Object Contraint Language: Precise Modelling with UML. Addison-Wesley (1999)
Warmer, J., Kleppe, A., Clark, T., Ivner, A., Högström, J., Gogolla, M., Richters, M., Hussmann, H., Zschaler, S., Johnston, S., Frankel, D.S., Bock, C.: Response to the UML 2.0 OCL RfP. Technical report (2001)
OMG: United Modeling Language Specification (Version 1.4). (2001)
Goguen, J.A., Burstall, R.M.: Institutions: abstract model theory for specification and programming. Journal of the ACM (JACM) 39 (1992) 95–146
Nipkow, T.: Order-sorted polymorphism in Isabelle. In Huet, G., Plotkin, G., eds.: Logical Environments. (1993) 164–188
Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5 (1940) 56–68
Andrews, P.B.: An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Academic Press (1986)
Barendregt, H.: Lambda Calculi with Types. In: Handbook of Logic in Computer Science. Clarendon Press (1992) 117–309
Frank Pfenning, C. E.: Higher-order abstract syntax. In: PLDI 1988. (1988) 199–208
G. Huet, B. L.: Proving and applying program transformations expressed with second order patterns. (Acta Informatica)
Boulton, R., Gordon, A., Gordon, M., Harrison, J., Herbert, J., Tassel, J.V.: Experience with embedding hardware description languages in HOL. In Stavridou, V., Melham, T.F., Boute, R.T., eds.: Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience. Volume A-10 of IFIP Transactions., Nijmegen, The Netherlands, North-Holland/Elsevier (1992) 129–156
Wadler, P.: Comprehending monads. In: Proc. 1990 ACM Conference on Lisp and Functional Programming. (1990)
King, D.J., Wadler, P.: Combining monads. In: Glasgow functional programming workshop. (1992)
Altenkirch, T., Gaspes, V., Nordström, B., von Sydow, B.: A User’s Guide to ALF. Chalmers University of Technology, Sweden. (1994)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brucker, A.D., Wolff, B. (2003). Using Theory Morphisms for Implementing Formal Methods Tools. In: Geuvers, H., Wiedijk, F. (eds) Types for Proofs and Programs. TYPES 2002. Lecture Notes in Computer Science, vol 2646. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-39185-1_4
Download citation
DOI: https://doi.org/10.1007/3-540-39185-1_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-14031-3
Online ISBN: 978-3-540-39185-2
eBook Packages: Springer Book Archive