In this paper we describe a framework that allows users of Formal Development Environments (FDEs) to prove verification conditions using stand-alone theorem provers. Verification conditions from a given FDE are translated into an intermediate representation, then in turn translated into a form that is readable by the target theorem prover. In this paper we describe a systematic approach to the development of translators from the intermediate representation to a target theorem prover representation. The approach involves the development of a generic translator, which is instantiated for a particular target theorem prover by defining a variety of translation rules. In this paper we describe the different kinds of translation rules and illustrate their use with an example.
展开▼
