Version 1.7 of ai12s/ai12-0220-1.txt

Unformatted version of ai12s/ai12-0220-1.txt version 1.7
Other versions for file ai12s/ai12-0220-1.txt

!standard 6.1.1(1/4)          18-04-05 AI12-0220-1/04
!standard 6.1.1(2/3)
!standard 6.1.1(4/3)
!standard 6.1.1(19/3)
!standard 6.1.1(28/3)
!standard 6.1.1(29/3)
!standard 6.1.1(39/3)
!standard 13.1.1(12/5)
!class Amendment 17-04-07
!status Amendment 1-2012 18-04-05
!status ARG Approved 9-0-1 18-04-02
!status work item 17-04-07
!status received 16-12-22
!priority Low
!difficulty Hard
!subject Pre/Post for access-to-subprogram types
!summary
Allow Pre and Post aspects for access-to-subprogram types.
!problem
In order to reason effectively about a subprogram call (perhaps in the context of a static analysis tool, perhaps not), more information is needed than just the parameter profile. That's why the Pre and Post were invented. But we still need to know this sort of contract information even in the case where the callee is not known at compile time. In the case of dispatching calls, this need was recognized and Pre'Class and Post'Class were invented to meet this need. The same need exists for the same reasons in the case of a call via an access-to-subprogram value; that need should be met by allowing Pre and Post aspects to be specified for an access-to-subprogram type.
!proposal
(See Summary.)
!wording
Modify 6.1.1(1/4):
For a noninstance subprogram, a generic subprogram, [or ]an entry, {or an access-to-subrprogam type,} the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
Modify 6.1.1(2/3):
This aspect specifies a specific precondition for a callable entity {or an access-to-subprogram type}; ...
Add after AARM 6.1.1(3.a/3):
AARM Ramification: Pre'Class cannot be specified on access-to-subprogram type because of a Legality Rule found in 13.1.1 that limits 'Class aspects to tagged types and primitive subprograms of tagged types. The same is true for Post'Class (below).
Modify 6.1.1(4/3):
This aspect specifies a specific postcondition for a callable entity {or an access-to-subprogram type}; ...
Modify 6.1.1(19/3):
...at the point of a corresponding aspect specification applicable to a given subprogram{,}[ or] entry,{ or access-to-subprogram type,} then
Modify 6.1.1(28/3):
For a prefix F that denotes a function declaration{ or an access-to-function type}, the following attribute is defined:
Modify 6.1.1(29/3):
Within a postcondition expression for [function ]F, denotes the {return}[result] object of the function{ call for which the postcondition expression is evaluated}. The type of this attribute is that of the {result subtype of the} function {or access-to-function type}[result] except within a Post'Class postcondition expression for a function with a controlling result or with a controlling access result; in those cases the type of the attribute was described previously.
AARM To-Be-Honest: An "access-to-function type" is an
access-to-subprogram type whose designated profile is a function profile.
Replace 6.1.1(39/3):
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.
AARM Implementation Note: A call via an access-to-subprogram value can be
considered equivalent (with respect to dynamic semantics) to call to a notional "wrapper" subprogram which has the Pre and Post aspects and the profile of the access-to-subprogram type and whose body contains (and returns, in the case of a function) only a call to the designated subprogram. However, other evaluation orders for the checks are allowed beyond those allowed by strictly following this model. This equivalence can be used to determine the appropriate point at which the constant associated with an Old attribute reference in the Post aspect for an access-to-subprogram type is elaborated and finalized.
AARM Ramification: In the case of type conversion
between two access-to-subprogram types, the Pre and Post aspects of the source type of the conversion play no role in any subsequent call via the conversion result; only the Pre and Post aspects of the target type of the conversion are relevant in that case. The same applies in the case of a "conversion" (using the term loosely) which is accomplished by combining a dereference and a 'Access attribute reference, as in Some_Pointer.all'Access.
Modify 13.1.1(12/5):
If the associated declaration is for a subprogram{, an}[ or] entry{, or an access-to-subprogram type}, the names of the formal parameters are directly visible ...
!discussion
We're not checking whether the subprogram for 'Access is "compatible" with the access-to-subprogram type. (Specifically, the preconditions of the designated subprogram should be the same or weaker than those of the access type, and the postconditions should be the same or stronger than those of the access type.)
For Ada, Pre/Post is purely a dynamic feature, so such checking would be inconsistent with the rest of the language. For instance, any arbitrary Pre can be used on a dispatching subprogram, regardless of the preconditions of the "root" subprogam. Such a Pre is not known to the caller, but still is evaluated. The same thing is happening here.
Note that this semantics for access-to-subprogram is not that unusual. A wrapper subprogram also might "add" a precondition to an existing routine. For instance, if we have:
procedure P with Pre => (Some_Expr_A);
If we then define:
procedure Wrap with Pre => (Some_Expr_B) is begin P; end Wrap;
A call on Wrap will effectively enforce both (Some_Expr_B) (from the call to Wrap) and (Some_Expr_A) (from the call to P inside of Wrap). That's the same thing that is happening here. Indeed, one implementation strategy for this would be for each 'Access reference creating such a wrapper.
One can imagine static analysis tools (like SPARK) and style checking tools taking a different approach to 'Access references. By Ada not enforcing any rules, it is easier for those tools to enforce their own rules (which might very well be weaker -- because of better proof capabilities -- than any Ada-defined rules could be).
---
Note that the visibility changes are not strictly compatible. Consider:
My_Size : constant := 32;
type An_Acc_Sub is access procedure (My_Size : Natural) with Size => My_Size;
This is legal and useful in Ada 2012. However, with the changes above, this will be illegal in Ada 2020 (My_Size in the aspect specification will refer to the parameter, which is not static as is required by Size).
This is not very likely, and the only existing aspects that are allowed to be specified for an access-to-subprogram type (Size, Alignment, stream-oriented attributes) all require static values or statically denoted subprograms, and parameters can be neither, so any such problem has to be detected at compile-time.
---
We also need to consider allowing Pre/Post for formal subprograms (important) and for renames (not important, other than to be consistent with formal subprograms). Note that the !problem statement makes the same sense with "access-to-subprogram" replaced by "generic formal subprogram".
We also need to consider whether we need to make this available for closure access-to-subprogram types (aka anonymous access-to-subprogram parameter types), which clearly need this capability and cannot be handled by just declaring a named type (which has very different semantics).
Both of these issues are better split to separate-but-related AIs.
!example
pragma Assertion_Policy (Check); type T1 is access procedure (X : Integer) with Pre => X mod 2 = 0; type T2 is access procedure (X : Integer); -- no Pre specification
generic
with procedure P (X : Integer);
package G is procedure Pp (X : Integer) renames P; end G;
procedure Foo (X : Integer) is ... end;
procedure Bar is Ptr1 : T1 := Foo'access; procedure Renamed (X : Integer) renames Ptr1.all;
package I1 is new G (Foo); package I2 is new G (Ptr1.all); begin Foo (111); -- no precondition check Ptr1.all (222); -- precondition check performed T2 (Ptr1).all (333); -- no precondition check T2'(Ptr1.all'access).all (444); -- no precondition check Renamed (666); -- precondition check performed I1.Pp (777); -- no precondition check I2.Pp (888); -- precondition check performed end;
!corrigendum 6.1.1(1/4)
Replace the paragraph:
For a noninstance subprogram, a generic subprogram, or an entry, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
by:
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):
!corrigendum 6.1.1(2/3)
Replace the paragraph:
Pre
This aspect specifies a specific precondition for a callable entity; it shall be specified by an expression, called a specific precondition expression. If not specified for an entity, the specific precondition expression for the entity is the enumeration literal True.
by:
Pre
This aspect specifies a specific precondition for a callable entity or an access-to-subprogram type; it shall be specified by an expression, called a specific precondition expression. If not specified for an entity, the specific precondition expression for the entity is the enumeration literal True.
!corrigendum 6.1.1(4/3)
Replace the paragraph:
Post
This aspect specifies a specific postcondition for a callable entity; it shall be specified by an expression, called a specific postcondition expression. If not specified for an entity, the specific postcondition expression for the entity is the enumeration literal True.
by:
Post
This aspect specifies a specific postcondition for a callable entity or an access-to-subprogram type; it shall be specified by an expression, called a specific postcondition expression. If not specified for an entity, the specific postcondition expression for the entity is the enumeration literal True.
!corrigendum 6.1.1(19/3)
Replace the paragraph:
If performing checks is required by the Pre, Pre'Class, Post, or Post'Class assertion policies (see 11.4.2) in effect at the point of a corresponding aspect specification applicable to a given subprogram or entry, then the respective precondition or postcondition expressions are considered enabled.
by:
If performing checks is required by the Pre, Pre'Class, Post, or Post'Class assertion policies (see 11.4.2) in effect at the point of a corresponding aspect specification applicable to a given subprogram, entry, or access-to-subprogram type, then the respective precondition or postcondition expressions are considered enabled.
!corrigendum 6.1.1(28/3)
Replace the paragraph:
For a prefix F that denotes a function declaration, the following attribute is defined:
by:
For a prefix F that denotes a function declaration or an access-to-function type, the following attribute is defined:
!corrigendum 6.1.1(29/3)
Replace the paragraph:
F'Result
Within a postcondition expression for function F, denotes the result object of the function. The type of this attribute is that of the function result except within a Post'Class postcondition expression for a function with a controlling result or with a controlling access result; in those cases the type of the attribute was described previously.
by:
F'Result
Within a postcondition expression for F, denotes the return object of the function call for which the postcondition expression is evaluated. The type of this attribute is that of the result subtype of the function or access-to-function type except within a Post'Class postcondition expression for a function with a controlling result or with a controlling access result; in those cases the type of the attribute was described previously.
!corrigendum 6.1.1(39/3)
Replace the paragraph:
For a call via an access-to-subprogram value, all precondition and postcondition checks performed are determined by the subprogram or entry denoted by the prefix of the Access attribute reference that produced the value.
by:
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.
!corrigendum 13.1.1(12/5)
Replace the paragraph:
If the associated declaration is for a subprogram or entry, the names of the formal parameters are directly visible within the aspect_definition, as are certain attributes, as specified elsewhere in this International Standard for the identified aspect. If the associated declaration is a type_declaration, within the aspect_definition the names of any visible components, protected subprograms, and entries are directly visible, and the name of the first subtype denotes the current instance of the type (see 8.6). If the associated declaration is a subtype_declaration, within the aspect_definition the name of the new subtype denotes the current instance of the subtype.
by:
If the associated declaration is for a subprogram, entry, or access-to-subprogram type, the names of the formal parameters are directly visible within the aspect_definition, as are certain attributes, as specified elsewhere in this International Standard for the identified aspect. If the associated declaration is a type_declaration, within the aspect_definition the names of any visible components, protected subprograms, and entries are directly visible, and the name of the first subtype denotes the current instance of the type (see 8.6). If the associated declaration is a subtype_declaration, within the aspect_definition the name of the new subtype denotes the current instance of the subtype.
!ASIS
None needed.
!ACATS test
ACATS B-Test and C-Tests are needed to check that the new capabilities are supported.
!appendix

