The contracts of a base type are automatically inherited by suptypes. This is very straightforward:
In addition, subtypes are allowed to extend the contracts of their base types. A subtype can:
Each of these extensions is described below.
When the same method is inherited from multiple types it is impossible to generate correct pre- and postconditions for the overriding method. The combination of preconditions (the same effect as weakening, see below) makes the overriding method too permissive about parameters passed by clients of the base types. And the combination of postconditions (the same effect as strengthening) can cause valid return values for a base type to be rejected. It is even possible that all return values are rejected because no value can satisfy the combination of postconditions.
Because of this issue inheritance of the same method from multiple types is not allowed.
Here is an example showing how the combination of pre- and postconditions would lead to unwanted results. This is the method declaration from the first base type:
/** * @pre v >= 10 * @post return <= 0 */ int someCalculation(int v);
And this is the method declaration from the second base type:
/** * @pre v <= 0 * @post return > 100 */ int someCalculation(int v);
If a class is a subtype of both base types, simply combining the pre- and postconditions will lead to the following pre- and postcondition:
/**
* @pre (v >= 10) | (v <= 0)
* @post (return <= 0) & (return > 100)
*/
public int someCalculation(int v)
{
...
}
Due to the way the preconditions are combined, a client of the first base type that invokes
someCalculation cannot only pass values greater than or equal to 10, but can also pass values
less than or equal to zero without a problem. However the values less than or equal should not be accepted
because the contract of the first base type does not allow them. If the client does pass values less than or
equal to zero it contains a bug, but this bug cannot detected.
The combination of postconditions prevents this method from returning any result at all as there is no integer that is both less than or equal to zero, and greater than one hundred.
Preconditions of a base type and a subtype are combined using a logical or to construct the actual precondition of the subtype. This makes the actual precondition less restrictive, hence the term weakening:
(precondition base type) | (precondition subtype)
Weakening the preconditions of a base type can lead to unexpected results. Code that has been tested against a weakened type could use parameter values that are not acceptable to the contracts of the base type. When the implementation is changed to an unweakened one, new contract violations can be detected. For this reason, it is advisable to never weaken preconditions. This is the same issue as inheriting preconditions from multiple base types. See inheriting the same method from multiple types above for an example.
The term strengthening is used because the way in which postconditions of a base type and a subtype are combined makes the actual postcondition of the subtype more restrictive than the original two. Postconditions are combined by using a logical and:
(postcondition base type) & (postcondition subtype)
When you strengthen a postcondition there are some things you have to take into account.
It is your responsibility to make sure postconditions in subtypes do not strengthen the postcondition in such a way that all return values become invalid.
Clients of a method that invoke strengthened methods will only receive a subset of the possible results of the original method. This means you cannot test your client with all possible return values, so bugs (instead of contract violations) might surface if the implementation is changed to one that does return all possible values.
Invariants are combined in the same way as postconditions: by using a logical and. However, the term strengthening is not used for invariants because (in general) an invariant of a subtype only has assertions about the attributes and methods introduced in that subtype. The restrictions on the members of the base type are not altered:
(invariant base type) & (invariant subtype)