Jass — Java with Assertions1 1This work was partially funded by the German Research Council (DFG) under grant OL 98/3-1.

Abstract

Design by Contract, proposed by Meyer for the programming language Eiffel, is a technique that allows run-time checks of specification violation and their treatment during program execution. Jass, Java with assertions, is a Design by Contract extension for Java allowing to annotate Java programs with specifications in the form of assertions. The Jass tool is a pre-compiler that translates annotated into pure Java programs in which compliance with the specification is dynamically tested. Besides the standard Design by Contract features known from classical program verification (e.g. pre- and postconditions, invariants), Jass additionally supports refinement, i.e. subtyping, checks and the novel concept of trace assertions. Trace assertions are used to monitor the dynamic behaviour of objects in time.