From: Steve Baird
Sent: Thursday, December 22, 2016  10:26 PM

This message is intended to open a discussion of allowing Pre and Post aspects
to be specified for named access-to-subprogram types.

First, a disclaimer about my motivation:
   This capability would make it easier for SPARK to add
   access-to-subprogram types to its supported subset of Ada.
   SPARK needs a Pre/Post contract for any supported form of call.
   This is what got me looking at this issue in the first place.
   However, I will try to argue for this proposal strictly from an
   Ada (as opposed to SPARK) perspective.

The benefits of this change are similar to the benefits associated with
Pre'Class and Post'Class. Having a more-precisely specified contract is of value
to both the "My_Subp_Ptr.all" caller and to the the
"Some_Concrete_Subprogram'Access" evaluator in much the same way that Pre'Class
and Post'Class are of value to both the caller in a dispatching call and to the
declarer of an overriding subprogram. Anything that allows the programmer to
more precisely express how a program works and the assumptions that the program
relies upon is of value.

The main idea is that the usual precondition/postcondition runtime checks are
performed for a call to a subprogram denoted via an access-to-subprogram value
if the Pre or Post aspects are specified for the given access type. This would
be in addition to any checks associated with the Pre or Post aspects of the
designated subprogram itself. If values of two different access-to-subprogram
types designate the same subprogram, then calls through the two values may
perform different precondition/postcondition checks.

To illustrate,

      pragma Assertion_Policy (Check);
      type T1 is access procedure (X : Integer) with Pre => X mod 2 = 0;
      type T2 is access procedure (X : Integer); -- no Pre specification

      generic
         with procedure P (X : Integer);
      package G is
         procedure Pp (X : Integer) renames P;
      end G;

      procedure Foo (X : Integer) is ... end;

      procedure Bar is
          Ptr1 : T1 := Foo'Access;
          procedure Renamed (X : Integer) renames Ptr1.all;

          package I1 is new G (Foo);
          package I2 is new G (Ptr1.all);
      begin
          Foo (111);                      -- no precondition check
          Ptr1.all (222);                 -- precondition check performed
          T2 (Ptr1).all (333);            -- no precondition check
          T2'(Ptr1.all'Access).all (444); -- no precondition check
          Renamed (666);                  -- precondition check performed
          I1.Pp (777);                    -- no precondition check
          I2.Pp (888);                    -- precondition check performed
      end;

Opinions?

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

From: Tucker Taft
Sent: Friday, December 23, 2016  10:22 AM

Worth mentioning explicitly is that we have discussed this quite a bit among
ourselves, and concluded that any sort of checks on creation or conversion of an
access-to-subprogram value didn't make sense in the Ada context.  Clearly in the
context of SPARK there should be static checks to prove that the precondition on
the access-to-subprogram type implies the precondition on the subprogram itself,
and vice-versa for postconditions, plus appropriate checks on conversion.  But
trying to do this in the Ada context is just too complex, and would require
proof capabilities that we have never required for an Ada compiler.

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

