design by contract versus doctest

[Colin Blackburn]

On Tue, 06 Apr 2004 13:51:29 +0100, Peter Hickman <peter at semantico.com>  
wrote:

> Colin Blackburn wrote:
>
>>  Only while checking is turned on. It is a design philosophy. You  
>> specify  the pre and post-conditions before code is even thought of, it  
>> is part of  the design.
>
> Sure but the checks are still made by the function that is called not by  
> the caller of the function. Which was my point and contrary to what aku  
> said.
>
> aku wrote:
>  > But in "design by contract" this responsibility is squarely
>  > on the shoulders  of the caller, and is *not* checked in
>  > the function.

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.

>>   This says that *if* the pre-conditions are met (by the caller) *then*  
>> the  post-conditions will be guaranteed to be met (by the called  
>> method.)
>
> No this is not entirely true, the require and ensure and both parts of  
> the contract. The function will not be called if the require section is  
> found to be false (such as count being greater than capacity).

In the installed code the pre-conditions are not necessarily implemented  
therefore the function cannot refuse to run since it does not know its  
pre-condition at this stage.

> Then after the function is executed (the do portion) then second half of  
> the contract is checked, the ensure section. If these conditions fail  
> then the contract is broken and the call fail just as if the require had  
> failed.

Again, not necessarily in the installed code since the post-conditions are  
not known. However, the result will be guaranteed if the preconditions are  
met even in the installed code since the code wil have been designed  
properly.

> Take this as an example (hacked at the keyboard, probably wont work)
>
> double (x: ELEMENT) is
> 	require
> 		x > 0
> 	do
> 		x = x * -2
> 	ensure
> 		x > 0
> 	end
>
> If you call it with double(-12) then the require section fails. If you  
> call it with double(12) then the require section passes but the do  
> section is creating a negative number and so the ensure section fails.

Your post-condition is incorrect. The method must ensure that the result  
is double the input parameter if that parameter is greater than zero.  
Howver, yes in this case the ensure will barf but this is at the design  
stage and is there to ensure you get the method right in the first place.  
When you deliver this routine the ensure will not be implement but by then  
you will have corrected your typo.

> Getting the require section to pass is no guarantee that the  
> post-conditions (ensure section) will be met, the do section is code  
> like anything else and may get things wrong.

In correctly developed DbC that is precisely what is guaranteed. The  
post-condition is *guaranteed* if the pre-condition is met. It is a design  
tool.

Colin
--