Version 1.6 of ai12s/ai12-0412-1.txt

Unformatted version of ai12s/ai12-0412-1.txt version 1.6
Other versions for file ai12s/ai12-0412-1.txt

!standard 6.1.1(18.2/4)          21-01-19 AI12-0412-1/05
!class binding interpretation 20-12-03
!status work item 20-12-03
!status received 20-11-23
!priority Low
!difficulty Easy
!qualifier Error
!subject Abstract Pre/Post'Class on primitive of abstract type
!summary
Allow specifying a Pre'Class or Post'Class aspect for a concrete primitive of an abstract type even if it uses an abstract function, but then disallow other uses of such a primitive.
!question
Given the following example:
package Object is
type T is abstract tagged record B : Boolean := True; end record;
function Is_Valid (X : T) return Boolean is abstract;
procedure Do_Stuff (X : in out T) is null with Extensions_Visible, Pre'Class => Is_Valid (X);
end Object;
---
Currently the above example is illegal, because the "corresponding expression" for the given Pre'Class aspect, when constructed according to the rules of 6.1.1(18/5-18.2/4), would be illegal, since it would involve a call on an abstract function Is_Valid. But the above combination of a null concrete primitive and an abstract Pre'Class would seem quite reasonable.
Should the above be legal? (Yes.)
Note that if this is made legal, then non-dispatching uses of the concrete primitive with such an abstract Pre'Class (or Post'Class) should be illegal:
Y : T'Class := ... begin Do_Stuff (T(Y));
The above call would need to be be illegal, given that we are making a non-dispatching call on Do_Stuff, and it has a Pre'Class that is abstract for the type T. Similarly, passing as a generic formal subprogram or using 'Access will need to be disallowed.
!recommendation
Using an abstract function in a Pre'Class or a Post'Class aspect for an operation of an abstract type is a common pattern. It is inevitable for interface types (since all primitive functions of an interface type are necessarily abstract -- no "null" functions are allowed), and will be common for any abstract root type. It will also be common to have null defaults for primitives of an abstract type, if they represent a kind of "hook" which is expected to often be a no-op. Using these two together, namely a null default and an abstract Pre'Class or Post'Class, should be allowed.
As mentioned above, the above combination of features is disallowed by 6.1.1(18/5-18.2/4). We recommend allowing it, because it would be unfortunate to have to provide a concrete Is_Valid for such an abstract type, as then you would lose the protection against forgetting to override Is_Valid in a concrete descendant. But because it is possible to actually invoke a concrete primitive of an abstract type by an explicit conversion to the abstract type, we need to catch this problem somewhere. We therefore recommend requiring that it be caught at the point of such a call (or other non-dispatching use). Also, we recommend that it be illegal even if corresponding checks are disabled, as we don't want legality to be affected by the state of an assertion policy.
More generally, the "notional formal derived type" model is only truly meaningful if the actual type is not abstract, as that is the way that formal derived types work when instantiating a generic. So we recommend a simple rule that if there are any applicable Pre'Class or Post'Class aspects that are not simply True or False, then the subprogram is not directly callable if the associated type is abstract.
!wording
Replace 6.1.1(18.2/4):
The primitive subprogram S is illegal if it is not abstract and the corresponding expression for a Pre'Class or Post'Class aspect would be illegal.
with:
If the primitive subprogram S is not abstract, but the given descendant of T is abstract, then a nondispatching call on S is illegal if any Pre'Class or Post'Class aspect that applies to S is other than a static boolean expression. Similarly, a primitive subprogram of an abstract type T, to which a non-static Pre'Class or Post'Class aspect applies, shall neither be the prefix of an Access attribute_reference, nor shall it be a generic actual subprogram for a formal subprogram declared by a formal_concrete_subprogram_declaration.
!discussion
Most of the rationale is given in the !recommendation. To minimize disruption, we have chosen to put the changes into the existing Static Semantics paragraph (18.2/4), rather than moving them into the Legality Rules paragraphs. The restrictions imposed are essentially those associated with abstract subprograms. Effectively the subprogram is treated as though it is abstract, except as far as the requirement to be overridden, so it can provide a default when inherited by a non-abstract type, but not be used directly.
The new rule completely replaces the old "corresponding expression" check. The old rule was intended to handle examples shown in AI12-0113-1 and AI12-0170-1. A narrow rule like the one original proposed for this AI covers almost all of those cases, but a somewhat broader rule is needed in order that the "Length(Empty)" example found in AI12-0170-1 is covered. We believe that the "notional formal derived type" prevents other possible errors, so no expression "recheck" is needed. Eliminating the expression "recheck" for each subprogram with an applicable Pre'Class or Post'Class should be simpler for implementations and easier for users to understand.
!ASIS
No ASIS effect.
!ACATS test
ACATS B & C-Tests are needed to check the newly allowed cases, and to check that a non-dispatching call of such a routine is illegal.
!appendix