From: Randy Brukardt
Sent: Wednesday, April  5, 2017  9:12 PM

I'm starting to process the older e-mail since the last time I did it. Steve
somehow did the equivalent of a Friday afternoon news dump by posting a bunch of
ideas just before Christmas (and the day after my last work cutoff). No one ever
commented on these before, so I'm doing it now as I'm rereading these ideas.

> This message is intended to open a discussion of allowing Pre and Post
> aspects to be specified for named access-to-subprogram types.
...
> The benefits of this change are similar to the benefits associated
> with Pre'Class and Post'Class. Having a more-precisely specified
> contract is of value to both the "My_Subp_Ptr.all" caller and to the
> the "Some_Concrete_Subprogram'Access" evaluator in much the same way
> that Pre'Class and Post'Class are of value to both the caller in a
> dispatching call and to the declarer of an overriding subprogram.
> Anything that allows the programmer to more precisely express how a
> program works and the assumptions that the program relies upon is of
> value.
...

I don't have any objection to the basic idea. But I do wonder why
access-to-subprogram is special in this regard, but renames and generic formal
subprograms do not allow new pre/post. In the latter case in particular, it
seems that the same dynamic would apply; else for a call inside of the generic
unit one has less contract information than for any other call. (At least in the
case of a renames, one can usually figure out the preconditions that apply to
the renamed entity.)

Ergo, I think any such change should apply to all three of access-to-subprogram,
generic formal subprogram, and renames (with the same additive semantics;
presumably SPARK would add additional requirements). Note that I've included
renames only because we've wanted to keep an equivalence between generic formal
parameters and the equivalent renames; this is much more important for generic
formal parameters.

Secondly, this again brings up the issue of anonymous access-to-subprogram
parameters, which cannot have aspects and thus could not have preconditions.
Since the semantics of anonymous access-to-subprogram types is very different
than that of a named access-to-subprogram, one cannot just replace one by the
other.

Allowing aspect specifications in anonymous access-to-subprogram types would
take an already terrible syntax situation and make it 100% unreadable.
Therefore, I believe that is a non-starter.

Therefore, I think we would have to reconsider again the idea of "named
anonymous access-to-subprogram types" (with better terminology!!!), essentially
using an aspect to select a "fat pointer" representation that includes the
necessary static link. (AI12-0025-1 proposed allowing "Unchecked_Access" with
such a representation in order to allow a more general version of the anonymous
access-to-subprogram. We rather abandoned that idea years ago, but the issue of
contracts for such types suggests re-raising it.)

Anyway, some thoughts on this topic, to inform an AI to be built. BTW, Steve,
are you volunteering to write such an AI???

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

From: Tucker Taft
Sent: Wednesday, April  5, 2017  9:36 PM

> ... I don't have any objection to the basic idea. But I do wonder why
> access-to-subprogram is special in this regard, but renames and
> generic formal subprograms do not allow new pre/post. In the latter
> case in particular, it seems that the same dynamic would apply; else
> for a call inside of the generic unit one has less contract
> information than for any other call. (At least in the case of a
> renames, one can usually figure out the preconditions that apply to
> the renamed entity.)
>
> Ergo, I think any such change should apply to all three of
> access-to-subprogram, generic formal subprogram, and renames (with the
> same additive semantics; presumably SPARK would add additional requirements).
> Note that I've included renames only because we've wanted to keep an
> equivalence between generic formal parameters and the equivalent
> renames; this is much more important for generic formal parameters.

I agree that just about the only justification, and it seems weak, for putting
these on renames is to preserve the equivalence with generic formals.  However,
one issue that did come up recently is there is no way to put a Pre'Class aspect
on a dispatching operation defined by a renaming of a non-dispatching operation,
and that seems a bit weird.

> Secondly, this again brings up the issue of anonymous
> access-to-subprogram parameters, which cannot have aspects and thus could not
> have preconditions.
> Since the semantics of anonymous access-to-subprogram types is very
> different than that of a named access-to-subprogram, one cannot just
> replace one by the other.
>
> Allowing aspect specifications in anonymous access-to-subprogram types
> would make an already terrible syntax situation and make it 100% unreadable.
> Therefore, I believe that is a non-starter.
>
> Therefore, I think we would have to reconsider again the idea of
> "named anonymous access-to-subprogram types" (with better
> terminology!!!), essentially using an aspect to select a "fat pointer"
> representation that includes the necessary static link. (AI12-0025-1
> proposed allowing "Unchecked_Access" with such a representation in
> order to allow a more general version of the anonymous
> access-to-subprogram. We rather abandoned that idea years ago, but the
> issue of contracts for such types suggests re-raising it.)

The original Ada 9X idea, before we went for anonymous access-to-object types,
was to have "limited" access types, which did not allow assignment, and hence
did not create dangling reference problems.  I think the same idea could be
generalized to access-to-subprogram types.  A "limited access-to-subprogram"
type could be used for subprogram pointers that could not be assigned, and would
be a place for a precondition.

A more radical idea is to get rid of "access" completely and talk about
"subprogram types."  Bob Duff pushed a bit for that originally, and it should
probably be on the table.  These would of course be of a limited type again.
This is somewhat related to lambda expressions, aka function expressions.

I think introducing limited access types would probably be less disruptive, if
somewhat less elegant.

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

From: Randy Brukardt
Sent: Wednesday, April  5, 2017  10:12 PM

...
> > Therefore, I think we would have to reconsider again the idea of
> > "named anonymous access-to-subprogram types" (with better
> > terminology!!!), essentially using an aspect to select a "fat pointer"
> > representation that includes the necessary static link. (AI12-0025-1
> > proposed allowing "Unchecked_Access" with such a representation in
> > order to allow a more general version of the anonymous
> > access-to-subprogram. We rather abandoned that idea years ago, but
> > the issue of contracts for such types suggests re-raising it.)
>
> The original Ada 9X idea, before we went for anonymous
> access-to-object types, was to have "limited" access types, which did
> not allow assignment, and hence did not create dangling reference
> problems.

That's what an anonymous access-to-subprogram is essentially. Making it a
limited type causes limited elementary types, which I think causes issues with
parameter passing (how does by-copy parameter passing work with a limited
type?). That's why we used accessibility instead to prevent assignment.

> I think the same idea could be
> generalized to access-to-subprogram types.  A "limited
> access-to-subprogram" type could be used for subprogram pointers that
> could not be assigned, and would be a place for a precondition.

We already have such a thing, we just stupidly tied it to anonymous-ness. I
don't think there is any particular issue in generalizing it with syntax and/or
an aspect. Except perhaps in coming up with a name. The obvious names "general"
and "universal" already have been stolen, er, used for other things. I suppose
we could get really weird and use "all":

     type General_Subp is access all procedure;

But of course "all" is a bit weird for a type that only allows very limited
assignment.

