Under the hood

C4J use the -javaagent switch that was added to Java 1.5. The javaagent concept provides a way to hook on to the class loader, and return custom byte code for any class that is loaded by the Java runtime. C4J contains an instrumentor class that instruments all loaded classes that are protected by a contract class.

Javassist, an extremely easy to use byte code library, is used for instrumenting.

The C4J instrumentor class does the following on each class that is loaded:
  • Does the target class or any of it's parents contain a valid ContractReference annotation? Or is an external contract attached to the target class or any of it's parents? If not, don't instrument this class.
  • If the target class has a direct contract (as opposed to inherited from a parent), insert a private member of the contract class in to the target class.
    For each method in the target class:
  • If a precondition exists in the contract or the parents contract, add a call to it at the beginning of the method.
  • If a postcondition exists in the contract or the parents contract, add a call to it at the end of the method.
  • If a classInvariant exists in the contract or the parents contract, add a call to it at the end of the method.
    For all of the above:
  • If both a direct contract and an inherited contract exist for the method, add method calls to both, according to the rules of contract inheritance.

Apart from this C4J provides a number of features to facilitate the writing of contract classes.
These features can be accessed by using C4J's annotations and static methods.

Please note that the syntax of first generation C4J contracts is not compatible to the syntax of second gneration C4J contracts as the C4J syntax had to be changed in order to fulfill agility requirements. The second generation C4J version number has a new meaning: The version number now corresponds to the Java version number starting from which C4J is upward compatible, i.e. C4J 6.x is compatible to Java 6, Java 7 and so on.

Please be aware of the fact that for contract inheritance C4J deals in a way with the Liskov substitution principle (LSP) that is different to Eiffel.

In Eiffel contract inheritance is implemented like this:
  • superclass preconditions and subclass preconditions of the same method are concatenated using OR.
  • superclass postconditions and subclass postconditions of the same method are concatenated using AND.
  • superclass class invariants and subclass class invariants are concatenated using AND.
    • Opposed to that, first generation C4J implements the inheritance of contracts like this:
  • superclass preconditions and valid subclass preconditions of the same method are concatenated using AND.
  • superclass postconditions and valid subclass postconditions of the same method are concatenated using AND.
  • superclass class invariants and subclass class invariants are concatenated using AND.

    • According to LSP valid subclass preconditions are preconditions which do not strengthen the superclass preconditions, i.e. the subclass precondition always has to prove true when the superclass precondition proves true. This is checked by C4J at runtime using the AND concatenation. If a subclass precondition is detected to break that rule at runtime, a C4J ERROR message is logged and the affected subclass precondition is discarded.

    According to LSP valid subclass postconditions are postconditions which do not weaken the superclass postconditions, i.e. the subclass postcondition always has to prove false when the superclass postcondition proves false. This is checked by C4J at runtime using the AND concatenation. If a subclass postcondition is detected to break that rule at runtime, a C4J ERROR message is logged and the affected subclass postcondition is discarded.

    Please note that Eiffel does not detect invalid preconditions as they are concatenated using OR. That is the reason why Richard Mitchell and Jim McKim give the following guideline in their book Design by Contract by Example:

    Guideline 4: To support redefinition of features, guard each postcondition clause with its corresponding precondition.


    A questionable guideline as it creates a lot of redundancy and makes contracts complex.

    C4J contracts do not need such a questionable guideline as the AND concatenation of preconditions guarantees the ability of redefining (overriding) features (methods) in subclasses.

    Second generation C4J is even more rigid and implements the inheritance of contracts like this:
    • superclass preconditions of a method are not allowed to be extended by any subclass.
    • superclass postconditions and subclass postconditions of the same method are concatenated using AND.
    • superclass class invariants and subclass class invariants are concatenated using AND.
    The rationale of that even more rigid implementation for precondition inheritance is:
    • A precondition can only prove false or true.
    • Case 1: The superclass precondition proves false. An AssertionError has to be thrown as a precondition violation is detected regardless whether the subclass precondition may prove true or false. The AND concatenation of superclass and subclass preconditions is perfectly right to implement that expected behaviour.
    • Case 2: The superclass precondition proves true. For this case it matters, whether the subclass precondition proves true or false.
    • Case 2.1: The subclass precondition proves false. That is a LSP violation as the subclass precondition strengthens its superclass precondition.
    • Case 2.1: The subclass precondition proves true. That is in accordance with the LSP as the subclass precondition does not strengthen its superclass precondition. There are two subcases for this case.
    • Case 2.1.1: The subclass precondition equals its superclass precondition, i.e. the subclass precondition always has to prove true when the superclass precondition proves true.
    • Case 2.1.2: The subclass precondition weakens its superclass precondition, the subclass precondition always has to prove true when the superclass precondition proves true.
    • As there is no difference in the effective result of case 2.1.1 and case 2.1.2 you can merge them to one constraint: As LSP says that preconditions may not be strengthend C4J demands that superclass preconditions are not allowed to be extended which has the same effective result.
    As C4J also supports multiple inheritance of interfaces. The implementation is the same for first and second generation C4J and looks like that:
    • all superinterface preconditions of the same method are merged using AND.
    • all superinterface postconditions of the same method are merged using AND.
    • all superinterface class invariants are merged using AND.
    The C4J implementation of contract inheritance is in accordance to the LSP paper of Barbara Liskov Behavioral Subtyping Using Invariants and Constraints (1999).

    Fore more information about the discussion of that topic please have a look at Jonas Bergströms answer in the first generation C4J forum (November 2006).