Version 1.4 of ai12s/ai12-0272-1.txt

Unformatted version of ai12s/ai12-0272-1.txt version 1.4
Other versions for file ai12s/ai12-0272-1.txt

!standard 6.1.1(1/5)          18-08-31 AI12-0272-1/03
!standard 6.1.1(39/5)
!standard 7.3.3(1/5)
!standard 7.3.3(2/5)
!standard 7.3.3(8/5)
!standard 7.3.4(5/5)
!standard F.1(1)
!class Amendment 18-04-09
!status Amendment 1-2012 18-07-11
!status ARG Approved 10-0-1 18-06-23
!status work item 18-04-09
!status received 18-04-05
!priority Low
!difficulty Easy
!subject Contracts for generic formal parameters
!summary
Pre and Post are allowed on generic formal (nonabstract) subprograms.
Default_Initial_Condition is allowed on generic formal private types.
!problem
Ada has a strong "contract model" for generic units, which makes it possible to reason about generic bodies without knowing anything about the properties of the actual types.
This model is fairly weak for formal subprograms, where even the subtypes of the subprogram profile are ignored. This can make it hard to reason in generic bodies.
We have allowed contracts on access-to-subprogram types, which have a similar situation (and sometimes, similar uses) as generic formal subprograms. It seems inconsistent to allow one but not the other.
Similarly, contracts that are allowed on private types probably should be allowed on generic formal private types.
!proposal
Allow Pre and Post to be specified on nonabstract generic formal subprograms.
!wording
Modify 6.1.1(1/5): [from AI12-0220-1]
For a noninstance subprogram{ (including a generic formal subprogram)}, a generic subprogram, or an entry, or an access-to-subprogram type, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
AARM Proof: A generic formal subprogram is a subprogram, and there are no rules to prevent such use.
Add after 6.1.1(39/5): [from AI12-0220-1]
Redundant[For a call on a generic formal subprogram, precondition and postcondition checks performed are as determined by the subprogram or entry denoted by the actual subprogram, along with any specific precondition and specific postcondition of the formal subprogram itself.]
AARM Proof: This follows from the general dynamic semantics rules given above, but we mention it explicitly so that there can be no doubt that it is intended.
[Editor's note: This follows from the rules of 6.1.1(37/4), but we can't give paragraph references in AARM notes.]
Modify 7.3.3(1/5) [from AI12-0265-1]
For a private type or private extension {(including a generic formal type)}, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1):
Modify 7.3.3(2/5) [from AI12-0265-1]
This aspect shall be specified by an expression, called a *default initial condition expression*. Default_Initial_Condition may be specified on a private_type_declaration{,}[ or] a private_extension_declaration{, a formal_private_type_definition, or formal_derived_type_definition}.
Add after 7.3.3(8/5): [from AI12-0265-1]
Redundant[For a generic formal type T, default initial condition checks performed are as determined by the actual type, along with any default initial condition of the formal type itself.]
AARM Proof: This follows from the general dynamic semantics rules given above, but we mention it explicitly so that there can be no doubt that it is intended.
[Editor's note: This follows from the rules of 7.3.3(8/5), but we can't give paragraph references in AARM notes.]
Modify 7.3.4(5/5): [from AI12-0187-1]
For a {nonformal} private type, {nonformal} private extension, or full type that does not have a partial view, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
Modify F.1(1)
{The representation attribute }Machine_Radix may be specified for a decimal first subtype (see 3.5.9) via an attribute_definition_clause; the expression of such a clause shall be static, and its value shall be 2 or 10. A value of 2 implies a binary base range; a value of 10 implies a decimal base range.
!discussion
We do not require any matching of contracts. This follows the model of access-to-subprogram types; the contracts are dynamically checked and no static rules are enforced. Since access-to-subprogram and formal subprograms are often used for similar purposes, it would be odd to have different rules for them.
---
Note that the dynamic model for generic formal subprograms is identical to the situation where the programmer had defined a new routine in the generic package specification:
generic type Foo is ... with function Reduce1 (Obj : Foo) return Integer with Post => Reduce1'Result in -9 .. 9; with function Reduce2 (Obj : Foo) return Integer; package Gen is ... function Local_Reduce2 (Obj : Foo) return Integer with Post => Local_Reduce2'Result in -9 .. 9 is (Reduce2(Obj)); ... end Gen;
If the actual subprogram for Reduce1 and Reduce2 is the same, then a call on Reduce1 has the same semantics as a call on Local_Reduce2. Thus, a compiler can always generate a wrapper for the formal subprogram if other implementations are unavailable.
This is essentially the same model that is used for access-to-subprogram types.
---
Note that Pre'Class and Post'Class aren't allowed because a generic formal subprogram is never primitive for a type (not even a formal abstract subprogram -- it's dispatching but not primitive). Also, Pre and Post aren't allowed for abstract subprograms, so no contracts are allowed for formal abstract subprograms.
One could imagine allowing Pre'Class and Post'Class on formal abstract subprograms, but since it is not clear how to reconcile those with the static binding model for class-wide contracts, this is not allowed.
---
Note that AI12-0064-2 allowed (unintentially?) aspects that are neither operational nor representation to be used on generic formal parameters. So we just need wording to reinforce that is meant on these aspects. We also need to check that other aspects aren't allowed on formal parameters. Here's the list of such aspects:
(1) Pre/Post - OK on formal subprograms - see above; (2) Pre'Class/Post'Class - Not allowed, see above; (3) Static_Predicate - Not allowed, a formal is never static; (4) Dynamic_Predicate - Not allowed, only allowed on type_declarations or
subtype_declarations. (Probably OK to allow, but would require rewording, did not investigate.)
(5) Type_Invariant/Type_Invariant'Class - Not allowed, since the places it
is allowed are given syntactically. Don't want it, either (see below).
(6) Default_Initial_Condition - Not allowed, since the places it
is allowed are given syntactically. But we do want it, so fixed that above.
(7) Stable_Properties/Stable_Properties'Class for types - We don't want to
allow it (see AARM 7.3.4(6.a/5)), but there's no wording to that effect. We add the missing wording here.
(8) Stable_Properties/Stable_Properties'Class for subprograms - Not allowed,
formal subprograms are never primitive.
(9) Machine_Radix - ??? This should be a representation aspect, but that's not
mentioned in F.1. we fix that here.
---
We don't want Type_Invariants to be used on formal subprograms. We do this because the rules for checking a type invariant apply to the unit in which it is defined - so it doesn't make sense for a generic formal (which is declared in a different unit than the actual).
!corrigendum 6.1.1(1/5)
Replace the paragraph:
For a noninstance subprogram, a generic subprogram, an entry, or an access-to-subprogram type, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
by:
For a noninstance subprogram (including a generic formal subprogram), a generic subprogram, an entry, or an access-to-subprogram type, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
!corrigendum 6.1.1(39/5)
Insert after the paragraph:
For a call via an access-to-subprogram value, precondition and postcondition checks performed are as determined by the subprogram or entry denoted by the prefix of the Access attribute reference that produced the value. In addition, a precondition check of any precondition expression associated with the access-to-subprogram type is performed. Similarly, a postcondition check of any postcondition expression associated with the access-to-subprogram type is performed.
the new paragraph:
For a call on a generic formal subprogram, precondition and postcondition checks performed are as determined by the subprogram or entry denoted by the actual subprogram, along with any specific precondition and specific postcondition of the formal subprogram itself.
!corrigendum 7.3.3(0)
Insert new clause:
Just enough to force a conflict. The actual text is found in the conflict file.
!corrigendum 7.3.4(0)
Insert new clause:
Just enough to force a conflict. The actual text is found in the conflict file.
!corrigendum F.1(1)
Replace the paragraph:
Machine_Radix may be specified for a decimal first subtype (see 3.5.9) via an attribute_definition_clause; the expression of such a clause shall be static, and its value shall be 2 or 10. A value of 2 implies a binary base range; a value of 10 implies a decimal base range.
by:
The representation attribute Machine_Radix may be specified for a decimal first subtype (see 3.5.9) via an attribute_definition_clause; the expression of such a clause shall be static, and its value shall be 2 or 10. A value of 2 implies a binary base range; a value of 10 implies a decimal base range.
!ASIS
[Not sure. It seems like some new capabilities might be needed, but I didn't check - Editor.]
!ACATS test
ACATS B- and C-Tests are needed to check that the new capabilities are supported.
!appendix

From: Randy Brukardt
Sent: Thursday, April 5, 2018  8:01 PM

When we discussed AI12-0220-1 on Monday, it was immediately concluded that 
Pre/Post for generic formal subprograms was "a separate issue for a separate
AI". What we didn't discuss further was whether we wanted such an AI. I'd be
willing to write up such an AI, but I'd like to have some idea of whether we
actually are interested first.

It seems that a lot of the same uses occur for formal subprograms and for 
access-to-subprogram types. I would not want an incentive to use 
access-to-subprogram parameters when a formal subprogram would be an
equivalent choice (in particular, inside of a generic unit).

As Steve noted in the e-mail discussion, the subtypes (and thus predicates)
of a formal subprogram are effectively ignored and thus cannot be relied upon.
Thus, we don't have any way to declare useful contracts for such entities
(even for things like ranges).

Note if there is no checking, one can get the effect by declaring a local 
subprogram that calls the formal:

     generic
        type Foo is ...
        with function Reduce (Obj : Foo) return Integer
           with Post => Reduce'Result in -9 .. 9;
     package Gen is
        ...

could be replaced by:

     generic
        type Foo is ...
        with function Reduce (Obj : Foo) return Integer;
     package Gen is
        ...
        function Local_Reduce (Obj : Foo) return Integer
           with Post => Local_Reduce'Result in -9 .. 9 is (Reduce(Obj));  

and this would have the same semantics.

This workaround has all of the obvious problems (need for an extra
declaration, easy to forget to call the extra routine rather than the
original) and also would be harder to do static checks for (as it would add 
an additional level of declaration without any information). In particular,
the instantiator has no guidance that a function that can return 42 is not 
expected by the generic.

Ideally, one would include matching checks for the actual subprogram during 
the instantiation, but we probably wouldn't want to do those for instances 
for the same reason that we didn't try to do them for 'Access. (Mainly that
if we did them, they'd necessarily have to be fairly conservative, and that
would prevent SPARK from doing better on similar checks -- even if SPARK
could tell that a given subprogram's definition is OK, it couldn't be used
because Ada would reject it.)

Before doing anything, I would like to know how SPARK deals with formal 
subprograms. Does it allow contracts on them, and if so, how are they 
interpreted.

I'd also like to know whether or not checking is expected on the instance.
(It's not particularly hard to define using conformance, but it's not clear
how likely it would be to cause issues in practice.)

Thoughts??

****************************************************************

From: Steve Baird
Sent: Friday, April 6, 2018  8:36 PM

> Before doing anything, I would like to know how SPARK deals with 
> formal subprograms. Does it allow contracts on them, and if so, how 
> are they interpreted.

SPARK sidesteps this issue by not trying to prove things about generic units;
instead SPARK focuses on instances (including instance bodies).

CodePeer takes the same approach; generic units are not analyzed but instances
are.

So I don't think this proposal would be a big deal (either positive or 
negative) for either SPARK or CodePeer.