> A more radical idea is to get rid of "access" completely and talk
> about "subprogram types."  Bob Duff pushed a bit for that originally,
> and it should probably be on the table.
> These would of course be of a limited type again.  This is somewhat
> related to lambda expressions, aka function expressions.

I've thought about that several times, too. The problem is that the semantics
end up 98% the same as access-to-subprogram (some form), the only difference is
removing some 'Accesses and the occasional .all from the source when using this.
Not at all convinced that is worth the hefty load of definitional work.

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

From: Tucker Taft
Sent: Wednesday, April  5, 2017  10:49 PM

> ... Making it a
> limited type causes limited elementary types, which I think causes
> issues with parameter passing (how does by-copy parameter passing work
> with a limited type?). That's why we used accessibility instead to
> prevent assignment.

We already have limited types that are passed by copy -- limited private types
where the full type is elementary.  So I don't see this as such a stretch.

> ... I suppose we could get really weird and use "all":
>
>      type General_Subp is access all procedure;

    type General_Subp is limited access procedure ...;

seems like the obvious syntax (to me!).

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

From: Randy Brukardt
Sent: Thursday, April  6, 2017  12:09 AM

> > ... Making it a
> > limited type causes limited elementary types, which I think causes
> > issues with parameter passing (how does by-copy parameter passing
> > work with a limited type?). That's why we used accessibility instead
> > to prevent assignment.
>
> We already have limited types that are passed by copy -- limited
> private types where the full type is elementary.  So I don't see this
> as such a stretch.

Those aren't immutably limited though...

> > ... I suppose we could get really weird and use "all":
> >
> >      type General_Subp is access all procedure;
>
>     type General_Subp is limited access procedure ...;
>
> seems like the obvious syntax (to me!).

...while anything with "limited" in the syntax IS immutably limited.

Such a type can only be build-in-place, and there are no build-in-place by-copy
parameters!

You want something that doesn't have assignment_statements, but does allow all
other sorts of assignment. That's clearly new, at least outside of limited
private types (which are not types at all, just a view). And those cause all
kinds of anomalies that I doubt that we want to repeat.

I suppose you could say something like a "limited access" type declares a
limited partial view of an access-to-subprogram type, and that there is also a
non-limited anonymous full view that has assignment. Seems groddy, though.

The full view of a type that is limited and still has assignment (not
build-in-place) would definitely be a new idea semantically.

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

From: Tucker Taft
Sent: Thursday, April  6, 2017  1:29 AM

>>> ... I suppose we could get really weird and use "all":
>>>
>>>      type General_Subp is access all procedure;
>>
>>     type General_Subp is limited access procedure ...;
>>
>> seems like the obvious syntax (to me!).
>
> ...while anything with "limited" in the syntax IS immutably limited.

Today that is true.  But we could just as easily say that "any composite type
that has "limited" in its syntax is immutably limited."  Or better, "any
composite type that is immutably limited is passed by reference, and built in
place."

> Such a type can only be build-in-place, and there are no
> build-in-place by-copy parameters!

Easy enough to narrow the rules to make this work.

> You want something that doesn't have assignment_statements, but does
> allow all other sorts of assignment. That's clearly new, at least
> outside of limited private types (which are not types at all, just a
> view). And those cause all kinds of anomalies that I doubt that we want to repeat.
>
> I suppose you could say something like a "limited access" type
> declares a limited partial view of an access-to-subprogram type, and
> that there is also a non-limited anonymous full view that has assignment.
> Seems groddy, though.
>
> The full view of a type that is limited and still has assignment (not
> build-in-place) would definitely be a new idea semantically.

It doesn't have assignment *statements*, but like other limited types (in Ada
2012), it allows assignment as part of initialization.

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

From: Steve Baird
Sent: Thursday, April  6, 2017  11:27 AM

> But I do wonder why
> access-to-subprogram is special in this regard, but renames and
> generic formal subprograms do not allow new pre/post.

It seems worth noting that contract information in general is in a much worse
state for these guys than for other callable constructs because the
result/parameter subtypes cannot be trusted.

Some_Subprogram'Access requires subtype conformance.

>  BTW, Steve, are you volunteering to write such an AI???

I'd like some assurance first that such an AI might have some reasonable chance
of being approved. If the group feels that this is a terrible idea even before
diving into details, then I'd rather not try to work out those details. Subject
to that caveat, I'd be glad to work on this AI.

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

From: Randy Brukardt
Sent: Thursday, April  6, 2017  4:09 PM

> > But I do wonder why
> > access-to-subprogram is special in this regard, but renames and
> > generic formal subprograms do not allow new pre/post.
>
> It seems worth noting that contract information in general is in a
> much worse state for these guys than for other callable constructs
> because the result/parameter subtypes cannot be trusted.
>
> Some_Subprogram'Access requires subtype conformance.

That's true, but it seems to make having contracts on these more important -
there is no other way to enforce a contract on a formal subprogram (since
subtypes and predicates can't be trusted).

Also, in a perverse sort of way, the fact that there might be other
preconditions on the actual than the ones you know about seems less nasty for a
generic formal subprogram when you already know that there might be subtypes and
predicates enforced on the call that you don't know about. That seems much more
jarring for access-to-subprogram where that's not true.

> >  BTW, Steve, are you volunteering to write such an AI???
>
> I'd like some assurance first that such an AI might have some
> reasonable chance of being approved. If the group feels that this is a
> terrible idea even before diving into details, then I'd rather not try
> to work out those details. Subject to that caveat, I'd be glad to work
> on this AI.

I've heard no one say that they think it is a terrible idea. I'm sure not
everyone is convinced, but a good AI writeup should fix that. :-)

For me personally, work on Nonblocking and thinking about Global makes it clear
to me that you can't think about subprogram contracts unless you handle formal
subprograms and access-to-subprogram somehow. And the totally dynamic scheme
that we currently have I suppose qualifies as "somehow", but only if you are
completely uninterested in the value of contracts! A "contract" between a caller
and a callee that the caller doesn't know about is hardly a contract at all: its
the sort of contract that only an intellectual property lawyer could love. :-)
:-)

Allowing the specification of contracts on these entities, plus the adoption of
"style rules" - perhaps ones that can be enforced by an outside tool - is the
only way to bring the advantages of contracts to such features.

Any sort of static checking (whether its part of the Ada language or enforced by
outside tools) requires contracts on formal subprograms and
access-to-subprogram. [Almost all of the complications for Nonblocking come from
dealing with these areas.] I can't imagine that we really want to not worry
about having the ability to make some form of static checking on these
contracts.

Ergo, I find this one of the highest priority contract AIs, probably right
behind Global and Nonblocking. (It's higher than the others because unlike them,
this one can get finished. :-)

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

From: Randy Brukardt
Sent: Thursday, April  6, 2017  3:56 PM

...
> > The full view of a type that is limited and still has assignment
> > (not
> > build-in-place) would definitely be a new idea semantically.
>
> It doesn't have assignment *statements*, but like other limited types
> (in Ada 2012), it allows assignment as part of initialization.

