Using Theory Morphisms for Implementing Formal Methods Tools

by Achim D. Brucker and Burkhart Wolff

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.

Keywords: Formal Methods, Formal Semantics, Shallow Embeddings, Theorem Proving, OCL
Categories:
Documents: (full text as PDF file)

Please cite this article as follows:
Achim D. Brucker and Burkhart Wolff. Using Theory Morphisms for Implementing Formal Methods Tools. In Types for Proof and Programs. Lecture Notes in Computer Science (2646), pages 59-77, Springer-Verlag, 2003.
Keywords: Formal Methods, Formal Semantics, Shallow Embeddings, Theorem Proving, OCL
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/3-540-39185-1_4) ( )

BibTeX
@InCollection{ brucker.ea:embedding:2003,
 abstract = {Tools for a specification language can be implemented \emph{directly} (by building a special purpose theorem prover) or \emph{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 \emph{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.}, address = {Heidelberg}, author = {Achim D. Brucker and Burkhart Wolff}, booktitle = {Types for Proof and Programs}, doi = {10.1007/3-540-39185-1_4}, editor = {Herman Geuvers and Freek Wiedijk}, isbn = {3-540-14031-X}, issn = {0302-9743}, keywords = {Formal Methods, Formal Semantics, Shallow Embeddings, Theorem Proving, OCL}, language = {USenglish}, location = {Nijmegen}, number = {2646}, pages = {59--77}, pdf = {https://www.brucker.ch/bibliography/download/2003/brucker.ea-embedding-2003.pdf}, project = {CSFMDOS}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, title = {Using Theory Morphisms for Implementing Formal Methods Tools}, url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-embedding-2003}, year = {2003},
}