design by contract versus doctest

[Colin Blackburn]

On Tue, 06 Apr 2004 16:08:30 +0100, Peter Hickman <peter at semantico.com>  
wrote:

> Colin Blackburn wrote:
>> Aku is correct, no checks are (necessarily) made by the function in   
>> installed code. It is the caller's responsibility to satisfy the   
>> pre-conditions.
>
> 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
--