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

--- ai12s/ai12-0418-1.txt	2021/01/13 06:30:51	1.3
+++ ai12s/ai12-0418-1.txt	2021/01/15 04:27:50	1.4
@@ -1,8 +1,15 @@
-!standard 4.3.1(17.2/5)                             21-01-12  AI12-0418-1/03
+!standard 4.3.1(17.2/5)                             21-01-14  AI12-0418-1/04
 !standard 4.3.3(10)
 !standard 4.3.5(76/5)
 !standard 4.5.2(3.1/4)
 !standard 5.5.2(10.2/5)
+!standard 6.1.1(3/3)
+!standard 6.1.1(5/3)
+!standard 6.1.1(7/5)
+!standard 6.1.1(8/3)
+!standard 6.5(5.1/5)
+!standard 6.5(8/4)
+!standard 6.5.1(1/5)
 !standard 9.7.4(14/4)                                 
 !standard 12.3(11)
 !standard 12.7(4.5/3)
@@ -49,6 +56,27 @@
 (8) In 4.5.2(3.1/4), "for" should be "of" for consistency, since the following 
 sentence uses "of" instead of "for". Change this? (Yes.)
 
+(9) In 6.1.1(7/5), the phrase "formal access parameter (or S'Result) of type 
+access-to-T" could be read to apply to all functions that return an access 
+type, not just those that are anonymous. Should this be reworded? (Yes.)
+
+(10) 6.1.1(8/3) talks about the expected type of an Old reference. Similar
+wording in 4.5.7 for conditional expressions includes "expected for some
+class of types". Do we need to mention this case here? (Yes.)
+
+(11) 6.5(5.1/5) would be improved with an "(if any)" to make it clear that
+no expression need exist. Should we do this? (Yes.)
+
+(12) 6.5(8/4) should say "the expression of the return statement"; AI12-0173-1
+made the To Be Honest note unnecessary if we use the full term. Do it? (Yes.)
+
+(13) 6.5.1(1/5) appears to give an exhaustive list of reasons that a 
+subprogram might not return, but clearly other reasons exist (such as blocking
+on an entry call forever). Should this be made more clearly examples? (Yes.)
+
+(14) 6.1.1(3/3) and 6.1.1(5/3) would be clearer if they said that they only
+apply to dispatching operations. This redundant with the Legality Rules of
+13.1.1, so it does not change anything. Do this? (Yes.)
 
 !recommendation
 
@@ -78,6 +106,19 @@
 
 (8) Replace "for" with "of".
 
