Version 1.8 of ai12s/ai12-0170-1.txt

Unformatted version of ai12s/ai12-0170-1.txt version 1.8
Other versions for file ai12s/ai12-0170-1.txt

!standard 3.9.3(7)          16-07-21 AI12-0170-1/04
!standard 6.1.1(7/4)
!standard 6.1.1(18.2/4)
!class binding interpretation 15-06-17
!status Amendment 1-2012 16-07-21
!status ARG Approved 9-0-2 16-06-11
!status work item 15-06-17
!status received 15-06-15
!priority Low
!difficulty Hard
!qualifier Clarification
!subject Abstract subprogram calls in class-wide precondition expressions
!summary
Rules are largely OK as is, but we clarify that the notional type NT is non-abstract, and the check on the corresponding expression is performed for the original type itself, provided the original subprogram is non-abstract.
!question
Consider:
package Pkg is type Ifc is interface;
function F1 (X : Ifc) return Boolean is abstract;
function F2 (Y : Ifc) return Boolean is abstract with Pre'Class => F1 (Y); end Pkg;
Does the call to F1 violate the rule against non-dispatching calls to abstract subprograms?
(No, because aspect re-interpreted using notional, non-abstract descendant)
Recall that any type is a descendant of itself.
So 6.1.1(18.2/4) which applies to primitive operations of descendants of a type T
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.
also applies to the original operation of T itself.
This makes the example legal, but it would allow all sorts of things that we would not want to allow. Is this the intent? (Yes, but it doesn't allow all sorts of things, because the interpretation of the expression using the notional non-abstract type NT must be legal.)
!recommendation
(See Summary.)
!wording
Modify 6.1.1(7/4):
Within the expression for a Pre'Class or Post'Class aspect for a primitive subprogram S of a tagged type T, a name that denotes a formal parameter (or S'Result) of type T is interpreted as though it had a (notional) {nonabstract} type NT that is a formal derived type whose ancestor type is T, with directly visible primitive operations. Similarly, a name that denotes a formal access parameter (or S'Result) of type access-to-T is interpreted as having type access-to-NT. The result of this interpretation is that the only operations that can be applied to such names are those defined for such a formal derived type.
AARM Ramification: The operations of NT are also nonabstract, so the rule against a call of an abstract subprogram does not trigger for a class-wide precondition or postcondition.
Modify 6.1.1(18/4):
If a Pre'Class or Post'Class aspect is specified for a primitive subprogram S of a tagged type T, or such an aspect defaults to True, then a corresponding expression also applies to the corresponding primitive subprogram S of each descendant of T {Redundant[(including T itself)]}. The corresponding expression is constructed from the associated expression as follows:
!discussion
The existing wording was essentially correct as written, but we have added two clarifications, namely that the notional formal derived type NT is non-abstract, and that the legality rule about corresponding expressions applies to the original type T itself (unless the original subprogram is abstract). Note that if the original subprogram is not abstract, even if T is abstract, then the corresponding expression for T itself must be legal. This would mean for the example given in the !question, it would be illegal if F2 were instead a null procedure rather than an abstract function, and F1 were still abstract.
Since according to paragraph 18/4, we interpret the class-wide aspect expressions for Pre'Class and Post'Class as though they apply to a notional, non-abstract type NT, normal legality rules will prevent the illegal things mentioned in the original !question. Because NT is non-abstract, all of its primitives are non-abstract, and so we also don't have the opposite problem, namely that the example in the
!question would be illegal. The check on the legality of the
"corresponding expression" is irrelevant for Ifc itself, because F2 is abstract.
Here are some examples, and how the clarified rules apply to them:
package Pkg4 is type Ifc is interface;
function Empty return IFc is abstract; function Length (Value : IFc) return Integer is abstract;
function F3 (Y : Ifc) return Boolean is abstract with Pre'Class => Length(Empty) /= 0;
end Pkg4;
if F3 (Ifc'Class(Some_Obj)) then
The above is not legal because the Pre'Class expression is illegal, even after any substitutions for NT per paragraph 18/4 (of which there are none in this case). That is good, because the call to F3 here would call the abstract Empty and Length, because the tag indeterminant call to Empty would use the tag of its specific type (as there is no other controlling tag to use). That we cannot allow.
Here is another case:
package Pkg5 is type Ifc is interface;
function F1 (X : Ifc) return Boolean is abstract;
function F2 (Y : Ifc) return Boolean is abstract with Pre'Class => F1 (Ifc'Class(Y)); end Pkg5;
This one is legal, since we are making a dispatching call on F1, whether or not we make the substitution of "NT" for Ifc.
---
Another example:
package Pkg6 is type Abs_T is abstract tagged null record;
function F1 (X : Abs_T) return Boolean is abstract;
function F2 (Y : Abs_T) return Boolean with Pre'Class => F1 (Y);
end Pkg6;
The above is illegal, because the corresponding expression for Abs_T is illegal, and is checked because F2 is not abstract. If the above were legal, we could end up with the following problem:
O : Abs_T'Class := ...;
if F2(Abs_T(O)) then ... -- This would be bad if it were legal, because would call -- the abstract F1
But this isn't allowed because the corresponding expression for Abs_T itself is illegal (courtesy of 3.9.3(7)).
!corrigendum 6.1.1(7/4)
Replace the paragraph:
Within the expression for a Pre'Class or Post'Class aspect for a primitive subprogram S of a tagged type T, a name that denotes a formal parameter (or S'Result) of type T is interpreted as though it had a (notional) type NT that is a formal derived type whose ancestor type is T, with directly visible primitive operations. Similarly, a name that denotes a formal access parameter (or S'Result) of type access-to-T is interpreted as having type access-to-NT. The result of this interpretation is that the only operations that can be applied to such names are those defined for such a formal derived type.
by:
Within the expression for a Pre'Class or Post'Class aspect for a primitive subprogram S of a tagged type T, a name that denotes a formal parameter (or S'Result) of type T is interpreted as though it had a (notional) nonabstract type NT that is a formal derived type whose ancestor type is T, with directly visible primitive operations. Similarly, a name that denotes a formal access parameter (or S'Result) of type access-to-T is interpreted as having type access-to-NT. The result of this interpretation is that the only operations that can be applied to such names are those defined for such a formal derived type.
!corrigendum 6.1.1(18/4)
Replace the paragraph:
If a Pre'Class or Post'Class aspect is specified for a primitive subprogram S of a tagged type T, or such an aspect defaults to True, then a corresponding expression also applies to the corresponding primitive subprogram S of each descendant of T. The corresponding expression is constructed from the associated expression as follows:
by:
If a Pre'Class or Post'Class aspect is specified for a primitive subprogram S of a tagged type T, or such an aspect defaults to True, then a corresponding expression also applies to the corresponding primitive subprogram S of each descendant of T (including T itself). The corresponding expression is constructed from the associated expression as follows:
!ASIS
No ASIS effect.
!ACATS test
An ACATS B-Test should be created to check the examples (if they aren't already covered).
!appendix

From: Steve Baird
Sent: Monday, June 15, 2015  3:06 PM

In some internal discussions at AdaCore, we've been looking at this example:

  package Pkg is
    type Ifc is interface;

    function F1 (X : Ifc) return Boolean is abstract;

    function F2 (Y : Ifc) return Boolean is abstract
      with Pre'Class => F1 (Y);
  end;

and the question is whether the call to F1 violates the rule against
non-dispatching calls to abstract subprograms.

I believe AI12-0113's authors/approvers intended that this example should be
legal.

Does the wording of the AI correctly capture this intent?

Recall that any type is a descendant of itself.

So the new 6.1.1 rule about primitive operations of descendants of a type T

    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.

also applies to the original operation of T itself.

That suggests that the function declaration F2 is legal (because it is abstract)
and all is well.

But couldn't the same reasoning be used to justify all sorts of things that we
don't want to allow, such as

    procedure P3 (Z : Ifc) is abstract with
      Pre'Class =>
        (Some_Function_With_An_In_Out_Parameter (Some_Constant));

? Do we need to more precisely specify the set of "normally illegal"
constructs that are legal in the Pre'Class or Post'Class aspect of an abstract
subprogram?

Tuck suggested another approach:
>  I always interpreted 18/4-18.2/4 to only apply to inherited
> interpretations,  where "descendant of T" should have been "descendant of T
> (other than T itself)".

As Tuck pointed out, stating that intent explicitly solves the problem with
accepting the P3 example (which we want to reject) but it also takes us back to
rejecting the original F2 example (which we want to accept).

So consider following wording (also introduced in AI12-0113):

   Within the expression for a Pre'Class or Post'Class aspect for a
   primitive subprogram {S} of a tagged type T, a name that denotes a
   formal parameter {(or S'Result)} of type T is interpreted as [having
   type T'Class] {though it had a (notional) type NT that is a formal
   derived type whose ancestor type is T, with directly visible
   primitive operations}

We never say anything one way or the other about the abstractness of this
notional derived type and of its primitive operations; this seems like a hole in
any case. If we stated explicitly that these notional guys are never abstract
and also incorporated Tuck's suggestion, then perhaps that would get us to where
we want to be.

Thoughts?

Tuck also suggested that an another case where we might consider the status of
the usual "no non-dispatching calls to abstract subprograms" rule is a default
expression for a controlling formal parameter of an abstract subprogram, as in

   package Pkg2 is
    type T is interface;

    function Empty return T is abstract;
    procedure Init(X : out T; Value : T := Empty) is abstract;
   end;

. Is the call to Empty currently legal? Do we want it to be legal?

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

From: Tucker Taft
Sent: Monday, June 15, 2015  4:06 PM

> So consider following wording (also introduced in AI12-0113):
>
>    Within the expression for a Pre'Class or Post'Class aspect for a
>    primitive subprogram {S} of a tagged type T, a name that denotes a
>    formal parameter {(or S'Result)} of type T is interpreted as [having
>    type T'Class] {though it had a (notional) type NT that is a formal
>    derived type whose ancestor type is T, with directly visible
>    primitive operations}
>
> We never say anything one way or the other about the abstractness of
> this notional derived type and of its primitive operations; this seems
> like a hole in any case. If we stated explicitly that these notional
> guys are never abstract and also incorporated Tuck's suggestion, then
> perhaps that would get us to where we want to be.

I would have said "of course the notional derived type is non abstract"
but I guess we really should say that explicitly!

...
> . Is the call to Empty currently legal? Do we want it to be legal?

I believe Empty ought to be legal in this case

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

From: Randy Brukardt
Sent: Monday, June 15, 2015  4:49 PM

> In some internal discussions at AdaCore, we've been looking at this
> example:
>
>   package Pkg is
>     type Ifc is interface;
>
>     function F1 (X : Ifc) return Boolean is abstract;
>
>     function F2 (Y : Ifc) return Boolean is abstract
>       with Pre'Class => F1 (Y);
>   end;
>
> and the question is whether the call to F1 violates the rule against
> non-dispatching calls to abstract subprograms.
>
> I believe AI12-0113's authors/approvers intended that this example
> should be legal.

As Tucker points out, this never was legal in Ada for default expressions (at
least if one follows the letter of the wording), which is similar to the uses
for preconditions/postconditions (as we noted last month for protected
operations). So this example has nothing to do with AI12-0113-1, but rather is a
more general bug in Ada.

> Does the wording of the AI correctly capture this intent?
>
> Recall that any type is a descendant of itself.
>
> So the new 6.1.1 rule about primitive operations of descendants of a
> type T
>
>     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.
>
> also applies to the original operation of T itself.

I agree with Tucker that it doesn't mean that; it only applies to inherited
Pre'Class/Post'Class operations. Probably we need to add the parenthetical
remark "(other than T itself)" -- this mistake we make often because my
"descendant"s do not typically include me (so the use is a bit off compared to
the English meaning of the word).

...
> As Tuck pointed out, stating that intent explicitly solves the problem
> with accepting the P3 example (which we want to
> reject) but it also takes us back to rejecting the original
> F2 example (which we want to accept).

The original example *is* illegal; there is no provision in Ada to allow that
anywhere. Hacking preconditions for this doesn't solve anything; we need to fix
the underlying problem (or leave it unchanged).

> So consider following wording (also introduced in AI12-0113):
>
>    Within the expression for a Pre'Class or Post'Class aspect for a
>    primitive subprogram {S} of a tagged type T, a name that denotes a
>    formal parameter {(or S'Result)} of type T is interpreted as [having
>    type T'Class] {though it had a (notional) type NT that is a formal
>    derived type whose ancestor type is T, with directly visible
>    primitive operations}
>
> We never say anything one way or the other about the abstractness of
> this notional derived type and of its primitive operations; this seems
> like a hole in any case. If we stated explicitly that these notional
> guys are never abstract and also incorporated Tuck's suggestion, then
> perhaps that would get us to where we want to be.

I'm not sure what the effect of not considering these objects abstract is. I
fear that you'll come up with lots of interesting anomolies in that case.

> Tuck also suggested that an another case where we might consider the
> status of the usual "no non-dispatching calls to abstract subprograms"
> rule is a default expression for a controlling formal parameter of an
> abstract subprogram, as in
>
>    package Pkg2 is
>     type T is interface;
>
>     function Empty return T is abstract;
>     procedure Init(X : out T; Value : T := Empty) is abstract;
>    end;
>
> . Is the call to Empty currently legal? Do we want it to be legal?

No. Seems like the answer should be Yes.

I suggest we fix these two problems the same way, because they're really the
same problem. Preferably by adjusting the root rule and not by hacking around
with special cases (because we'll never remember all of them).

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

From: Randy Brukardt
Sent: Wednesday, June 17, 2015  12:15 AM

Steve wrote:

> In some internal discussions at AdaCore, we've been looking
> at this example:
>
>   package Pkg is
>     type Ifc is interface;
>
>     function F1 (X : Ifc) return Boolean is abstract;
>
>     function F2 (Y : Ifc) return Boolean is abstract
>       with Pre'Class => F1 (Y);
>   end;
>
> and the question is whether the call to F1 violates the rule
> against non-dispatching calls to abstract subprograms.

In writing this up, I find that there doesn't seem to be any sensible way to
allow this case without opening the door to calling abstract functions (I've
got several examples in the AI). I also find that the default parameter case
that Tucker brought up (which has existed since Ada 95) is uniformly
rejected by Ada 95 compilers -- probably it's required by an ACATS test. Do
we really find this so important to cause implementors to do a lot of work??

...
> Tuck also suggested that an another case where we might
> consider the status of the usual "no non-dispatching calls to
> abstract subprograms" rule is a default expression for a
> controlling formal parameter of an abstract subprogram, as in
>
>    package Pkg2 is
>     type T is interface;
>
>     function Empty return T is abstract;
>     procedure Init(X : out T; Value : T := Empty) is abstract;
>    end;
>
> . Is the call to Empty currently legal? Do we want it to be legal?

The answer is clearly No, and every compiler I tried this on agrees.
(Replace type T with "type T is abstract tagged null record;" and there a
lot of compilers to try.)

We probably don't want it to be legal unless we can figure out a way to
prevent the many cases where an abstract subprogram could be called. Even
for the above:
    Init (T(Some_Obj_of_NT));
would make a statically bound call to the abstract function. How do we avoid
that??

Similarly, assume that 3.9.3(7) is repealed for Pre'Class of abstract
subprograms, then consider:

  package Pkg4 is
    type Ifc is interface;

    function Empty return IFc is abstract;
    function Length (Value : IFc) return Integer is abstract;

    function F3 (Y : Ifc) return Boolean is abstract
      with Pre'Class => Length(Empty) /= 0;

  end Pkg4;

  if F3 (Ifc'Class(Some_Obj)) then

The call to F3 here would call the abstract Empty and Length, because the tag
indeterminant call to Empty would use the tag of its specific type (as there
is no other controlling tag to use). That we cannot allow!

Rechecking legality (of defaults and of pre/post) on all calls is not
appealing. And I don't see any simple rules that would really help.

Besides, the workaround is easy (if annoying):

  package Pkg5 is
    type Ifc is interface;

    function F1 (X : Ifc) return Boolean is abstract;

    function F2 (Y : Ifc) return Boolean is abstract
      with Pre'Class => F1 (Ifc'Class(Y));
  end Pkg5;

This is surely legal, as the call to F1 is now always dispatching.

Anyway, we have to have some fun AI for this meeting. :-)

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

From: Randy Brukardt
Sent: Tuesday, October 13, 2015  4:53 PM

> This is a minor update. [Version /02 of the AI - Editor.]

A bit too minor, I'd say. It leaves the **TBD in the !discussion, and leaves
the editor's rant that follows it (and even adds to it!) without explaining
how you addressed the issues that I was ranting about. A finished AI should
not say "I have no solution for the original question"!

And you added:

We allow calls on abstract subprograms if they are within the aspect
specification of an abstract subprogram.

which is obviously true from reading the !wording; but you give no clue as to
why that's OK or how come no actual call on an abstract routine will result.
(And if you can't explain that, we have a problem. :-)

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


Questions? Ask the ACAA Technical Agent