> I'd also like to know whether or not checking is expected on the instance.

I'm not sure what you are asking here.

Are you talking about static conformance checking of some kind, somehow 
checking that the actual subprogram already has the desired PPC?
I wouldn't expect anything like that.

Or are you talking about the question of whether PPC checks are performed at 
runtime in a case like

    generic
      with procedure P (X, Y : in out Integer) return Integer with
        Pre => ..., Post => ...;
    package G is
       procedure Ren (X, Y : in out Integer) renames P;
    end G;

    procedure PP (X, Y : in out Integer); -- no PPC

    package I is new G (P => PP);

    procedure Foo (X, Y : in out Integer) is
    begin
       PP (X, Y); -- clearly no PPC check here

       I.Ren (X, Y); -- PPC check here?
    end;

? It would be something new if the two calls in the preceding example behaved 
differently at runtime (i.e., if only the second call performs PPC checks).
This example does suggest that this AI might be less straightforward than it
seems at first.

Along those lines, how would name resolution work? Could a precondition for a
formal subprogram of a generic package reference something declared in the
visible part of the package?

> As Steve noted in the e-mail discussion, the subtypes (and thus 
> predicates) of a formal subprogram are effectively ignored and thus 
> cannot be relied upon.

Given that Ada does not require subtype conformance between a formal
subprogram and a corresponding actual, adding postconditions seems somewhat
odd. We'll let you write explicit PPCs for these guys, but we won't let you
assume the usual implicit contract (i.e., Pre => in and in-out param values
belong to their respective subtypes, Post => same for in-out and out params
and for a function result).