From: Tucker Taft
Sent: Monday, November 23, 2020  8:39 AM

!Subject Pre'Class using an abstract function applied to a concrete operation of abstract type

!summary

Allow specifying a Pre'Class or Post'Class aspect for a concrete primitive
of an abstract type even if it uses an abstract function, but then disallow
nondispatching calls on such a primitive.

!problem

Given the following example:

package Object is

 type T is abstract tagged record
    B : Boolean := True;
 end record;

 function Is_Valid (X : T) return Boolean is abstract;

 procedure Do_Stuff (X : in out T) is null with
   Extensions_Visible,
   Pre'Class => Is_Valid (X);

end Object;

---

Currently the above example is illegal, because the "corresponding expression"
for the given Pre'Class aspect, when constructed according to the rules of
6.1.1(18/5-18.2/4), would be illegal, since it would involve a call on an
abstract function Is_Valid.  But the above combination of a null concrete
primitive and an abstract Pre'Class would seem quite reasonable.   Therefore,
we suggest that it should be legal, but then a non dispatching call on the
concrete primitive with such a Pre'Clss should be caught:

   Y : T'Class := ...
begin
   Do_Stuff (T(Y));

The above call would need to be be illegal, given that we are making a
non-dispatching call on Do_Stuff, and it has a Pre'Class that is abstract for
the type T.

!proposal

Using an abstract function in a Pre'Class aspect for an operation of an
abstract type is a common pattern.  It is inevitable for interface types
(since all primitive functions of an interface type are necessarily abstract
-- no "null" functions are allowed), and will be common for any abstract root
type.  It will also be common to have null defaults for primitives of an
abstract type, if they represent a kind of "hook" which is expected to often
be a no-op.  Using these two together, namely a null default and an abstract
Pre'Class, should be allowed.

As mentioned above, the above combination of features is disallowed by
6.1.1(18/5-18.2/4).  We propose to allow it, because it would be unfortunate
to have to provide a concrete Is_Valid for such an abstract type, as then you
would lose the protection against forgetting to override Is_Valid in a
concrete descendant.  But because it is possible to actually invoke a concrete
primitive of an abstract type by an explicit conversion to the abstract type,
we need to catch this problem somewhere.  We therefore propose to require that
it be caught at the point of such a call.  Also, we recommend that it be
illegal even if precondition checks are disabled, as we don't want legality
to be affected by the state of an assertion policy.

!wording

Revise 6.1.1(18.2/4):

   The primitive subprogram S is illegal if [it]{the given descendant of T} is
   not abstract and the corresponding expression for a Pre'Class or Post'Class
   aspect would be illegal.  {If S itself is not abstract, then a non
   dispatching call on S is illegal if the corresponding expression for a
   Pre'Class or Post'Class aspect would be illegal.}

!discussion

Most of the rationale is given in the !proposal.  To minimize disruption, we
have chosen to keep the changes as part of the existing Static Semantics
paragraph (18.2/4), rather than moving them into the Legality Rules paragraphs.

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

From: Claire Dross
Sent: Thursday, December 3, 2020  9:13 AM

> The above call would need to be be illegal, given that we are making a
> non-dispatching call on Do_Stuff, and it has a Pre'Class that is abstract
> for the type T.

I am not sure the use case is important enough to warrant a special case. If
Do_Stuff is abstract, then it would be legal I suppose. I am not convinced
that it brings much to allow Do_Stuff to be concrete if we are not allowed
to call it in a non dispatching way.

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

From: Randy Brukardt
Sent: Thursday, December 3, 2020  11:20 PM

I originally had the same thought, but then I remembered that interfaces only
allow abstract subprograms and null procedures. If you want to define a
Pre'Class or Post'Class for such a null procedure, you'd run into this problem
as the functions that you'd call are going to be abstract. Tucker probably
should have put the reason into his original message; he did mention it in his
AI write-up.

