Under the hood

C4J use the new -javaagent switch that was added to Java 1.5. It 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 contain an "instrumentor class" that instruments all loaded classes that defines a ContractReference annotation with contract verification code.
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? 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 pre_<method-name> exists in the contract or the parents contract, add a call to it at the beginning of the method.
  • If a post_<method-name> 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 there is more stuff going on if the contract extends ContractBase; return- and pre- values are made available to post conditions, and logging hooks are notified of all contract checking.