Inheritance

Contracts are divided into several semantic parts:

• State machine

• List of invariants

• Pre-conditions

• Post-conditions

Each of these parts can be inherited in separate ways in derived classes, unless a matching part has been found in the derived class.

If you specify invariants for a class, they override the invariants defined for any base class. Similarly, a state machine description for a class overrides any state machine definition inherited from a base class.

If a class inherits from several base classes for which a class contract is defined, but does not define any invariant, the base class's invariants are merged. Similarly, if no state transition is defined, a state-transition is maintained for every sub-object inheriting a tested base class.

If you want to define a contract for a class, but not all of its base classes are associated to a contract, then you should use invariants and state transitions with care, because the methods inherited from the non-tested classes are not instrumented. In this situation, define a contract, even empty, for every base class of the class you want to test. A warning is generated during the instrumentation if such a case is encountered.