Design by Contract Using Meta-Assertions

The important role that class contracts - pre and post-conditions of methods, and invariants - play in the specification, monitoring and reuse of classes is becoming increasingly accepted by the OO community. The several languages of assertions and monitoring code generation tools that exist allow the specification and, eventually, the runtime checking of very powerful and elegant contracts. This is definitely so for classes as simple as Stack, Point or Account. However, when the aim is the writing of pre and post-conditions for methods in classes that are clients of those simple classes, the task reveals itself harder and brings undesirable effects, like the increasing in class coupling and encapsulation decreasing. In addition, the conviction that assertions should have no side effects in order to be possible to monitor them, weakens the expressive power of assertion languages and makes it more difficult to avoid the above mentioned undesirable effects. In this paper we propose a pattern to the design of class contracts that is an adaptation of existing patterns of design into a declarative context - the world of assertions. The use of this pattern produces contracts that preserve low class coupling and data encapsulation. The expressive power of existing assertion languages is insufficient, however, to write these contracts. In order to fill this lack, we propose meta-assertions and formally define their syntax and semantics. In order to be possible to check contracts at runtime, we define rules for the expansion of meta-assertions that can be monitored by existing tools, and we show grammatical and semantic soundness of the expansio