iContract-the JavaTM design by ContractTM tool

Until today, the explicit specification of “software contracts” by means of class invariants and method pre- and post-conditions was only available to Eiffel developers. iContract is the first tool that provides the same thorough support for Java. iContract is a freely available source-code pre-processor that instruments source-code with checks for class invariants as well as preand post-conditions that may be associated with methods in classes and interfaces. Special comment tags (@pre, @post, @invariant) are interpreted by iContract and converted into assertion check code that is inserted into the source-code. iContract supports universal and existential quantifiers in contract expressions. Contracts are propagated via all 4 Java type extension mechanisms (class extension: innerclasses, interface implementation and interface extension). Due to the non-mandatory nature of the comment tags, source code that contains design by contract annotations remains fully compatible with Java and can thus be processed with standard Java compilers, enabling a risk-free adoption of the technique in an organisation