Re: Ada vs Eiffel - Ada programmer approach

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

Dmitry A. Kazakov schrieb:
> On Tue, 26 May 2009 06:37:49 -0700 (PDT), Ludovic Brenta wrote:

>> - pre/post conditions and invariants involve run-time checks most of
>> the time (if not all the time). They slow the program down if enabled,
>> or become useless when disabled for performance.
> 
> There should be no run-time contract checks. That is inconsistent:
> 
> function Return_False return Boolean is
>     -- The contract of Return_False is to return False
> begin
>    if Is_OK (Return_False) then
>       -- Is_OK returns True if Return_False satisfies its contract
>       return True;
>    else
>       return False;
>    end if;
> end Return_False;
> 
> Now, if Return_False is OK, then Is_OK returns True and then Return_False
> returns True and so it is not OK. So is it, or is it not?

Eiffel defines the conditions for when a contract's assertions
will be tested. In particular, not every call will
trigger the tests. ;-)  So the never ending loop above is
not a problem within the Eiffel DbC framework of definitions.
(The stack may overflow, though.)