Re: Ada vs Eiffel - Ada programmer approach

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On Tue, 26 May 2009 19:59:26 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov schrieb:
> 
>> There is no loop since "contract is satisfied" is not a variable. Otherwise
>> you cannot design "by contract", obviously.
> 
> The Eiffel answer is that yes, you can do that because
> in order to get anything done, assertion checking must
> not happen at times.  That's a reasonable design, because
> there is no practical alternative. ;-)

Confusing things? (:-))

>> Ada's static typing system and SPARK do it right.
> 
> SPARK imposes limitations that are not present when employing
> DbC.

More checks you want to do more language limitations you need. Nothing is
for free.

> SPARK cannot replace DbC, or improve it, and vice versa,
> basically because DbC (not used as static assertions only) and
> SPARK are largely incommensurable.

Nope, the point is not how many checks, it is about consistency of checks.
SPARK does it consistently, Eiffel does not.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de