This seems inconsistent to me. Would we also want to introduce a "Conforming" 
aspect for formal subprograms indicating that subtype conformance is required 
for a corresponding actual?
Perhaps that question doesn't belong in this AI (there would be details to
work out regarding the "conventions must match" part of subtype conformance).

> Thoughts??

I can see how a precondition like the one in

    generic
       type File is limited private;
       with function Open_For_Reading (F : File) return Boolean;
       with function Read_Line (F : File) return String
         with Pre => Open_For_Reading (F);
       ...
    package G is
      ...
    end;

could help clarify/document/define an interface.
The question is whether it is worth the added complexity.

****************************************************************

From: Tucker Taft
Sent: Thursday, April 5, 2018  9:07 PM

Because things are re-checked in each instance in SPARK (and CodePeer), it
would not seem unreasonable to take the same general attitude about
pre/post-conditions, though that clearly creates contract model violations,
since we are re-checking generic bodies of each instance.

I would say we should create the AI, but leave it low priority for now, and
take it up again for Ada 2028 if we have interest in it.

****************************************************************

From: Randy Brukardt
Sent: Friday, April 6, 2018  9:54 PM

> > I'd also like to know whether or not checking is expected
> on the instance.
> 
> I'm not sure what you are asking here.
> 
> Are you talking about static conformance checking of some kind, 
> somehow checking that the actual subprogram already has the desired 
> PPC?
> I wouldn't expect anything like that.

