Proving Consistency and Completeness of Model Classes Using Theory Interpretation

Date Added: Jan 2010
Format: PDF

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, the authors present a formal framework based on theory interpretation for proving this correspondence.