Tutorial at CADE-20

Integrating Object-oriented Design and
Deductive Verification of Software

Chapter

Deductive analysis of design and formal specification

To analyse a design and specification it must be translated into a logical language that is accessible to a deductive treatment. We present a translation of UML/OCL or JML, respectively, into (classical) first-order predicate logic.

Making use of the translation it is then possible to generate proof obligations for properties of the design such as the structural subtyping condition (the invariant of a sub-class is stronger than the invariant of its super-class). Automated and interactive theorem proving techniques provide means to discharge such proof obligations.

We show how, in the KeY-Tool, both the generation and discharging of proof obligations has been integrated into a commercial CASE tool.