design by contract versus doctest

[Peter Hickman]

Colin Blackburn wrote:

> On Tue, 06 Apr 2004 12:41:45 +0100, Peter Hickman <peter at semantico.com>  
> wrote:
> 
>> Looking at the Eiffel site the contract is enforced within the called  
>> function.
> 
> 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.

>> put (x: ELEMENT; key: STRING) is
>>      -- Insert x so that it will be retrievable through key.
>>      require
>>          count <= capacity
>>          not key.empty
>>      do
>>          ... Some insertion algorithm ...
>>      ensure
>>          has (x)
>>          item (key) = x
>>          count = old count + 1
>>      end
> 
> 
> 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). 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.

The require is a contract between the caller and the called. The ensure 
is, in effect, a contract between the called and itself. You might get 
the require section correct, this would mean that valid parameters have 
been passed to the called by the caller. But this is no guarantee that 
the do section doesnt screw things up.

Which is why we have the ensure section, this checks that the do section 
has not done anything stupid.

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.

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.