Sciweavers

Share
FASE
2010
Springer

Proving Consistency and Completeness of Model Classes Using Theory Interpretation

9 years 24 days ago
Proving Consistency and Completeness of Model Classes Using Theory Interpretation
Abstract. 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.
Ádám Darvas, Peter Müller
Added 28 May 2010
Updated 28 May 2010
Type Conference
Year 2010
Where FASE
Authors Ádám Darvas, Peter Müller
Comments (0)
books