CVS difference for ai12s/ai12-0220-1.txt

Differences between 1.4 and version 1.5
Log of other versions for file ai12s/ai12-0220-1.txt

--- ai12s/ai12-0220-1.txt	2017/06/13 02:56:07	1.4
+++ ai12s/ai12-0220-1.txt	2018/04/06 04:52:02	1.5
@@ -1,6 +1,14 @@
-!standard 6.1.1(1/4)                                  17-06-12  AI12-0220-1/03
+!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
@@ -28,56 +36,74 @@
 
 !wording
 
-6.1.1
+Modify 6.1.1(1/4):
 
-In 1/4, "For a noninstance subprogram, a generic subprogram, or an entry"
-becomes "For a noninstance subprogram, a generic subprogram, an entry, or
-an access-to-subprogram type".
+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):
 
-In 2/3 and 4/3, "for a callable entity" becomes "for a callable entity
-or an access-to-subprogram type".
+Modify 6.1.1(2/3):
 
-Intent: Pre and Post aspects may be specified for access-to-subprogram types.
+This aspect specifies a specific precondition for a callable entity
+{or an access-to-subprogram type}; ...
 
-In 19/3, "applicable to a given subprogram or entry" gets replaced by
-"applicable to a given subprogram, entry, or access-to-subprogram type".
+Add after AARM 6.1.1(3.a/3): 
 
-Intent: Pre and Post for access-to-subprogram types get enabled/disabled
-in the same way that other Pre/Post aspects do.
+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).
 
-In 28/3 "that denotes a function declaration" becomes "that denotes a
-  function declaration or an access-to-function type (that is, an
-  access-to-subprogram type whose designated profile is a function profile)".
 
-In 29/3, "Within a postcondition expression for function F" becomes
-"Within a postcondition expression".
+Modify 6.1.1(4/3):
 
-Intent: 'Result works for access-to-subp postconditions.
+This aspect specifies a specific postcondition for a callable entity
+{or an access-to-subprogram type}; ...
 
+Modify 6.1.1(19/3):
 
-Replace 39/3 with:
+...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 made. Similarly, a
+  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 made.
-  [Editor's note: I reworded the above in version /03 to use the terms
-  "precondition check" and "postcondition check" in order to bring
-  "enabled" and "arbitrary order" rules into play. That however makes
-  the following a lie. Since Steve tells us this is all about where
-  'Old objects live, it may be better to handle some other way.]
-  More specifically, a call via an access-to-subprogram value is
-  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.
-
-AARM Discussion: 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
+  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
@@ -86,71 +112,26 @@
   combining a dereference and a 'Access attribute reference, as in
   Some_Pointer.all'Access.
 
-Intent: This is the heart of the matter - the dynamics semantics of a
-  call to Ptr.all where Pre/Post has been specified for Ptr's type.
+Modify 13.1.1(12/5):
 
-Question: Is this overspecified? Do we want an implementation permission
-   here allowing the Pre/Post checks of the access-to-subprogram type
-   to be interspersed with those of the designated subprogram?
-
-====
-
-13.1.1
-
-In 12/5. "If the associated declaration is for a subprogram or entry, the
-names of the formal parameters are directly visible" becomes "If the associated
-declaration is for a subprogram, an entry, or an access-to-subprogram type,
-the names of the formal parameters are directly visible".
-
-Intent: In Pre/Post for an access-to-subp, ok to mention parameters,
-'Result and 'Old.
-
-Question: Could this possibly introduce an incompatibility? If so,
-  then do we want to restrict this rule (in the new access-to-subprogram case)
-  to apply only in the case of a Pre or Post aspect specification.
-
-A more restrictive version of this rule might be to leave sentence
-in 12/5 unmodified and instead append something like
-   "Formal parameter names are similarly directly visible in
-   a Pre or Post aspect specification for an access-to-subprogram type".
-immeditely afterwards.
+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
-
-See questions in the !wording proposal.
-
----
-
-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).
 