+(9) Add "for an access result" after the second S'Result.
+
+(10) Add "(or class of types)". Also, there are two syntax terms in the wrong
+font in this paragraph.
+
+(11) Add "(if any)".
+
+(12) Add " of the return statement".
+
+(13) Add ", for example,".
+
+(14) Replace "an operation" with "a dispatching operation" in both paragraphs.
+
 !wording
 
 [Editor's note: These changes were applied to Draft 28 of the Ada 202x RM, 
@@ -158,6 +199,72 @@
 of a parallel generalized iterator is complete when all of its logical threads
 of control are complete.
 
+Modify 6.1.1(3/3):
+
+This aspect specifies a class-wide precondition for {a dispatching}[an] 
+operation of a tagged type and its descendants; it shall be specified by an 
+expression, called a class-wide precondition expression. If not specified 
+for an entity, then if no other class-wide precondition applies to the entity,
+the class-wide precondition expression for the entity is the enumeration
+literal True.
+
+Modify 6.1.1(5/3):
+
+This aspect specifies a class-wide postcondition for {a dispatching}[an]
+operation of a tagged type and its descendants; it shall be specified by
+an expression, called a class-wide postcondition expression. If not 
+specified for an entity, the class-wide postcondition expression for 
+the entity is the enumeration literal True.
+
+Modify 6.1.1(7/5):
+
+Within the expression for a Pre'Class or Post'Class aspect for a primitive
+subprogram S of a tagged type T, a name 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 name that denotes a formal 
+access parameter (or S'Result{ for an access result}) of type access-to-T is 
+interpreted as having type access-to-NT access-to-T'Class. 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.
+
+Modify 6.1.1(8/3):
+
+For an attribute_reference with attribute_designator Old, if the attribute
+reference has an expected type (or class of types) or shall resolve to a given
+type, the same applies to the prefix; otherwise, the prefix shall be resolved 
+independently of context.
+
+Modify 6.5(5.1/5):
+
+The expression of an extended_return_statement is the expression {(if any)}
+of the extended_return_object_declaration of the extended_return_statement.
+
+Add an AARM Ramification:
+
+   The /expression of a return statement/ is either the 
+   expression of a simple_return_statement or the expression of an
+   extended_return_statement as defined above.
+
+Modify 6.5(8/4):
+
+If the result type of a function is a specific tagged type, the tag of the
+return object is that of the result type. If the result type is class-wide,
+the tag of the return object is that of the value of the expression{ of the 
+return statement}, unless the return object is defined by an
+extended_return_object_declaration with a subtype_indication that is specific,
+in which case it is that of the type of the subtype_indication.
+A check is made that the master of the type identified by the tag of the 
+result includes the elaboration of the master that elaborated the function
+body. If this check fails, Program_Error is raised.
+
+Delete AARM 6.5(8.d.1/4).
+
+Modify 6.5.1(1/5):
+
+Specifying aspect No_Return to have the value True indicates that a subprogram
+cannot return normally; it may{, for example,} propagate an exception or loop 
+forever. 
 
 Modify 9.7.4(14/4):
 
@@ -267,6 +374,138 @@
 @dby
 *** The replacement text is found in the conflict file ***
 
+
+!corrigendum 6.1.1(3/3)
+
+@drepl
+@xhang<@xterm<Pre'Class>
+  This aspect specifies a class-wide precondition for an operation of a tagged
+  type and its descendants; it shall be specified by an @fa<expression>, called
+  a @i<class-wide precondition expression>. If not specified for an entity,
+  then if no other class-wide precondition applies to the entity, the
+  class-wide precondition expression for the entity is the enumeration
+  literal True.>
+@dby
+@xhang<@xterm<Pre'Class>
+  This aspect specifies a class-wide precondition for a dispatching operation
+  of a tagged type and its descendants; it shall be specified by an
+  @fa<expression>, called
+  a @i<class-wide precondition expression>. If not specified for an entity,
+  then if no other class-wide precondition applies to the entity, the
+  class-wide precondition expression for the entity is the enumeration
+  literal True.>
+
+!corrigendum 6.1.1(5/3)
+
+@drepl
+@xhang<@xterm<Post'Class>
+  This aspect specifies a class-wide postcondition for an operation of a tagged
+  type and its descendants; it shall be specified by an @fa<expression>, called a
+  @i<class-wide postcondition expression>. If not specified for an entity,
+  the class-wide postcondition expression for the entity is the enumeration
+  literal True.>
+@dby
+@xhang<@xterm<Post'Class>
+  This aspect specifies a class-wide postcondition for a dispatching operation
+  of a tagged type and its descendants; it shall be specified by an 
+  @fa<expression>, called a
+  @i<class-wide postcondition expression>. If not specified for an entity,
+  the class-wide postcondition expression for the entity is the enumeration
+  literal True.>
+
+!corrigendum 6.1.1(7/4)
+
+@drepl
+Within the expression for a Pre'Class or Post'Class aspect for a primitive
+subprogram @i<S> of a tagged type @i<T>, a @fa<name> that denotes a formal
+parameter (or @i<S>'Result) of type @i<T> is interpreted as though it
+had a (notional) type @i<NT> that is a formal derived type whose ancestor type
+is @i<T>, with directly visible primitive operations. Similarly, a @fa<name>
+that denotes a formal access parameter (or @i<S>'Result) of type access-to-@i<T>
+is interpreted as having type access-to-@i<NT>. The result of this
+interpretation is that the only operations that can be applied to such
+@fa<name>s are those defined for such a formal derived type.
+@dby
+Within the expression for a Pre'Class or Post'Class aspect for a primitive
+subprogram @i<S> of a tagged type @i<T>, a @fa<name> that denotes a formal
+parameter (or @i<S>'Result) of type @i<T> is interpreted as though it had a
+(notional) nonabstract type @i<NT> that is a formal derived type whose ancestor
+type is @i<T>, with directly visible primitive operations. Similarly, a @fa<name>
+that denotes a formal access parameter (or @i<S>'Result for an access result)
+of type access-to-@i<T> is interpreted as having type access-to-@i<NT>. The
+result of this interpretation is that the only operations that can be applied
+to such @fa<name>s are those defined for such a formal derived type.
+
+!corrigendum 6.1.1(8/3)
+
+@drepl
+For an attribute_reference with attribute_designator Old, if the attribute
+reference has an expected type or shall resolve to a given type, the same
+applies to the @fa<prefix>; otherwise, the @fa<prefix> shall be resolved
+independently of context.
+@dby
+For an @fa<attribute_reference> with @fa<attribute_designator> Old, if the
+attribute reference has an expected type (or class of types) or shall resolve
+to a given type, the same applies to the @fa<prefix>; otherwise, the
+@fa<prefix> shall be resolved independently of context.
+
+!corrigendum 6.5(5/3)
+
+@drepl
+A function body shall contain at least one return statement that applies to
+the function body, unless the function contains @fa<code_statement>s.
+A @fa<simple_return_statement> shall include an @fa<expression> if and only
+if it applies to a function body. An @fa<extended_return_statement> shall
+apply to a function body. An @fa<extended_return_statement> with the
+reserved word @b<constant> shall include an @fa<expression>.
+@dby
+A function body shall contain at least one return statement that applies to
+the function body, unless the function contains @fa<code_statement>s.
+A @fa<simple_return_statement> shall include an @fa<expression> if and only
+if it applies to a function body. An @fa<extended_return_statement> shall
+apply to a function body. An @fa<extended_return_object_declaration> with the
+reserved word @b<constant> shall include an @fa<expression>.
+
+The @fa<@i<expression>> @i<of an> @fa<@i<extended_return_statement>> is the
+@fa<expression> (if any) of the @fa<extended_return_object_declaration> of the
+@fa<extended_return_statement>.
+
+!corrigendum 6.5(8/4)
+
+@drepl
+If the result type of a function is a specific tagged type, the tag of the
+return object is that of the result type. If the result type is class-wide,
+the tag of the return object is that of the value of the @fa<expression>,
+unless the return object is defined by an @fa<extended_return_object_declaration>
+with a @fa<subtype_indication> that is specific, in which case it is that of
+the type of the @fa<subtype_indication>. A check is made that the master of
+the type identified by the tag of the result includes the elaboration of the
+master that elaborated the function body. If this check fails, Program_Error
+is raised.
+@dby
+If the result type of a function is a specific tagged type, the tag of the
+return object is that of the result type. If the result type is class-wide,
+the tag of the return object is that of the value of the @fa<expression>
+of the return statement, unless the return object is defined by 
+an @fa<extended_return_object_declaration>
+with a @fa<subtype_indication> that is specific, in which case it is that of
+the type of the @fa<subtype_indication>. A check is made that the master of
+the type identified by the tag of the result includes the elaboration of the
+master that elaborated the function body. If this check fails, Program_Error
+is raised.
+
+!corrigendum 6.5.1(1/3)
+
+@drepl
+Specifying aspect No_Return to have the value True
+indicates that a procedure cannot return normally; it may propagate
+an exception or loop forever.
+@dby
+Specifying aspect No_Return to have the value True
+indicates that a subprogram cannot return normally; it may, for
+example, propagate an exception or loop forever.
+
+
 !corrigendum 9.7.4(14/4)
 
 @drepl
@@ -800,5 +1039,107 @@
 This isn't quite as close to the expansion, but more obviously shows the 
 result than either of the other suggestions.
 end Editor's response.]
+
+****************************************************************
+
+From the AARM review of Steve Baird, October 2020
+
+   6.1.1 Paragraph 1 seems to suggest that Pre'Class and Post'Class
+   aspects may be specified for an access-to-subprogram type. This is
+   contradicted later. We prefer it if the RM doesn't contradict
+   itself, although the meta-rule "if two rules in the RM contradict
+   each other and one is more specific than the other, then the
+   more specific rule takes precedence" does seem to apply here.
+   Is there a problem here that needs fixing?
+
+[Editor's response: The only fix would be to delete the class-wide aspects
+from their current locations, move them after the current ones, and give them
+a new more restrictive header. Seems painful, and we don't repeat the restriction
+to primitives of a tagged type for the class-wide aspects, either. That is,
+it was always expected that the class-wide aspects would not allow everything
+supported by the other versions. So this seems like something that should have
+been done initially if it was going to be done at all.
+
+Tucker suggests replacing "an operation" with "a dispatching operation" for
+for Pre'Class and Post'Class. This doesn't fix the concern directly, but is
+thought to be an improvement.
+end Editor's response.]
+
+   In 6.1.1(7/5), do we need to add the one word "anonymous" to clarify that
+   the rule
+       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.
+   does not apply in the case of a named access-to-T function result type?
+
+[Editor's response: I think it would be better to refer to an "access result"
+here to mirror the use of "access parameter", but certainly a fix is needed.
+So I used:
+       Similarly, a name that denotes a formal access parameter
+       (or S'Result{ of an access result}) of type access-to-T is interpreted
+       as having type access-to-NT.
+end Editor's response.]
+
+   6.1.1(8/3) reads
+      For an attribute_reference with attribute_designator Old, if the
+      attribute reference has an expected type or shall resolve to a given
+      type, the same applies to the prefix; otherwise, the prefix shall be
+      resolved independently of context.
+
+   Perhaps there is no problem here, but I'm wondering whether
+   "shall resolve to a given type" ought to be "shall resolve to a
+   given type or class of types" or something similar.
+
+[Editor's response: We never talk about "shall resolve to a
+class of types. The conditional expression wording does talk about "expected
+type in a class of types". It seems rare that we do that, but there is some
+precedent.
+
+Tucker suggested "expected type {or class of types} or shall resolve to"
+to fix the problem. That has an "or" problem, so I enclosed the insertion in
+parens:
+
+"expected type {(or class of types)} or shall resolve to"
+end Editor's response.]
+
+6.5
+
+   In 5.1/5, add an "if any" modifier (surrounded by commas or parens?).
+     The expression of an extended_return_statement is the expression
+     (if any)
+     of the extended_return_object_declaration of the extended_return_statement.
+
+   ---
+
+   In 8/4 (in the context of a return statement), we talk about
+     "the expression".
+   Should this be "the expression of the return statement"? I know,
+   what other expression could it be? But still ...
+   It doesn't help any that the possibility exists that there is no
+   such expression and this possibility isn't addressed until after
+   the reference to "the expression", when we get to the
+   "unless the return object is defined by" part.
+
+   This is hardly an oversight; this point was discussed (see TBH note
+   8.d.1/4), so perhaps nothing more needs to be done here.
+   I think the TBH note is an acknowledgement that there is a problem
+   and that the proposed two-word addition would help with that problem.
+
+[Editor's response: The correct definition of the term "expression of a return
+statement" wasn't made until now (Ada 202x, by AI12-0173-1), while the wording 
+you are referring to was trying to avoid the badly defined term in Ada 2012. 
+Probably the fix you suggest should be added and the TBH deleted. Part of the 
+TBH should go after 5.1/5 as a ramification to define "expression of a return 
+statement", which is used a lot but never formally defined. The "(if any)"
+suggestion seems like a good one. (I don't want to formally define
+"expression of a return statement", that's more likely to cause trouble than 
+fix anything.) This is included in AI12-0418-1.]
+
+   In 6.5.1(1/5), the nonnormative text "it may propagate an exception or
+   loop forever" might be interpreted as an exhaustive list
+   (suggesting, for example, that blocking forever awaiting the acceptance
+   of an entry call is not a possibility).
+
+   Perhaps "it may, for example, propagate ...".
 
 ****************************************************************