Chapter 1 Project Description

Proving programs in a fully mathematical and rigorous way is hard and time consuming. Although there exist a number of formal approaches to software engineering like the Z specification language or the B method, these environments strongly focus on refinement based programming and do not directly support object-oriented programming. On the other side, the JML specification language is an object-oriented extension to the JAVA programming language, which allows annotating existing JAVA programs with specification attributes and contracts. But neither of these approaches really take advantage of the most beneficial concept in software engineering: Reuse of already available software elements. It should not only be possible to reuse units of implemented software, but also rely on units of already proven software. Unfortunately, the traditional methods like B and JML only gradually support the reuse of already proven software units. In the Eiffel method, contracts have become first-class citizens of the programming language. Designed as taking an integral part in the software specification process and providing expressive semi-formal definitions of software interfaces, it turns out that Eiffel contracts are not powerful enough to express the complicated relationships in object graphs of modern object-oriented environments. Faced with these shortcomings, the idea to combine the reusability and extendibility of object-oriented methods with th