Re: On pragma Precondition etc.

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

On Wed, 30 Jul 2008 11:06:16 +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).
> 
> How about this: For the purpose of expressing the contract
> of a subprogram, dream up its "contract-type".

This type is obviously a tuple of the parameters of Foo.

> Base this type on
> 
> (1) the precursor's contract-type (up the derivation hierarchy)
> (2) the profile
> 
> So given
> 
>     function Foo(X, Y: Integer) return Whatever;
> 
> denote the precondition of its "contract-type" by something like
> 
>     Foo'Precondition;

Naming does not solve the problem.

In presence of:

   subtype My_Integer is Integer range 1..500;
   type My_Whatever is new Whatever with private;

what are the preconditions of Foo defined on the tuples:

Integer x My_Integer x Whatever
My_Integer x Integer x Whatever
Integer x My_Integer x Whatever
My_Integer x My_Integer x Whatever
Integer x My_Integer x My_Whatever
My_Integer x Integer x My_Whatever
Integer x My_Integer x My_Whatever
My_Integer x My_Integer x My_Whatever

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