I suspect that we both have failed to look at the forest instead of the trees.
That is, what problem are we trying to solve and dos this solve it? I'm pretty
sure that we ended up rejecting this idea when we did "anonymous
access-to-subprogram" because it didn't prevent all of the things that we needed
to prevent. The same thing happened when we tried to use limit access types to
implement references -- in the end, it didn't help.

So it doesn't really pay to talk about whether or not limited access could be
made to work until we're sure it solves the problem. (I'm pretty sure it
doesn't, not by itself at least.)

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

From: Tucker Taft
Sent: Thursday, April  6, 2017  4:03 PM

Agreed, we should focus on that first.  I suspect if we are only trying to use
them instead of anonymous access-to-subprograms, the challenges are simpler.  In
particular, there are no run-time accessibility checks associated with anonymous
access-to-subprograms, and no 'Unchecked_Access.

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

From: Randy Brukardt
Sent: Thursday, April  6, 2017  4:55 PM

...
> > So it doesn't really pay to talk about whether or not limited access
> > could be made to work until we're sure it solves the problem. (I'm
> > pretty sure it doesn't, not by itself at least.)
>
> Agreed, we should focus on that first.  I suspect if we are only
> trying to use them instead of anonymous access-to-subprograms, the
> challenges are simpler.  In particular, there are no run-time
> accessibility checks associated with anonymous access-to-subprograms,
> and no 'Unchecked_Access.

Correct. Perhaps we need to decide what precisely we want to do before spending
effort on feature design. So let me toss out some possible goals. (For these
exercise I'm going to call these "closure access types" in the hopes of
decoupling the feature from any syntax. What I mean by that is the underlying
access type that implements anonymous access-to-subprogram parameters.)

   (1) Allow a separate declaration for closure access types, so that we can
       give properties of the type as needed (contracts in particular, but
       also possibly conventions, alignment, or anything else that can get
       defined by an aspect);
   (2) Allow giving a name for closure access types, so one does not have to
       repeat a given profile in many subprogram declarations;
   (3) Allow closure access types in more contexts (local objects?
       components? etc.);
   (4) Allow 'Unchecked_Access for subprograms;
   (5) Allow/require C interoperability;
   (6) Allow interconversion with other access-to-subprogram types.

Analysis: (1) is the current issue. (2) was an issue during the development of
"anonymous access-to-subprogram parameters" (from Erhard in particular), but we
got hung up on terminology ("named anonymous access-to-subprogram type" is an
obvious non-starter) and we never really looked at the issue seriously. I think
any solution has to handle at least (1) and (2).

(4) and implicitly (3) was the issue in AI12-0025-1. It's certainly something
that can be done, but whether it is worth it is unknown.

(5) I think we can leave to compilers, since by definition standard C doesn't
have this issue (no nested subprograms). For a C implementation that allows such
an extension (as GCC does), the implementation should and will come up with a
solution. (1) of course will help as it would allow conventions to be specified.

(6) I think is a bad idea for closure access types. It's impossible in general
to convert *to* a closure access type from a regular access-to-subprogram type
that doesn't have the closure information -- you don't know what it is. The
other direction can also be problematical, as one might use a wrapper to
"correct" the profile of some routines for a regular access-to-subprogram type
(this is what Janus/Ada does to "hide" the generic parameter data for a shared
generic body), but one probably isn't doing that for a closure access type (for
Janus/Ada, the generic parameter data is part of the closure, this is similar to
what is done for formal subprograms and for protected objects declared inside of
a generic unit).

If we're just trying to do (1) and (2), then "limited" access types don't buy us
anything, as we use infinite accessibility to make almost all conversions
illegal (which implicitly disallows assignment outside of parameter passing);
we'd still need that in any case. We would have to make using the name of a
closure access type illegal anywhere other than as the subtype of a parameter.
This would be a weird restriction, but it's easy to describe and implement. (But
note that some rules are probably missing because previously there was no
declaration, meaning that some combinations were impossible. As soon as there's
a declaration, they become possible and we have to worry about them.)

If we wanted to avoid the weird restriction, and allow the name of a closure
access type in most/all places, then making the type "limited" might help. In
that case, the "build-in-place" restrictions would have to apply to this type
(even though it wouldn't, officially at least, be built-in-place since it is a
by-copy type, and it wouldn't be immutably limited). We'd need some sort of
accessibility check on 'Access (sort of similar to the one for access
discriminants) that the object/component can't outlive the subprogram. And we'd
also have to prevent problematic conversions somehow; the infinite accessibility
trick couldn't be used anymore given the need to have a real accessibility check
on 'Access (we'd need the real level to be visible in order to be able to
describe that check). "Limited" wouldn't be a help for that per-se (although I
suppose we could use it as a hook to hang a Legality Rule).

Anyway, my $2 worth. (Definitely more than $0.50 worth. ;-)

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

From: Randy Brukardt
Sent: Friday, April  7, 2017  10:13 PM

>    (1) Allow a separate declaration for closure access types, so that
> we can give properties of the type as needed (contracts in particular,
> but also possibly conventions, alignment, or anything else that can
> get defined by an aspect);
>    (2) Allow giving a name for closure access types, so one does not
> have to repeat a given profile in many subprogram declarations;
>    (3) Allow closure access types in more contexts (local objects?
> components? etc.);
>    (4) Allow 'Unchecked_Access for subprograms;

In filing this mail, I spent some time thinking about these issues, and now
have the perfect solution. ;-) Besides, actually trying to constructively talk
about what we're trying to accomplish seems to have ended discussion
completely, probably because it's more fun to pointlessly yell at each other...

Anyway, it strikes me that a lot of the complication of accessibility checking
comes from worrying about unlikely cases of nesting and intermediate levels of
accessibility. In real programs, 98% of the access types are at library level,
and almost of the rest are local (in the current scope). One can simplify
accessibility simply into "local" and "non-local", apply nasty checks to the
latter, and that's about it.

Moreover, we don't need any checks for things that necessarily are going to
disappear before the local scope (like parameters, locals of called routines,
and the like). [Note that other sorts of closures: generators, lambdas, and
the like, destroy this property and essentially make accessibility checks
impractical. Another reason such things are inappropriate for Ada - but I
digress.]

Also recall that we need to prevent conversions to other kinds of
access-to-types. We currently use accessibility for that, but there are two
issues: the conventions of the subprograms might be different for the two
kinds of type, and in some cases that insufficient information is available
to construct the appropriate closure. Note that just banning the conversion
is not enough, because you also need to ban the similar Obj.all'Access.

