Inheritance of contracts

C4J support full contract inheritance, both for target classes and for contracts themselves. If a class is protected by a contract, all extending classes will automatically enforce those contracts as well. Also, if a parent class is protected by a contract and an extending class is protected by another contract, the contracts will be combined for the extending class.
Furthermore, contracts defined for super interfaces to interfaces that a class implements will also be enforced.

Contract inheritance in C4J works as follows:
  • Class invariants are merged (AND'ed), except for in constructors where only the target class' own class invariants are verified.
  • Pre conditions may not be strengthened, i.e. the contract in the extending class may not disallow a method call that the contract in the parent allows.
  • Post conditions may not be weakened, i.e. the contract in the extending class may not allow more outcomes than the contract in the parent.
  • Contracts defined on the same inheritance level, e.g. by implementing two interfaces which both has contracts for the same methods, are merged.

    • If contracts don't adhere to these rules, it will be discovered during run time and a warning will be printed.