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

Please cite this work as follows:
A. D. Brucker and B. Wolff, “Using theory morphisms for implementing formal methods tools,” in Types for proof and programs, H. Geuvers and F. Wiedijk, Eds. Heidelberg: Springer-Verlag, 2003, pp. 59–77. doi: 10.1007/3-540-39185-1_4. Author copy: https://logicalhacking.com/publications/brucker.ea-embedding-2003/

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.},
  keywords  = {Formal Methods, Formal Semantics, Shallow Embeddings, Theorem
               Proving, OCL},
  location  = {Nijmegen},
  author    = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Types for Proof and Programs},
  language  = {USenglish},
  pages     = {59--77},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {2646},
  isbn      = {3-540-14031-X},
  editor    = {Herman Geuvers and Freek Wiedijk},
  title     = {Using Theory Morphisms for Implementing Formal Methods
               Tools},
  doi       = {10.1007/3-540-39185-1_4},
  issn      = {0302-9743},
  areas     = {formal methods},
  year      = {2003},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-embedding-2003/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-embedding-2003/brucker.ea-embedding-2003.pdf},
}