Treffer: Constructing Verifiably Correct Java Programs Using OCL and CleanJava

A recent trend in software development is building a precise model that can be used as a basis for the software development. Such a model may enable an automatic generation of working code, and more importantly it provides a foundation for correctness reasoning of code. In this paper we propose a practical approach for constructing a verifiably correct program from such a model. The key idea of our approach is (a) to systematically translate formally-specified design constraints such as class invariants and operation pre and postconditions to code-level annotations and (b) to use the annotations for the correctness proof of code. For this we use both the Object Constraint Language (OCL) and CleanJava. CleanJava is a formal annotation language for Java and supports a Cleanroom-style functional program verification. The combination of OCL and CleanJava makes our approach not only practical but also easily incorporated and integrated into object-oriented software development methods. We expect our approach to provide a practical alternative or complementary technique to program testing to assure the correctness of software.