Re: On pragma Precondition etc.

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

On Wed, 30 Jul 2008 11:22:38 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov schrieb:
>> On Tue, 29 Jul 2008 17:55:18 +0200, Georg Bauhaus wrote:
> 
>>> What if one precondition states a relation between two suprogram
>>> parameters, or between properties of two suprogram parameters?
>> 
>> This case is equivalent to full multiple dispatch. Ada does not have it. If
>> it had multiple dispatch then it would clearer how to deal with the
>> corresponding contracts (=conditions).
> 
> Design by Contract™ has been made to be a *design* tool.

This applies to everything.

> It starts from the simple truth that we will likely think
> about pre/post of subprograms once the language suggests we
> can. The checking mechanism supports us by checking our
> assumptions as good as it possibly can do this.
> 
> DbC is not meant to be reduced to a static proof tool.

OK, that is another discussion.

No, correctness is a property of a given program. As such it is static per
the definition of <=> correctness of P may not depend on any of the
run-time states of P <=> P cannot be correct in one of its states and
incorrect in another <=> a correct P traverses only the states where P is
correct, etc.

Contracts *when* thought as statements about the correctness are static. I
don't care about the meaning of DbC™ as a registered trademark. I care
about Ada. (:-)) 

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