C4J supports:

Class invariants.

Pre conditions.

Post conditions, with access to return- and pre- values.

Access to private members of the tested class from the contract implementation.

Automatic detection of simple getters (i.e. "pure" methods, that don't change state), where no class invariant verifications are necessary.

It is possible to explicit mark methods as "pure" (even methods defined in interfaces).

Inheritance of contracts, i.e. extending classes inherit the parent's contracts, also overridden methods.

Contract refinement, i.e. extending classes may define their own contracts in which case they are merged with the parent contracts according to Liskov substitution principle.

Contracts for interfaces, i.e. define a contract for an Interface and all implementing classes (and their sub classes) will verify the contract.

Contracts for abstract methods, i.e. define a contract for an abstract method in an abstract class and all implementing classes (and their sub classes) will verify the contract.

Combinations of "interface contracts" and "class contracts", works like contract refinement.

Logging of contract verifications, it is possible to register loggers that are notified when contracts are verified, e.g. to support statistics gathering.

Possibility to debug contracts in your favorite IDE.

Concurrency is supported.

Contract consistency is verified so that refactorings or simple typos don't risk to hide a class' contracts.