-This latter issue may be better split to a separate-but-related AI.
+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.
 
----
-
-We definitely need to explain here why we're not making any attempt at
-matching. It seems to me that is a job for separate tools (and style rules??),
-and not the language (from a language perspective, this is purely a dynamic
-feature so matching isn't needed for correctness).
-
-Personally, I'm not interested in doing this for access-to-subprogram types
-and not also doing it for formal subprograms, as I do not want to create
-incentives to use access-to-subprogram values (fully dynamic) instead of
-formal subprograms (with static checking for some properties) - RLB
-
-----
-
-[A snippet from my mail to Jeff on this topic - Editor.]
-
 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:
@@ -164,9 +145,48 @@
 
 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. You could even imagine each of the 'Access
-references creating such a wrapper.
+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);
@@ -197,6 +217,133 @@
           I2.Pp (888);                    -- precondition check performed
       end;
 
+!corrigendum 6.1.1(1/4)
+
+@drepl
+For a noninstance subprogram, a generic subprogram, or an entry, the
+following language-defined aspects may be specified with
+an @fa<aspect_specification> (see 13.1.1):
+@dby
+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 @fa<aspect_specification> (see 13.1.1):
+
+!corrigendum 6.1.1(2/3)
+
+@drepl
+@xhang<@xterm<Pre>
+  This aspect defines a specific precondition for a callable entity; it
+  shall be specified by an @fa<expression>, called a @i<specific precondition
+  expression>. If not specified for an entity, the specific precondition
+  expression for the entity is the enumeration literal True.>
+@dby
+@xhang<@xterm<Pre>
+  This aspect defines a specific precondition for a callable entity or an
+  access-to-subprogram type; it shall
+  be specified by an @fa<expression>, called a @i<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)
+
+@drepl
+@xhang<@xterm<Post>
+  This aspect specifies a specific postcondition for a callable entity; it
+  shall be specified by an @fa<expression>, called a @i<specific postcondition
+  expression>. If not specified for an entity, the specific postcondition
+  expression for the entity is the enumeration literal True.>
+@dby
+@xhang<@xterm<Post>
+  This aspect specifies a specific postcondition for a callable entity or an
+  access-to-subprogram type; it shall
+  be specified by an @fa<expression>, called a @i<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)
+
+@drepl
+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 @i<enabled>.
+@dby
+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 @i<enabled>.
+
+!corrigendum 6.1.1(28/3)
+
+@drepl
+For a @fa<prefix> F that denotes a function declaration, the following
+attribute is defined:
+@dby
+For a @fa<prefix> F that denotes a function declaration or an
+access-to-function type, the following attribute is defined:
+
+!corrigendum 6.1.1(29/3)
+
+@drepl
+@xhang<@xterm<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.>
+@dby
+@xhang<@xterm<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
+   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)
+
+@drepl
+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.
+@dby
+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)
+
+@drepl
+If the associated declaration is for a subprogram or entry, the names of the
+formal parameters are directly visible within the @fa<aspect_definition>, as
+are certain attributes, as specified elsewhere in this International Standard
+for the identified aspect. If the associated declaration is a @fa<type_declaration>,
+within the @fa<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 @fa<subtype_declaration>, within the @fa<aspect_definition> the name of the
+new subtype denotes the current instance of the subtype.
+@dby
+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 @fa<aspect_definition>, as
+are certain attributes, as specified elsewhere in this International Standard
+for the identified aspect. If the associated declaration is a @fa<type_declaration>,
+within the @fa<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 @fa<subtype_declaration>, within the @fa<aspect_definition> the name of the
+new subtype denotes the current instance of the subtype.
+
 !ASIS
 
 None needed.
@@ -462,7 +609,7 @@
 
 ****************************************************************
 
-From: Randy Brukardt
+From: Tucker Taft
 Sent: Wednesday, April  5, 2017  10:49 PM
 
 > ... Making it a
@@ -1327,5 +1474,60 @@
 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. :-)
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent