Tutorial at CADE-20
Integrating Object-oriented Design and
Deductive Verification of Software
Chapter
Design and specification of object-oriented programs
The approach which is subject of this tutorial comprises two alternative specification mechanisms as 'front ends'. The one is UML/OCL, the other is JML.
Using the Unified Modeling Language (UML), in particular UML class diagrams, and the Object Constraint Language (OCL), which is part of the UML standard, we show how domain models can be designed and how details of the model can be clarified by adding formal textual constraints. Alternatively, using the Java Modeling Language (JML), constraints are being attached to the implementation directly. In addition to functional specifications consisting of pre-/post-condition pairs and invariants, we describe how to handle the frame problem, i.e., how to specify which parts of the state an operation do not change.
We demonstrate two kinds of tool support for authoring formal specifications that help inexperienced developers to create constraints:
- Pattern and idiom instantiation mechanisms that are based on extending design patterns and idioms with constraint schemata.
- A natural language authoring tool, which allows users to develop constraints simultaneously in natural language (e.g. English) and a formal specification language (e.g. OCL).