Re: On pragma Precondition etc.

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

On Wed, 30 Jul 2008 19:45:03 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov schrieb:
>> On Wed, 30 Jul 2008 11:06:16 +0200, Georg Bauhaus wrote:
> 
>>> (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;
> 
>> 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
>   [some more combinations]
> 
> Any preconditions are those that you specify, of course.
> They don't magically start to exist[*],

Of course they do. If there is no explicit precondition specified for an
argument X of the type T, it still exists, and is:

   X in T [and true]

> Now the rules that say how preconditions are to be logically
> connected when overriding. Go ahead!  First,
> do you want a derived object to be a suitable argument for a
> parent's procedure?

Yep, substitutability is it all about.

> With or without preconditions, arguments
> may meet both: the type constraints that Ada has to offer,
> and the DbC constraints.

The point is that when you hang some contracted constraints on the
parameters of a subprogram, you implicitly define a set of derived types
constrained to that. The subprogram become a primitive operation of these
derived types.

[a liberal explanation of LSP skipped]

> Seen in this light,  range 1 ... 500 takes away values
> from Integer'range.  (Not surprisingly, since it is a constraint.)
> 
>     subtype My_Integer is Integer range 1 .. 500;
> 
>     overriding
>     procedure Bar(Item: My_Whatever; Num: My_Integer);
> 
> With or without DbC, it seems reasonable to me to expect
> that Bar fails when it gets an argument for Num outside
> range 1 .. 500.  Say it fails with a Constraint_Error.

No, it fails at compile time, provided, 1 .. 500 goes into the contract,
because the result is not LSP-conform.

But the question was different. It was about composition of conditions in
presence of tuples of parameters. You consider each parameter and its
contracted constraints independently, this is wrong.

> This exceptional behavior is already illustrating why the DbC
> idea of having a 'Constraint on a type makes sense.  It is
> already working for subtypes now.

Wrong. Ada constraints are not contracts. A constrained subtype when it
inherits primitive operations of the unconstrained base type, also does the
contracts of these operations in full. To be LSP-conform these contracts
shall include Constraint_Error. Otherwise, that would violate
substitutability.

Ada assumes Constraint_Error in all contracts, which is quite unfortunate
for static analysis. But it was necessary to do because its exceptions are
not contracted.

> Many shrug when they
> are more busy with the practical benefits of DbC.

I don't buy it. Practice unsupported by a sound theory is shamanism.

------
BTW, we could drop the idea of making conditions contracted. Instead of
that, we would consider constraints in the sense of Ada subtypes. Which is
the model used in Eiffel. In that case it would be all dynamic, run-time.
[Contracted constraints are more like SPARK model] But in any case the
problem would remain. We would have to introduce anonymous subtypes of
tuples of [sub]types. In both cases we need a [sub]type to associate the
constraint with. We cannot do it for a subprogram, except the case when it
has only one parameter.

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