In C4J, contracts for a class (called the target) are implemented in a separate class (the contract). The contract class can by of any type, in any location. However, since you usually do not want to deploy your contracts together with your final product, it is a good idea to keep them in a separate source tree (or even a separate project).
The contracts are tied to their targets via the ContractReference annotation. The simplest example of a target class and its contract, wich both do nothing, is:
@ContractReference(contractClassName="DummyContract")
public class Dummy {}
public class DummyContract {}
This works if the Dummy and DummyContract classes are defined in the same package. If they are not, you must supply a fully qualified class name as the value for the contractClassName attribute.
How to write actual contracts for classes and methods is explained in the sections Class Invariants, Pre and Post Conditions andTarget Members.
Your contract class gains access to its target by defining a non-standard constructor, which has as its only argument a target object. This enables the contract to access all but the private members of its target:
@ContractReference(contractClassName="DummyContract")
public class Dummy {
...
}
public class DummyContract {
Dummy m_target;
public DummyContract(Dummy target) {
m_target = target
}
...
}
If you need to get your hands on private members, see Target Members.
The package net.sourceforge.c4j contains the generic class ContractBase<T> which is designed in order to give your contracts access to pre invocation values, method return values and private members of the target class. Additionally, you can register a Logger object to track contract verifications, see also the Logging section, for further details.