So here is a very rough proposal:

    Adding "all" into an access-to-subprogram type gives one a subprogram
    closure access type. (Both the syntax and this naming isn't very
    satisfying, hopefully someone will make better suggestions --- but I need
    something for this writeup.) An anonymous access-to-subprogram parameter
    type is also a subprogram closure access type.

    Objects of a subprogram closure access type are divided into two groups:
    local and non-local. The designation of an object depends on where it is
    viewed from; thus the designation may change during the lifetime of the
    object. Local objects of a subprogram closure access type are stand-alone
    objects of the type that belong to the innermost-enclosing master (a
    runtime view) and parameters of the type of calls that belong to the
    innermost-enclosing master.

    Assignments to local objects of a subprogram closure access type are
    unrestricted. Assignments to non-local objects cannot be of 'Access of a
    non-library level subprogram (a legality check). Moreover, assignments to
    non-local objects include a check that the value is either null or the
    designated subprogram is of library level (runtime check). If
    Subp'Unchecked_Access is assigned to a subprogram closure object, the
    subprogram is considered library level (and the program is erroneous if it
    is called after it ceases to exist).

    For the conversion of a subprogram closure access type to some other kind
    of access type or vice versa, a check is made that the represented
    subprogram is library-level (or that the value is null). (This is a
    runtime check to avoid contract problems.) If the prefix of 'Access or
    'Unchecked_Access is a dereference of an access-to-subprogram type, we
    make the same check on the prefix of the dereference.

---

As far as I can tell, that's all that's required. "Local" objects always live
longer than anything that can be put into them; once you're inside of some
nested scope they're no longer local and checks are needed. Other objects only
allow library-level subprograms (always safe) or null or Unchecked_Access
(buyer beware!), or an subprogram put into them while they were local.

This idea supports all of (1)..(4). Dropping (4) [that is, not supporting
Unchecked_Access] doesn't change it at all.

Note that Tucker's limited access type doesn't work for (4), since it wouldn't
allow putting an arbitrary subprogram into a data structure (on a buyer beware
basis, of course).

It turns out that Tucker's limited access type doesn't work (completely) even
without (4), as it would allow local allocators to stuff local subprograms into
global data structures:

      -- Library level:
      type Clo_Sub_Ptr is access all procedure;
      type Some_Rec is record
          ...
          SP : Clo_Sub_Ptr;
      end record;
      type SR_Ptr is access Some_Rec;
      Root : SR_Ptr;

      procedure Something is
          Obj : Natural := 0;
          procedure Fooey is
          begin
             ... do something with Obj ...
          end Fooey;
          Local : constant Clo_Sub_Ptr := Fooey'Access; -- Should be legal.
      begin
          Root := new Some_Rec'(..., SP => Fooey'Access);
              -- This allocator is legal, even if Clo_Sub_Ptr is limited,
              -- since Fooey'Access could be built-in-place and
              -- meets the restrictions of 7.5.
          ...
      end Something;

   begin
      Something;
      Root.SP.all; -- Uses non-existent Obj.
   end;

To prevent this, you still need some sort of accessibility check on the
allocator. But if you have such a check, you can use it on other assignments
as well, so there's no advantage (to me at least) in banning
assignment_statements. (Of course, assignment statements really are only
useful if 'Unchecked_Access is available, but why ban something for no
reason?)

Anyway, enough musings for today. I think the main thing this exercise shows
is that it doesn't make much sense to worry about this until we've decided
in or out for lamdbas and generators -- because either would totally destroy
the model of this feature and would require a major redesign.

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

From: Erhard Ploedereder
Sent: Friday, April 14, 2017  12:55 PM

> A more radical idea is to get rid of "access" completely and talk
> about "subprogram types."  Bob Duff pushed a bit for that originally,
> and it should probably be on the table.  These would of course be of a
> limited type again.  This is somewhat related to lambda expressions,
> aka function expressions.

In the end, I think this is much preferable to subprogram access types (even
if the implemention is likely to be the same). Generic formal subprograms
were on the right track there already: get rid of exposing the by-reference
nature of the type. Of course, they are by-reference types. It has the charm
that it is a new class of types and thus we can come up with its own rules
that need not necessarily match up with named or anonymous access types.

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

From: Bob Duff
Sent: Friday, April 14, 2017  1:13 PM

I've always thought that:

    procedure P(...; Action: not null access procedure(X: Elem));

"not null access" is an annoying bit of noise.

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

From: Randy Brukardt
Sent: Friday, April 14, 2017  3:39 PM

I agree "access" is noise, but not necessarily the "not null". Because I often
use:

    procedure P (...; Logger : access procedure (Msg : String) := null);

to provide an optional debugging log. This is the best way (IMHO) to add
debugging to Pure and Preelaborated packages (in the latter case, Ada 2012
has another option, but for code portable to non-GNAT compilers the above is
best). There is no logging if the subprogram is null (this is often the normal
case).

Without the null, one has to use a dummy routine and that could be
substantially more expensive (calls dumping pipelines on modern machines) and
surely clutters the code - one has to come up with a name and declaration
location for the dummy.

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

From: Bob Duff
Sent: Friday, April 14, 2017  4:27 PM

> I agree "access" is noise, but not necessarily the "not null". Because
> I often use:
>
>     procedure P (...; Logger : access procedure (Msg : String) := null);
>
> to provide an optional debugging log. This is the best way (IMHO) to
> add debugging to Pure and Preelaborated packages (in the latter case,
> Ada 2012 has another option, but for code portable to non-GNAT
> compilers the above is best).

I never do that.  I don't want to scatter "if Logger /= null..."
all over the place.  Plus it just seems kludgy -- if you want a procedure
that does nothing, then write a procedure that does nothing.  Plus null might
mean something else (e.g. "send the logs to a default location").

>... There is no logging if the subprogram is null (this is often the
>normal case).

For logging, yes.  But it's not often you want a do-nothing default for
anon-access-to-subp params.

> Without the null, one has to use a dummy routine and that could be
> substantially more expensive (calls dumping pipelines on modern
> machines) and surely clutters the code

Clutters the code less than "if Logger /= null".

>... - one has to come up with a name and

procedure Do_Nothing(...) is (null);

> declaration location for the dummy.

Before the first occurrence of Do_Nothing'Access in the same package spec.

Anyway, presumably "X: not null access procedure(...)" will still be legal.
I would strongly object if "X: procedure(...)" allowed X to be null.

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

From: Bob Duff
Sent: Friday, April 14, 2017  4:48 PM

> For logging, yes.  But it's not often you want a do-nothing default
> for anon-access-to-subp params.

FWIW, in the gnat sources, I see about 230 anon-access-to-subp params.
About 228 have "not null", and most of those are in the containers packages.
About 2 do not have "not null", and default to null.

I say "about" because I'm doing textual searching, and could have gotten a
few false positives or negatives.

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

From: Tucker Taft
Sent: Friday, April 14, 2017  5:21 PM

For what it is worth in ParaSail, there are subprogram values, and a "null"
procedure value does nothing.  So you don't have to check for it explicitly.
A "null" function returns "null" so you can't use it in a context where the
null value is not permitted as a result.

This relies on the fact that all ParaSail types have an associated "null"
value, which is only permitted in certain contexts (i.e. when the modifier
"optional" is used -- so instead of "not null" there is "allows null").

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

From: Randy Brukardt
Sent: Friday, April 14, 2017  5:22 PM

> I never do that.  I don't want to scatter "if Logger /= null..."
> all over the place.  Plus it just seems kludgy -- if you want a
> procedure that does nothing, then write a procedure that does nothing.

