Faithful mapping of model classes to mathematical structures

ion techniques are indispensable for the specification and verification of functional behavior of programs. In object-oriented ation languages like JML, a powerful abstraction technique is the use of model classes, that is, classes that are only used for specification purposes and that provide object-oriented interfaces for essential mathematical concepts such as set or relation. While the use of model classes in specifications is natural and powerful, they pose problems for verification. Program verifiers map model classes to their underlying logics. Flaws in a model class or the mapping can easily lead to unsoundness and incompleteness. This paper proposes an approach for the faithful mapping of model classes to mathematical structures provided by the theorem prover of the program verifier at hand. Faithfulness means that a given model class semantically corresponds to the mathematical structure it is mapped to. Our approach enables reasoning about programs specified in terms of mod...

• Type: Journal
• Year: 2008
• Where: IEE
• Authors: Ádám Darvas, Peter Müller
• Keywords: IEE 2008, Mathematical Structure, Model Classes, Specification