Remember that a null procedure is essentially a default implementation for an
interface. We should have allowed expression functions to be used that way as
well (but they hadn't been invented yet).

In any case, we don't want to force people to have to chose between contracts
or default implementations. Ideally, as many features as possible work together
seamlessly. (If you are like me and don't find interfaces very valuable, then
it's harder to get interested in this fix. But I don't see much point in making
things harder for those that do like these things.)

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

From: Claire Dross
Sent: Thursday, December 3, 2020  11:20 PM

> I originally had the same thought, but then I remembered that interfaces
> only allow abstract subprograms and null procedures. If you want to define a
> Pre'Class or Post'Class for such a null procedure, you'd run into this
> problem as the functions that you'd call are going to be abstract. Tucker
> probably should have put the reason into his original message; he did
> mention it in his AI write-up.

> Remember that a null procedure is essentially a default implementation for
> an interface. We should have allowed expression functions to be used that
> way as well (but they hadn't been invented yet).

yes, probably. We already discussed allowing expression functions as default
of generic units too. I think it would be worthwhile.

> In any case, we don't want to force people to have to chose between
> contracts or default implementations. Ideally, as many features as possible
> work together seamlessly.

No, but it could make sense that a subprogram with a default has a contract
containing only subprograms which have a default.

>(If you are like me and don't find interfaces very
>valuable, then it's harder to get interested in this fix. But I don't see
>much point in making things harder for those that do like these things.)

Yes, except it makes the rules harder to understand, so I am still not in
favor of it. The lengthy discussion about whether or not the initial example
is legal shows in my opinion that the rules are already far too complex. I
don't think making them even more complicated is a good idea.

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

From: Randy Brukardt
Sent: Wednesday, December 16, 2020  11:33 PM

...
>>We should have allowed expression functions to be used that
way as well (but they hadn't been invented yet).
>
>yes, probably. We already discussed allowing expression functions as
>default of generic units too. I think it would be worthwhile.

I'm not sure who "we" are, but both of these ideas have been part of
expression functions from the very beginning. My original detailed proposal
for "expression renaming" (which eventually became expression functions)
ends: [see the !appendix of AI05-0177-1, message of Thursday, March 19, 2009
12:01 AM]

   Finally, this construct could be allowed as a primitive subprogram of an
   interface. If we did that, we would get the benefit of the identity
   function idea without adding anything special specifically for that
   case. (If we wanted to add the generic default for that case, then it
   gets a bit messier, but not a huge amount.) We would have to somehow
   include the expression in the matching rules in order to deal with the
   Steve Baird problem for diamond inheritance with interfaces. I'm not
   quite sure this is worth it, but it does add to the things that you
   cannot do now.

I think we eventually dropped these ideas in the interest of simplification.
I know I was focused on getting expression functions into the language, and
a simpler proposal certainly made that easier.

I'm pretty sure that I wrote up a more detailed proposal for rules for these
two extensions to expression functions, but I haven't been able to find it.
Probably it never made it to an AI and was buried somewhere in the pile of
e-mail related to Ada 2012 (or perhaps in one of the phone meetings minutes
-- those were never put on-line and thus cannot be searched -- much of the
Ada 2012 design was decided in those meetings).

Anyway, I don't know why this idea wasn't re-raised for Ada 202x, but it's
obviously too late now.

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

From: Claire Dross
Sent: Thursday, December 17, 2020  2:45 AM

Yes, let's reraise it for Ada 202y.

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

From: Tucker Taft
Sent: Tuesday, January 19, 2021  9:58 AM

After looking at the issue identified in AI12-0421-1 where the rules in 
6.1.1(18.2/4) about Pre'Class/Post'Class legality seem overly broad, Randy
and I concluded that it made more sense to fold that issue into AI12-0412-1
which was already addressing the very same paragraph.

So during our discussion of AI12-0412-1 we should fold in the concerns 
identified in AI12-0421-1 from Steve's review.  Below is an update to 
AI12-0412-1 which simplifies the rules, and I believe also addresses the
concerns identified by Steve.

So please consider this as a replacement for the posted version of AI12-0412-1.
[This is version /04 of the AI - Editor.]

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

From: Randy Brukardt
Sent: Tuesday, January 19, 2021  8:31 PM

...
> !discussion

It would probably be a good idea to explain here that the replacement rule 
makes illegal all of the problematic examples shown in AI12-0113-1 and 
AI12-0170-1. In particular, the bizarre one with a tag indeterminant 
function, which would not have been covered by the original proposal. We 
certainly don't want there to be a possibility of calling an abstract function
in a non-dispatching call!
 
****************************************************************

From: Randy Brukardt
Sent: Tuesday, January 19, 2021  8:45 PM

Here's what I wrote to fulfill my suggestion below:
 
The new rule completely replaces the old "corresponding expression" check.
The old rule was intended to handle examples shown in AI12-0113-1 and
AI12-0170-1. A narrow rule like the one original proposed for this AI
covers almost all of those cases, but a somewhat broader rule is needed in
order that the "Length(Empty)" example found in AI12-0170-1 is covered. 
We believe that the "notional formal derived type" prevents other possible
errors, so no expression "recheck" is needed. Eliminating the expression 
"recheck" for each subprogram with an applicable Pre'Class or Post'Class
should be simpler for implementations and easier for users to understand.

We can discuss this tomorrow.
 
           Randy.

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

Questions? Ask the ACAA Technical Agent