I don't want a routine that does nothing, I don't want any logging at all.
That's not quite the same thing. Setting up a logging string can be quite
expensive (involving Image and concats); not doing all of that when it is
not needed can matter (if the routine is otherwise cheap).

And yes, it's annoying to put "Logger /= null" or "if Trace then" all over,
but that gives better performance than the "simple" solution. We were very
consistent about that in the Janus/Ada compiler (almost to the point of
harming readability) to avoid sapping performance with stuff that isn't going
to get executed (the code size used to matter, too).

...
> For logging, yes.  But it's not often you want a do-nothing default
> for anon-access-to-subp params.

I would have just said "it's not often you want ... anon-access-to-subp
params." I only use them in this instance because the restrictions on Pure
and Preelaborated packages make the normal solution impossible.

...
> Anyway, presumably "X: not null access procedure(...)" will still be
> legal.  I would strongly object if "X:
> procedure(...)" allowed X to be null.

I would strongly object to allowing "X : procedure(...)"; no more anonymous
parameter types for me. (Fool me once, fool me twice...) Besides, the entire
point of this discussion is to add a place to hang a precondition, so a type
declaration is required or we're not even solving the problem.

As for
    type Logger_Type is procedure (Msg : String);

I'm ambivalent. Allowing null "feels" wrong, but not allowing it seems to make
managing data structures containing components of this type harder.
(And what's the default initialization in that case??)

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

From: Jean-Pierre Rosen
Sent: Friday, April 14, 2017  11:47 PM

> For what it is worth in ParaSail, there are subprogram values, and a
> "null" procedure value does nothing.

Too bad you didn't call it "OM" ...

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

From: Steve Baird
Sent: Friday, June  9, 2017  6:50 PM

Here is a first cut at wording for this AI. (This is version /02 of the AI
 - Editor.)

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

From: Randy Brukardt
Sent: Friday, June  9, 2017  8:59 PM

Thanks. We still need a !problem, !summary, and !discussion. And for me at
least, we need this to work on generic formal subprograms, as those are an
access-to-subprogram analogue.

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

From: Steve Baird
Sent: Monday, June 12, 2017  2:21 PM

On 06/11/2017 12:10 PM, Tucker Taft wrote (in private correspondence, in reply
to a slightly earlier version of the proposed wording):

>> Replace 39/3 with:
>>    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, before any such precondition checks are performed,
>>    any precondition associated with the access-to-subprogram type is checked
>>    Similarly, after any such postcondition checks are performed, any
>>    postcondition associated with the access-to-subprogram type is checked.

> Stop here.  Move what comes below into an AARM note of some sort.  It is not
> adding anything significant, in my view, to the normative wording.  If you
> think there is something essential that is not covered by the above sentence,
> then try to identify it and only include that bit.
> 

I don't think the above portion by itself covers the dynamic semantics of a 'Old
attribute reference in the postcondition for an access-to-subprogram type. The
text you are suggesting moving to a note consists of one normative sentence
followed by some square-bracketed (i.e., redundant, non-normative) text. I'd
have no objection to moving the non-normative text to an AARM note. For the one
normative sentence however, I don''t see a cleaner/simpler way to express the
rules for 'Old.

>>    More specifically, a call via an access-to-subprogram value is
>>    equivalent (with respect to dynamic semantics) to call to a 
>> notional

typo: "to call" => "to a call"

>>    "wrapper" subprogram which has the Pre and Post aspects and the profile of the
>>    access-to-subprogram type and whose body contains (and returns, in the case
>>    of a function) only a call to the designated subprogram. [This equivalence,
>>    determines, for example, the point at which the constant associated with
>>    an Old attribute reference in the Post aspect for an access-to-subprogram
>>    type is elaborated and finalized. Note that in the case of type conversion
>>    between two access-to-subprogram types, the Pre and Post aspects of the
>>    source type of the conversion play no role in any subsequent call via
>>    the conversion result; only the Pre and Post aspects of the target type
>>    of the conversion are relevant in that case.]

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

From: Steve Baird
Sent: Monday, June 12, 2017  4:46 PM

The wording I proposed earlier didn't deal at all with assertion policies and
the question of whether a given Pre/Post check is enabled.

I think the following remedies this:

In 19/3:
>  If performing checks is required by the Pre, Pre'Class, Post, or 
> Post'Class assertion policies (see 11.4.2) in effect  at the point of a
> corresponding aspect specification applicable to a given subprogram or entry,
> then the respective precondition or postcondition expressions are considered
> enabled.

we need to either replace "subprogram or entry" with something like "subprogram,
entry, or access-to-subprogram type" or perhaps instead simply delete the entire
"applicable to a given subprogram or entry" qualification.

Then, in the wording I proposed earlier about the dynamics semantics of an
access-to-subprogram call, replace
    "any precondition" and "any postcondition"
with
    "enabled precondition" and "any enabled postcondition", respectively.

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

From: Tucker Taft
Sent: Monday, June 12, 2017  4:49 PM

> I don't think the above portion by itself covers the dynamic semantics 
> of a 'Old attribute reference in the postcondition for an 
> access-to-subprogram type. The text you are suggesting moving to a 
> note consists of one normative sentence followed by some 
> square-bracketed (i.e., redundant, non-normative) text. I'd have no 
> objection to moving the non-normative text to an AARM note.

Please do.

> For the one normative sentence however, I don''t see a cleaner/simpler 
> way to express the rules for ‘Old.

I am not totally convinced, if ‘Old is really the only problem you are trying
to solve.  But let’s discuss this live.

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

From: Steve Baird
Sent: Monday, June 12, 2017  5:01 PM

> replace
>     "any precondition" and "any postcondition"
> with
>     "enabled precondition" and "any enabled postcondition",

typo: "enabled precondition" => "any enabled precondition".

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

From: Randy Brukardt
Sent: Monday, June 12, 2017  6:40 PM

> The wording I proposed earlier didn't deal at all with assertion 
> policies and the question of whether a given Pre/Post check is 
> enabled.

The existing wording is already very inconsistent about that (as I found out
trying to piggyback the Stable_Properties aspect on top). I won't mind if we
scrubbed the wording so that we used consistent language throughout 6.1.1.
(But that's work :-).
 
> I think the following remedies this:
> 
> In 19/3:
> >  If performing checks is required by the Pre, Pre'Class, Post, or 
> > Post'Class assertion policies (see 11.4.2) in effect  at
> the point of a corresponding aspect specification applicable to a 
> given subprogram or entry, then the respective > precondition or 
> postcondition expressions are considered enabled.
> 
> we need to either replace "subprogram or entry" with something like 
> "subprogram, entry, or access-to-subprogram type" or perhaps instead 
> simply delete the entire "applicable to a given subprogram or entry" 
> qualification.

The qualification is there to emphasize that it is the point of the
declaration, and not the point of the call, that determines whether or not
a contract is enabled.

> Then, in the wording I proposed earlier about the dynamics semantics 
> of an access-to-subprogram call, replace
>     "any precondition" and "any postcondition"
> with
>     "enabled precondition" and "any enabled postcondition", 
> respectively.

Sounds good, but is that done in the rest of the Dynamic Semantics? I'd hate
to make it even more inconsistent.

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

From: Steve Baird
Sent: Monday, June 12, 2017  7:19 PM

[Sent summary, problem, and an example. This is version /03 of the AI.
Also, some wording changes were applied from the mail threads. - Editor.]

---

Incidentally, we probably only want to allow Pre/Post to be specified for a
*non-derived* access-to-subprogram type. This isn't 100% obvious; perhaps
allowing the derived case would be useful, but I suggest disallowing it at
least initially.

Do we need to state that Pre and Post are type-related aspects when specified
for a type? When used in this way, are Pre and Post nonoverridable (see 13.1.1
18.2/5)?

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

From: Randy Brukardt
Sent: Monday, June 12, 2017  8:25 PM

> >   We still need a !problem, !summary, and !discussion.
> !summary
...
Now you're just yanking my chain, sending this 2.5 hours after the deadline.
At least I was waiting for Tucker...

> > And for me at
> > least, we need this to work on generic formal subprograms, as those 
> > are an access-to-subprogram analogue.

You didn't explain why you didn't do this. If you substitute "generic formal
subprogram" for "access-to-subprogram" in your problem statement, it's obvious
that the same thing is true. (Along with your example, which also demonstrates
nicely that the contracts of a generic formal subprogram are completely
unknown.)

...
> Then, in the wording I proposed earlier about the dynamics semantics 
> of an access-to-subprogram call, replace
>     "any precondition" and "any postcondition"
> with
>     "enabled precondition" and "any enabled postcondition", 
> respectively.

I said earlier:
>Sounds good, but is that done in the rest of the Dynamic Semantics? I'd hate
to make it even more inconsistent.

Actually, this is unnecessary. Only paras 32, 33, and 35 take about enabled
expressions; that defines what a precondition check (and postcondition check)
do. The rest of the dynamic semantics section does not mention enabled/disabled
and only talks about checks, rather than expressions. The point being that a
"precondition expression" is enabled/disabled; a "precondition check" checks
some appliable precondition expressions. These are NOT the same thing, and that
looks intentional.

Thus your paragraph 39 wording needs to talk about "precondition checks", and
never just "precondition" alone. So "In addition, before any such precondition
checks are performed, any precondition associated with the access-to-subprogram
type is checked." is no good. Better would be something like:

"In addition, before any such precondition checks are performed, a precondition
check of any precondition expression associated with the access-to-subprogram
type is made."

Probably could use some wordsmithing, the key though is to talk about the
"precondition check" so that we're dragging in the parts about "enabled" and
"arbitrary order" and the like. 

Indeed, is there any reason here to specify an order of checks? Usually such
checks are in an unspecified order, and that seems fine here. So drop the part
in commas.

"In addition, a precondition check of any precondition expression associated
with the access-to-subprogram type is made."

"Similarly, a postcondition check of any postcondition expression associated
with the access-to-subprogram type is made."

I made this change to the wording in the latest draft; we can discuss further
in Vienna. (I suspect that there is a better way to handle 'Old than to
overspecify how checking is done.)

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

From: Randy Brukardt
Sent: Thursday, April 5, 2018  10:12 PM

Steve had the following wording (with some editorial fixes):

For a prefix F that denotes a function declaration{ or an access-to-function
type}, the following attribute is defined: 

Within a postcondition expression for [function ]F, denotes the result object
of the function. The type of this attribute is that of the function result
except within a Post'Class postcondition expression for a function with a
controlling result or with a controlling access result; in those cases the
type of the attribute was described previously.

The question I have is whether "result object of the function" and "function
result" are well-defined for an access-to-function type. At least that was
the original question.

However, neither "result object" nor "function result" are indexed in the 
Standard's index -- neither of these appear to be defined terms (I wasn't
able to find any definition with a search). We still use both a lot in the
Standard - especially the latter.

We do define "result subtype" and "return object" of a function, sort of close
but no cigar. Neither of these appear to be defined for access-to-function
types.

So the best I can do using actually defined terms would be (I'm not showing
the changes in order to keep some readability):

Within a postcondition expression for F, denotes the return object of the 
function call for which the postcondition expression is evaluated.
The type of this attribute is that of the result subtype of the function or
access-to-function type except within a Post'Class postcondition expression
for a function with a controlling result or with a controlling access result;
in those cases the type of the attribute was described previously.

Improvements? Brickbats??

P.S. I'm not so silly to try to change all of the other uses of these terms; 
I'd probably try to define the terms somewhere. But since that wouldn't fix
the problem at hand anyway, I'm not bothering for now and am just changing
this text to use actually defined terms.

P.P.S. I put Steve's explanation of "access-to-function type" into a
To-Be-Honest note -- it seemed more clutter than valuable, as I find hard to
believe anyone would be confused. I also added a AARM note to clarify that
Pre'Class/Post'Class can't be used an access types as 'Class aspects can only
be used on tagged types and primitive subprograms of tagged types.

P.P.P.S. You can look at these changes when you do your own editorial review.
The above is mine. :-)

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