Yes, that's what I was thinking about. But since it would be inconsistent with
the rest of the language, probably it shouldn't be included. (SPARK probably
ought to check such things, though, although if the model is to forget the
contract model, it really doesn't matter.)

> Or are you talking about the question of whether PPC checks are 
> performed at runtime in a case like
> 
>     generic
>       with procedure P (X, Y : in out Integer) return Integer with
>         Pre => ..., Post => ...;
>     package G is
>        procedure Ren (X, Y : in out Integer) renames P;
>     end G;
> 
>     procedure PP (X, Y : in out Integer); -- no PPC
> 
>     package I is new G (P => PP);
> 
>     procedure Foo (X, Y : in out Integer) is
>     begin
>        PP (X, Y); -- clearly no PPC check here
> 
>        I.Ren (X, Y); -- PPC check here?
>     end;
> 
> ? It would be something new if the two calls in the preceding example 
> behaved differently at runtime (i.e., if only the second call performs 
> PPC checks). This example does suggest that this AI might be less 
> straightforward than it seems at first.

Of course the checks would be different. The recently approved AI12-0220-1
does exactly this, you can write precisely this example using
access-to-subprogram types:

    type PPtr is procedure (X, Y : in out Integer) return Integer with
       Pre => ..., Post => ...;

    procedure PP (X, Y : in out Integer); -- no PPC

    Pobj : PPtr := PP'Access;

     procedure Foo (X, Y : in out Integer) is
     begin
        PP (X, Y); -- clearly no PPC check here
 
        Pobj.all (X, Y); -- PPC check here
     end;

> Along those lines, how would name resolution work? Could a 
> precondition for a formal subprogram of a generic package reference 
> something declared in the visible part of the package?

