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

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

!standard 3.9.3(7)          15-10-13 AI12-0170-1/02
!standard 6.1.1(7/4)
!standard 6.1.1(18.2/4)
!standard 7.3.2(5/4)
!class binding interpretation 15-06-17
!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
** TBD.
!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? (Surely, there are no exceptions to this rule. ;-)
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. So clearly that is not the intent.
!recommendation
(See Summary.)
!wording
Modify 3.9.3(7):
A call on an abstract subprogram{, unless it appears within an aspect specification of an abstract subprogram,} shall be a dispatching call; [Redundant: nondispatching calls to an abstract subprogram are not allowed.]
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 {(other than T itself)}. The corresponding expression is constructed from the associated expression as follows:
Modify 7.3.2(5/4):
Within an invariant expression, the identifier of the first subtype of the associated type denotes the current instance of the type. Within an invariant expression for the Type_Invariant aspect of a type T, the type of this current instance is T. Within an invariant expression for the Type_Invariant'Class aspect of a type T, the type of this current instance is interpreted as though it had a (notional) {nonabstract} type NT that is a visible formal derived type whose ancestor type is T. The effect of this interpretation is that the only operations that can be applied to this current instance are those defined for such a formal derived type.
!discussion
We allow calls on abstract subprograms if they are within the aspect specification of an abstract subprogram.
6.1.1(18-18.2/4) was intended to apply only to operations of actual descendants and not to the original operation. 6.1.1(18.1/4) doesn't make much sense otherwise, and one cannot daisy-pick readings that they like for individual phrases. Even so, we clarify the wording.
We also clarify 6.1.1(7/4) (and the similar 7.3.2(5/4)) to make it clear that the notional type NT is not abstract, since we want the expression to work in non-abstract contexts.
Having done this, the original question is easy to answer: no, the call is not legal. However, that seems weird because such an expression makes sense.
Note, however, that other expressions that "make sense" have never been allowed in Ada. For instance, consider:
package Pkg2 is type T is interface;
function Empty return T is abstract; procedure Init (X : out T; Value : T := Empty) is abstract; end Pkg2;
Empty is clearly illegal here, because it is not a dispatching call; it violates 3.9.3(7). (That rule is not conditional on the context.)
It's tempting to think this was a mistake, but it should be obvious that such a call only works in calls where the controlling tag comes from somewhere else. Most such expressions could never have a legal call:
package Pkg3 is type T is interface;
function Empty return T is abstract; function Length (Value : T := Empty) return Integer is abstract; end Pkg3;
A call of Length using the default parameter would end up statically bound to T, which is not a call we want to allow.
Since this has been true since Ada 95 (replace "interface" with "abstract tagged null record" and you have Ada 95 code), and all Ada 95 compilers tested reject this, we leave well-enough alone. (It seems unlikely that this is important, as if it was we would have heard about it by now - it's been 20 years since Ada 95 was approved and 8 years since Ada 2005 was approved.)
[Editor's note: I tried the Ada 95 example on both GNAT and Janus/Ada; both rejected the call of "Empty". I suspect that there is an ACATS test that requires this. Changing something here strikes me as answering a question not asked. Why make work for implementers?]
** TBD.
[Editor's note: I have no solution for the original question. The problem here is that an abstract function has to be called in a dispatching call, but Pre'Class (post AI12-0113-1) expressions are usually statically bound. On top of which, 3.9.3(7) is not context dependent. Declaring that NT is abstract in this case does not help - 3.9.3(7) still applies.
The only way that I can see to do this is to make an exception for 3.9.3(7) in the case when the expression is used directly in some expression of an abstract operation ("some expression" = precondition, postcondition, default expression of a parameter of an abstract type, more???). But then there has to be some recheck on a call, else nonsense like the Length call above or its Pre'Class counterpart would be allowed. For instance, we can't allow:
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 rules for defaults and pre/post on a call is a new concept; we don't do that currently, and it would seem to be a major headache to implement.
Thus I lean toward not fixing the problem at all. The code can be made legal by explicitly forcing the calls to be dispatching -- and any other solution looks worlds worse. Specifically:
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;
---
Another troublesome example:
package Pkg6 is type at is abstract null record;
function F1 (X : at) return Boolean is abstract;
function F2 (Y : at) return Boolean with Pre'Class => F1 (Y);
end Pkg6;
O : at'Class := ...;
if F2(at(O)) then ... -- OK, but the precondition calls F1 for AT.
This is illegal by 3.9.3(7), including after the above modification.
!ASIS
No ASIS effect.
!ACATS test
!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