From: Tucker Taft
Sent: Friday, April 6, 2018  7:53 AM

> ...
> So the best I can do using actually defined terms would be (I'm not 
> showing the changes in order to keep some readability):
> 
> Within a postcondition expression for F, denotes the return object of 
> the function call for which the postcondition expression is evaluated.
> The type of this attribute is that of the result subtype of the 
> function or access-to-function type except within a Post'Class 
> postcondition
> 
> expression for a function with a controlling result or with a 
> controlling access result; in those cases the type of the attribute 
> was described previously.
> 
> 
> Improvements? Brickbats??

Your rewording looks good to me.


> P.S. I'm not so silly to try to change all of the other uses of these 
> terms; I'd probably try to define the terms somewhere. But since that 
> wouldn't fix the problem at hand anyway, I'm not bothering for now and 
> am just changing this text to use actually defined terms.

Yes, we should probably eventually replace "result object" with "return object"
and "return subtype" with "result subtype" to be consistent.

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

From: Tullio Vardanega
Sent: Saturday, April 7, 2018  12:12 PM

In the opening sentence of:
> Within a postcondition expression for F, denotes the return object of 
> the function call for which the postcondition expression is evaluated.
> The type of this attribute is that of the result subtype of the 
> function or access-to-function type except within a Post'Class 
> postcondition expression for a function with a controlling result or 
> with a controlling access result; in those cases the type of the 
> attribute was described previously.
I am missing the subject that denotes.

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

From: Randy Brukardt
Sent: Sunday, April 8, 2018 12:53 AM

You need to look at this in context -- this is an attribute definition and
they are all written like this.

For a prefix F that denotes a function declaration or an access-to-function
type, the following attribute is defined: 

F'Result    Within a postcondition expression for F, denotes the return
object ...

I was only concerned about the non-boilerplate part of the text.

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

Questions? Ask the ACAA Technical Agent