I'd expect just the things allowed in the formal part + parameters. But you
are right that some thought would be required to see if that enough.
Definitely wouldn't want anything inside of the package (lest you get 
recursive dependence between the formals and the instantiated routines).

> > As Steve noted in the e-mail discussion, the subtypes (and thus
> > predicates) of a formal subprogram are effectively ignored and thus 
> > cannot be relied upon.
> 
> Given that Ada does not require subtype conformance between a formal 
> subprogram and a corresponding actual, adding postconditions seems 
> somewhat odd. We'll let you write explicit PPCs for these guys, but we 
> won't let you assume the usual implicit contract (i.e., Pre => in and 
> in-out param values belong to their respective subtypes, Post => same 
> for in-out and out params and for a function result).
> 
> This seems inconsistent to me. Would we also want to introduce a 
> "Conforming" aspect for formal subprograms indicating that subtype 
> conformance is required for a corresponding actual?

In that case, a PPC check would also make sense. (It's not really that hard 
to define, it just would be a bit inflexible in that the "parts" would have
to fully conform.)

> Perhaps that question doesn't belong in this AI (there would be 
> details to work out regarding the "conventions must match"
> part of subtype conformance).

Right. And if you are doing that sort of matching, you really need contract 
conformance as well. That's clearly messier than just adding some additional
checking possibilities.
 
> > Thoughts??
> 
> I can see how a precondition like the one in
> 
>     generic
>        type File is limited private;
>        with function Open_For_Reading (F : File) return Boolean;
>        with function Read_Line (F : File) return String
>          with Pre => Open_For_Reading (F);
>        ...
>     package G is
>       ...
>     end;
> 
> could help clarify/document/define an interface.
> The question is whether it is worth the added complexity.

