design by contract versus doctest

[aku]

On 2004-04-06, 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.
> 
> > 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.
> 
>  I can think of no good reason to turn off checking of the pre and post 
>  conditions unless you can guarantee that the live system will never 
>  encounter a combination of inputs and states that have not already been 
>  tested for. You hardly need DbC for such hubris.

Isn't that where doc/unit tests can serve a purpose? In other words: 
These tests will test many combinations of states and inputs , so that
in the live system the DBC can be turned off.

> >> 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.
> 
>  Not sure I would want to state that, or rely on it. I would only go as 
>  far as saying what I have tested is guaranteed. But then I am paranoid.

"program testing can best show the presence of errors 
but never their absence" -- E. Dijkstra
His formal methods indeed *proved* and *guaranteed* that the
postcondition(s) are met IF the precondition(s) were true.