Ease of use

Adding class invariants, pre conditions, and post conditions to your regular Java objects is easy with C4J. Contracts for a class (the target) are implemented in a separate class (the contract). The contract is linked to the target at compile time using an annotation, and the actual contract verification code is tied to the target using instrumentation during class loading at run time.

Contracts implementations have a reference to the instance of the target that it is verifying. This reference is used to implement class invariants. Pre and post conditions also have access to the target reference, as well as the parameters that the target method is invoked with. If the contract class extends a C4J ContractBase class, post conditions will also have access to method return values, and pre invokation values (i.e. values of instance variables in the target prior to the method invocation).

There are several reasons for defining contracts in plain Java and in a separate class:

You don't have to learn any new language constructs.

You will get help from your IDE when implementing the contract (as opposed to implementing contracts in comment blocks).

It is possible to put break points in your contract if you want to debug them.

Separating the contract code from the application makes it possible to remove the risk of accidentally deploying the contracts together with your application.

You get to keep your beautiful code nice and clean without all the ugly assertions.