Re: On pragma Precondition etc.

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

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[*], and DbC adds no
magic for excluding subtle contradictions. Of course,
Boolean expressions involving the subprogram parameters
will be checked by the compiler. Just like with Ada; they
are checked now,

    pragma Precondition(<boolean expression>);

with some rules for what can be part of <boolean expression>.
No more, no less.

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? With or without preconditions, arguments
may meet both: the type constraints that Ada has to offer,
and the DbC constraints. Let's see,


    type Whatever is tagged private;

    procedure Foo(Item: Whatever);
      -- pre: permissible values of Item


    type My_Whatever is new Whatever with private;

    overriding
    procedure Foo(Item: My_Whatever);
      --  pre: permissible values at least as above

    X: Whatever'Class := ...;
begin

    Foo(X);

end;

In this case object X must satisfy the parent's preconditions
for calling Foo and the child's preconditions for calling its
Foo.  So the rule would be to "weaken" the precondition in child
overridings. The phrase "at least" from the comment on the
overridden Foo translates into "or else". Theory then says,
"When overriding, only add permissible values, do not remove any."

For extended records I find this rule strikingly obvious, because
every component added to the parent type will enlarge the set of
values available in the child type.

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.

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.

With or without DbC, you can always be troubled by the typical
variance problems, for which, as you  have said before, there is
no universally good solution.  Many shrug when they
are more busy with the practical benefits of DbC.



___
[*] Sofcheck's tools can extract a number of assertions.
There is also an Eiffel(?) tool doing similar things.
But this is beside the point when you want to design a
provable DbC component (typically, a tagged type).
It adds nothing in the sense of DbC, just more assertions
for us that help with analyzing our programs which would
typically lack assertions.