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 the Object Constraint Language (OCL) and CleanJava. CleanJava is a formal annotation language for Java and supports Cleanroom-style functional program verification. The combination of OCL and CleanJava makes our approach not only practical but also suitable for its incorporation into existing 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.