To me, this is precisely the same question as whether they are valuable on 
access-to-subprogram types. The constructs are often used for similar things.
So it's certainly worth it unless there is some complexity that I don't know 
about (this doesn't seem any harder than the access-to-subprogram was).

****************************************************************

From: Randy Brukardt
Sent: Friday, April 6, 2018  10:08 PM

> Because things are re-checked in each instance in SPARK (and 
> CodePeer), it would not seem unreasonable to take the same general 
> attitude about pre/post-conditions, though that clearly creates 
> contract model violations, since we are re-checking generic bodies of 
> each instance.

...in SPARK/Codepeer, not in Ada (which isn't doing any static checking at
all, and if it did [as Steve sort of proposed], then it would solely be at
the instance). I can't really care if other people's tools mess up the Ada
model -- that's out of our hands in any case.

> I would say we should create the AI, but leave it low priority for 
> now, and take it up again for Ada 2028 if we have interest in it.

Well, as this is a "directly related" to a WG 9 instruction ("improve 
contracts"), if it exists it would "leap" ahead of any non-easy AIs that
aren't "directly related". So we'd have to have it on the agenda at least
once (although we could explicitly decide to put it on Hold then).

Moreover, the basic version as discussed is probably in the "easy" category:
if there is no static matching required, the rule changes needed would be just
a few places to make it clear that it is allowed to give Pre/Post in formal
subprograms (substantially less than the access-to-subprogram rules in the 
recently approved AI12-0220-1, which required more wording since a type is 
not any form of subprogram) [presumably also renames-not-as-body].
I'd have to verify that, of course, which would take some effort.

I suspect that the discussion would come down to a yes/no type of vote, again
mirroring what happened with AI12-0220-1.

The version involving static matching of subtypes and contracts (that Steve
suggests in his mail) is a more complex beast, probably best left for Ada
2028. (I'd suggest a version for access-to-subprogram as well, so that
contract matching would be an option for those who want it.) I could write up
an empty version of this, mainly to keep the idea for the future -- I'd put it
into the Hold vote.

***************************************************************

From: Tucker Taft
Sent: Saturday, April 7, 2018  5:32 AM

I am easy either way.  I don't think contracts are critical on generic formals
at this point, but I agree that in the long run they make sense.  And as you
point out, enhanced contracts are one of our key goals for 202X.  And I suppose
someone coming from outside would naturally ask: "why no contracts on generic
formals?".  I suppose Default_Initial_Condition would also make sense on a
generic formal private type or extension, as it is very much like a
Postcondition.

***************************************************************

From: Randy Brukardt
Sent: Tuesday, April 10, 2018  12:18 AM

Having looked at the wording, I've convinced myself that we are already
allowing (unintentionally) Pre/Post on formal subprograms.

As such, the AI I'm writing is more "we meant that" rather than allowing 
something new. If we *don't* want to allow this, we'll have to add some
wording to make that happen.

Specifically, we have a blanket rule that says that operational and 
representation aspects are not allowed on generic formal parameters
(13.1(9.4/5) - this was moved recently, not sure the old paragraph but it's
an old rule). We used to have a similar rule for aspect specifications in
general, but we got rid of it when aspect Nonblocking was defined on formal
subprograms.

So for any aspects that aren't specified as either operational or 
representation and that don't specifically have an prohibition against formal
parameters, we seem to have allowed using the aspect on a formal parameter.

For Pre/Post/Default_Initial_Condition/Dynamic_Predicate and maybe even 
Type_Invariant, this is what we want. I'll add a bit of wording to re-enforce
that, but none is actually needed (the dynamic rules have the right effects
for all but Type_Invariant).

Looking at Pre/Post more closely, it seems certain that a generic formal 
subprogram is a "callable entity" inside of the generic unit; if it wasn't,
we'd need special rules to call them (and those don't exist so far as I can
tell). As such, the rules work properly for a formal subprogram just as they
would for any other subprogram (it just adds additional
precondition/postconditions that apply to the subprogram).

The same applies for Default_Initial_Condition and for Dynamic_Predicate 
(Static_Predicate doesn't apply since no formal type is static).

I suppose I need to check if there are any other such aspects that need 
wording that they are not allowed on formal parameters.

Agree? Disagree? Could care less?

****************************************************************

From: Randy Brukardt
Sent: Tuesday, April 10, 2018  1:09 AM

Having spent another hour looking at this, there are only a handful of other
aspects that need wording fixes, and some of what I said in the earlier 
message was wrong. I've attached the AI [this is version /01 of the AI - ED]
so anyone who's really interested can see the full situation (I did indeed 
check the entire set of aspects - most of them are operational or 
representational or allow being used only on specific syntax).

****************************************************************

From: Tucker Taft
Sent: Tuesday, April 10, 2018  7:19 AM

I think Type_Invariant is lowest priority.  Default_Initial_Condition and 
Pre/Post seem useful.  Dynamic_Predicate would be pretty weird, I think, and
probably a pain to implement.  You could always define a subtype and put a 
Dynamic_Predicate on it, if that is what you wanted.  I suppose that could be
what we would want for the semantics of a generic formal type with a 
Dynamic_Predicate, namely that it is simply added on as though we were
defining a new subtype.  But it seems odd to associate it with the generic 
formal subtype rather than a newly defined subtype.

****************************************************************

From: Steve Baird
Sent: Tuesday, April 10, 2018  8:01 AM

> I think Type_Invariant is lowest priority. 

I think Type_Invariant for a generic formal type is a bad idea.
Defining the "boundary" seems like it could get messy; it probably could be
done, but would it be worth the trouble?

> Default_Initial_Condition and Pre/Post seem useful.

Agreed.

> Dynamic_Predicate would be pretty weird, I think, and probably a pain to 
> implement.

Agreed, but see below.

> You could always define a subtype and put a Dynamic_Predicate on it, if that
> is what you wanted. I suppose that could be what we would want for the
> semantics of a generic formal type with a Dynamic_Predicate, namely that it 
> is simply added on as though we were defining a new subtype. But it seems
> odd to associate it with the generic formal subtype rather than a newly 
> defined subtype.

I think there is a stronger argument for allowing this construct than what was
given (but perhaps still not strong enough to justify allowing it).

Specifying the Dynamic_Predicate as part of the instantiator/instantiatee 
contract is different than declaring a subtype within the generic and then, by
convention, using that subtype instead of the original formal type everywhere 
within the generic.

It conveys more information to the instantiator about how the type will be
used in the generic and it enforces (as opposed to relying on a convention)
that requirement for the generic's implementation.

Still, I am not convinced that it is worth the added complexity.
I don't think I've ever wished that I had this feature.

****************************************************************

From: Randy Brukardt
Sent: Wednesday, April 11, 2018  6:10 PM

> > I think Type_Invariant is lowest priority. 
> 
> I think Type_Invariant for a generic formal type is a bad idea.
> Defining the "boundary" seems like it could get messy; it probably 
> could be done, but would it be worth the trouble?

That's what I said in the AI. The "boundary" for the formal type and the
actual type would naturally be different, which would make its implied use
as a restriction on the actual impossible. Or you could try to fix that, but
it (like Type_Invariant itself) would be a mess. Best to stay out of that 
morass.

... 
> I think there is a stronger argument for allowing this construct than 
> what was given (but perhaps still not strong enough to justify 
> allowing it).
> 
> Specifying the Dynamic_Predicate as part of the 
> instantiator/instantiatee contract is different than declaring a 
> subtype within the generic and then, by convention, using that subtype 
> instead of the original formal type everywhere within the generic.
> 
> It conveys more information to the instantiator about how the type 
> will be used in the generic and it enforces (as opposed to relying on 
> a convention) that requirement for the generic's implementation.

I didn't emphasize this part in the AI because the proposed dynamic-only 
feature really doesn't provide it. You'd need a form of static contract
"matching" (discussed in AI12-0273-1 - not for Ada 2020 - hopefully I'll get
everything posted today) in order to really provide that capability.

But one purpose of all of these constructs on generic formals is to provide 
requirements on the actuals in an instantiation. Even if those requirements 
are not actually enforced, they're still there.

This, again, is similar to the purpose of giving Pre/Post on an 
access-to-subprogram type, or a Dynamic_Predicate that references the 
designated object of an access-to-object type.

For instance, if you have:

     generic
        type Foo is ...
        with function Reduce (Obj : Foo) return Integer
           with Post => Reduce'Result in -9 .. 9;
     package Gen is
        ...
     end Gen;

An instantator of Gen can see that a function that can return any integer is
inappropriate for this generic; passing it just causes a risk of an
Assertion_Error for no good reason.

If we bury that information somewhere else, it then just ends up as a comment
somewhere associated with the generic. I think we all agree that an explicit 
Pre/Post is much better than a comment.

One would hope that CodePeer/SPARK would start checking instances for 
"compatibility" in this sense.

An example from the containers. There is a text requirement that all of the 
ordering operators passed to the containers represent a "strict weak ordering".
It would be so much better to specify this in the container generic contract
rather than an obscure blanket rule buried in A.18.

For instance:
generic
   type Element_Type is private;
   with function "<" (Left, Right : Element_Type) return Boolean is <>
       with Post => Is_Strict_Weak_Ordering (Left, Right);
   with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Ordered_Sets is

Note: We can't actually do this particular thing because it isn't sensible to 
write the function Is_Strict_Weak_Ordering. The definition is essentially:
    function Is_Strict_Weak_Ordering (Left, Right : Element_Type) return Boolean is
         (if Left < Right then (for all Z in Element_Type => (Left < Z or Z < Right))
          elsif Right < Left then (for all Z in Element_Type => (Right < Z or Z < Left)));
but we don't have an enumerator for all values of Element_Type [for good
reason -- such values might not be numerable] and even if we did it would
usually be too expensive to evaluate. Moral: not everything is reasonable to
write as a contract.

Still, the capability seems useful in the many cases where a requirement can be 
usefully modeled as a Pre/Post.

> Still, I am not convinced that it is worth the added complexity.
> I don't think I've ever wished that I had this feature.

Note that I didn't put Dynamic_Predicate on formal types into the proposed AI.
Doing so would have taken some wording, and it seemed to answer a question
that nobody had asked. But it did seem to me that someone would be asking it
soon enough, because it is an obvious sort of additional contract.

****************************************************************


Questions? Ask the ACAA Technical Agent