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).