Abstraction is essential in the formal specification of programs. A common way of writing abstract specifications is to specify implementations in terms of basic mathematical structures. Specification languages like JML offer so-called model classes that provide interfaces to such structures. One way to reason about specifications that make use of model classes is to map model classes directly to structures provided by the theorem prover used for verification. Crucial to the soundness of this technique is the existence of a semantic correspondence between the model class and the related structure. In this paper, we present a formal framework based on theory interpretation for proving this correspondence. The framework provides a systematic way of determining the necessary proof obligations and justifies the soundness of the approach.
展开▼
