True but the caller does not check the pre-conditions, that is done in
the called. The called does not trust the caller to get things right,
hence the contract.
You have DbC completely wrong. The contract is there to be trusted. As far
as I can tell you are seeing what looks like a parameter check at the
start of a method and assuming that that is a defensive check against the
caller providing incorrect parameters. That is not what the preconditions
are.
The preconditions (and other constraints) were developed early in the
design process. In fact, they guided the design process.
The preconditions are ultimately coded (in Eiffel) but they are not part
of the implementation of the method. They are not there to check for
errors in production code. They are there to specify the contract, to
specify what the caller must provide for the outcome to be guaranteed.
They form part of the documentation whereas the implementation code
(following do in Eiffel) does not. Writers of calling code can examine the
pre and post-condition to know what they must do and what they can expect
if the do things right.
In fact some pre-conditions cannot be expressed computationally, there are
put in as comments, and so cannot be checked by the called method.
It is entirely the responsibility of the caller to check that the
preconditions are satisfied, by providing correct parameters, say. It
might do this explicitely, or implicitely but it is the caller that must
satisfy those conditions. The called routine has no responsibility to
check the preconditions, in fact it has every reason to expect those
preconditions to be satisfied by the caller because that *is* the contract.
Colin
--
