CVS difference for ai05s/ai05-0269-1.txt
--- ai05s/ai05-0269-1.txt 2012/02/04 09:07:39 1.6
+++ ai05s/ai05-0269-1.txt 2012/02/10 08:17:57 1.7
@@ -1,23 +1,30 @@
-!standard 3.2.4(0) 12-02-03 AI05-0269-1/06
+!standard 3.2.4(0) 12-02-09 AI05-0269-1/07
!standard 3.5(56/2)
!standard 3.10.1(13)
!standard 4.1.5(0)
!standard 4.1.6(0)
+!standard 4.5.2(2)
!standard 4.5.2(27)
!standard 4.5.2(28)
!standard 4.5.2(30.2/2)
+!standard 4.5.7(0)
+!standard 4.8(3/1)
!standard 4.9(33)
!standard 6.1.1(0)
!standard 7.3(15)
+!standard 7.3.1(5/1)
!standard 7.3.2(0)
!standard 7.4(2)
!standard 7.6(17/2)
!standard 7.6.1(13/2)
-!standard 13.3(65)
-!standard 13.11(21)
-!standard 13.11.3(5)
-!standard 13.11.4(0)
-!standard 13.13.2(26)
+!standard 9.6.1(42/2)
+!standard 13.3(65)
+!standard 13.11(21)
+!standard 13.11.3(5)
+!standard 13.11.4(0)
+!standard 13.13.2(26)
+!standard A.3.5(0)
+!standard A.4.11(0)
!standard A.16.1(0)
!standard A.17(19/2)
!standard A.18.2(147/2)
@@ -38,12 +45,14 @@
!standard A.18.23(0)
!standard A.18.24(0)
!standard B.1(1)
+!standard B.1(40)
!standard B.1(51)
!standard B.3.3(1/2)
!standard D.2.4(11/2)
!standard D.10(10)
!standard D.14(11/2)
!standard D.16.1(0)
+!standard E.2(5)
!class Amendment 11-11-09
!status Amendment 2012 12-01-12
!status work item 11-11-09
@@ -148,9 +157,9 @@
(31) 7.3(15) is not really a definition, but the italics imply that it is. Now that we've decided
that this definition is in 3.4 (see AI-0110-1), this wording should reflect that.
-(32) 7.3.2(22/3) shows that it is intended for invariant checks to apply to all visible subprograms,
-including inherited ones. But 7.3.2(15/3) says "explicitly declared", which excludes inherited
-subprograms from the checks of 7.3.2(14-18/3). This should be fixed.
+(32) 7.3.2(22/3) and it's AARM note are confusing, because it is not clear how the rules, particular
+7.3.2(12/3) are applied. In addition, 7.3.2(12/3) doesn't seem to require checking intermediate
+types when the conversion "crosses" multiple types.
(33) 7.4(2/3) is awkward, as the "unless" seems to bind with "shall".
@@ -160,6 +169,48 @@
But of course it can't be part of the expression, it's part of the result of evaluating the
expression.
+(36) 4.5.2(2/3) contains: "...or is convertible to and with accessibility level appropriate for a
+given access type." "...to and with..." is awkward, it makes the phrase hard to comprehend. [Canada
+informal comment]
+
+(37) 4.5.7(19/3) has a stray comma. [Canada informal comment]
+
+(38) 4.8(3/3) is hard to understand. Recommend adding "which is" before "the type used to identify
+a subpool". [Canada informal comment]
+
+(39) In 6.1.1(29/3), "The checks" is vague; this should say "The precondition checks". [Canada informal
+comment]
+
+(40) In 7.3.1(5.1/3), "some more" is poor wording, try to say something else. [Canada informal comment]
+
+(41) In 9.6.1(42/3), the wording is now "the result of subtracting A, and B". If we want to say
+"subtracting" it should be "A from B", not "A, and B". [Canada informal comment]
+
+(42) 4.5.7(17/3) is hard to read; perhaps consider a bulleted list. [Canada informal comment]
+
+(43) 13.3(38/3) should say "specifying the Pack aspect as True" rather than "to True" as currently.
+[Canada informal comment]
+
+(44) In 13.11.4, some functions have mode "in" on their parameters, while some procedure parameters
+are missing the mode. [Canada informal comment]
+
+(45) In A.3.5, some descriptions end with "; otherwise returns False", others end with ", otherwise
+returns False". These should all use the semicolon form. [Canada informal comment]
+
+(46) In A.4.11, 60/3 is unusual in that "otherwise" comes at the end rather than in the middle;
+92/3 and 104/3 mention the result while similar functions don't elsewhere in this section.
+[Canada informal comment]
+
+(47) B.1(40/3) should say "the aspect Export" as it is talking about specifying it as True.
+[Canada informal comment]
+
+(48) E.2(6/3) is confusing as written. We suggest using "earlier one in the hierarchy"
+instead of "earlier one" in E.2(5/3), and then making it clear that E.2(6/3) is referring to this.
+[Canada informal comment]
+
+(49) 7.3.1(14-18/3) is awkward because of the partial sentence at the end. Can this be improved?
+[Canada informal comment]
+
!wording
(1) Remove pragma Preelaborate from D.16.1(3/3).
@@ -287,7 +338,7 @@
parent node, and so on until a node with no parent is reached.
Similarly, the descendants of a node are the {node itself, its} child
nodes, the children of each child node, and so on.
-
+
Modify A.18.10(5/3):
The nodes of a subtree can be visited in several different orders.
For a depth-first order, [the last step of] {after} visiting a
@@ -332,11 +383,29 @@
(28) Add "Program_Error is raised upon calling Suspend_Until_True_And_Set_Deadline
if another task is already waiting on that suspension object." as the
penultimate sentence of D.10(10.1/3).
+
+(29) Replace D.2.4(11/3) with:
-(29) Modify D.2.4(11/3):
-"...may allow a task {of a partition using the
-Non_Premptive_FIFO_Within_Priorities policy} to execute..."
-"...does not contain {any calls to Yield_to_Higher, } any subprograms..."
+Since implementations are allowed to round all ceiling priorities in subrange System.Priority
+to System.Priority'Last (see D.3), an implementation may allow a task of a partition
+using the Non_Premptive_FIFO_Within_Priorities policy to execute within a protected object
+without raising its active priority provided the associated protected unit does not contain
+any subprograms with aspects Interrupt_Handler or Attach_Handler specified, nor does the unit
+have aspect Interrupt_Priority specified. When the locking policy (see D.3) is Ceiling_Locking,
+an implementation taking advantage of this permission shall ensure that a call to Yield_to_Higher
+that occurs within a protected action uses the ceiling priority of the protected object (rather
+than the active priority of the task) when determining whether to preempt the task.
+
+AARM Reason: We explicitly require that the ceiling priority by used
+in calls to Yield_to_Higher in order to prevent a risk of priority
+inversion and consequent loss of mutual exclusion when Yield_to_Higher
+is used in a protected object. This requirement might lessen the value of
+the permission (as the current Ceiling_Priority will have to be maintained
+in the TCB), but loss of mutual exclusion cannot be tolerated. The primary
+benefit of the permission (eliminating the need for preemption at the end
+of a protected action) is still available. As noted above, an
+implementation-defined locking policy will need to specify the semantics of
+Yield_to_Higher, including this case.
(30) Modify 6.1.1(32/3):
@@ -344,9 +413,32 @@
(31) In 7.3(15), replace the italisized "characteristics" with "characteristics
(see 3.4)", as the definition of these things live there, not here.
+
+(32) Replace 7.3.2(12/3) with:
-(32) In 7.3.2(15/3), delete "explicitly" (these checks need to apply to
-inherited routines as well as explictly declared ones).
+For a view conversion, outside the immediate scope of T, that converts from a descendant
+of T (including T itself) to an ancestor of type T {(other than T itself), a check is
+performed on the part of the object that is of type T:
+ * after assigning to the view conversion; and
+ * after successful return from a call that passes the view conversion as *in out* or
+ *out* parameter.
+
+Replace 7.3.2(22/3) and the AARM note with:
+
+For a call of a primitive subprogram of type NT that is inherited
+from type T, the specified checks of the specific invariants of both
+the types NT and T are performed. For a call of a primitive subprogram
+of type NT that is overridden for type NT, the specified checks of the
+specific invariants of only type NT are performed.
+
+AARM Proof: This follows from the definition of a call on an inherited subprogam
+as view conversions of the parameters of the type and a call to the original
+subprogram (see 3.4), along with the normal invariant checking rules. In particular,
+the call to the original subprogram takes care of any checks needed on type T,
+and the checks required on view conversions take care of any checks needed on
+type NT, specifically on *in out* and *out* parameters. We require
+this in order that the semantics of an explicitly defined wrapper that does nothing
+but call the original subprogram is the same as that of an inherited subprogram.
(33) In 7.4(2/3), replace the last sentence with:
"Unless the Import aspect (see B.1) is True for a deferred constant declaration,
@@ -364,6 +456,67 @@
"...If such an anonymous object is part of {the result of evaluating} the actual
parameter expression for..."
+(36) Modify 4.5.2(2/3):
+"...to and {has}[with]..."
+
+(37) Modify 4.5.7(19/3):
+"... case_statement (see 5.4)[,]{ also} apply to the discrete_choices..."
+
+(38) Modify 4.8(3/3):
+"... descended from Subpool_Handle, {which is} the type used to identify a subpool, ..."
+
+(39) Modify 6.1.1(29/3) [Probably will be 6.1.1(34/3) in Draft 15 - Editor]
+"The {precondition} checks are performed..."
+
+(40) Modify 7.3.1(5.1/3)
+"...or a descendant only through record extensions of {a}[some] more distant ancestor."
+
+(41) Modify 9.6.1(42/4)
+"...time zone of Calendar{ from}[, and] UTC time, ..."
+
+(42) Modify 4.5.7(17/3)
+"... none shall be dynamically tagged{. In this case,}[;] the conditional_expression..."
+
+(43) Modify 13.3(38/3):
+"...Pack aspect {as}[to] True..."
+
+(44) In 13.11.4, parameter modes should be given on all parameters except for function
+parameters with mode "in".
+
+(45) In A.3.5, replace all occurrences of ", otherwise" with "; otherwise".
+
+(46) In A.4.11, make the following modifications:
+
+A.4.11(60/3): "... If so, returns the scheme corresponding to the BOM;
+{otherwise, }returns the value of Default[ otherwise]."
+
+A.4.11(92/3) "Returns the result of decoding Item, which is encoded in
+UTF-8[, and returns the corresponding Wide_String value]."
+
+A.4.11(104/3) "Returns the result of decoding Item, which is encoded in
+UTF-8[, and returns the corresponding Wide_Wide_String value]."
+
+(47) Modify B.1(40/3):
+"...specifying {the} Export {aspect} as True is supported."
+
+(48) Modify E.2(5/3):
+"...of that category or an earlier one {in the hierarchy}, except that..."
+
+Replace E.2(6/3) with:
+
+"The overall hierarchy (including declared pure) is as follows,
+with a lower-numbered category being "earlier in the hierarchy" in the sense of
+the previous paragraph):"
+
+(49) Modify 7.3.2(14/3):
+
+{An invariant is checked upon}[Upon] successful return from a call on any subprogram or
+entry that:
+
+Modify 7.3.2(18/3):
+
+{The}[the] check is performed on each such part of type T.
+
!discussion
For (23), we copy the wording of 13.3(26.3/2).
@@ -381,6 +534,9 @@
differences between the target object and the anonymous object, which may have different
types, tags, and finalization.
+For (36), the subphrases of 4.5.2(2/3) all bind to "determines whether or not a value", and
+"has accessibility level" makes more sense than "with accessibility level" with this lead-in.
+
!corrigendum 3.2.4(0)
@@ -425,6 +581,19 @@
[A placeholder to cause a conflict; the real wording is found in the conflict
file.]
+!corrigendum 4.5.2(2)
+
+@drepl
+A @i<membership test>, using @b<in> or @b<not in>, determines whether or not a value
+belongs to a given subtype or range, or has a tag that identifies a type that is
+covered by a given type. Membership tests are allowed for all types.
+@dby
+A @i<membership test>, using @b<in> or @b<not in>, determines whether or
+not a value belongs to any given subtype or range, is equal to any given value, has
+a tag that identifies a type that is covered by a given type, or is convertible
+to and has accessibility level appropriate for a given access type.
+Membership tests are allowed for all types.
+
!corrigendum 4.5.2(27)
@dinsb
@@ -458,6 +627,28 @@
@fa<simple_expression> is non-null, the tag of the object designated by the value of the
@fa<simple_expression> is covered by the designated type of the tested type.>
+!corrigendum 4.5.7(0)
+
+@dinsc
+[A placeholder to cause a conflict; the real wording is found in the conflict
+file.]
+
+!corrigendum 4.8(3/1)
+
+@drepl
+The expected type for an @fa<allocator> shall be a single access-to-object type with
+designated type @i<D> such that either @i<D> covers the type determined by the
+@fa<subtype_mark> of the @fa<subtype_indication> or @fa<qualified_expression>,
+or the expected type is anonymous and the determined type is @i<D>'Class.
+@dby
+The expected type for an @fa<allocator> shall be a single access-to-object type with
+designated type @i<D> such that either @i<D> covers the type determined by the
+@fa<subtype_mark> of the @fa<subtype_indication> or @fa<qualified_expression>,
+or the expected type is anonymous and the determined type is @i<D>'Class.
+A @i<subpool_handle_>@fa<name> is expected to be of any type descended from
+Subpool_Handle, which is the type used to identify a subpool, declared in package
+System.Storage_Pools.Subpools (see 13.11.4).
+
!corrigendum 4.9(33)
@drepl
@@ -505,6 +696,36 @@
visible, what attributes and other predefined operations are allowed, and whether the first
subtype is static. See 7.3.1.
+!corrigendum 7.3.1(5/1)
+
+@dinsa
+For example, an array type whose component type is limited private becomes
+nonlimited if the full view of the component type is nonlimited and visible at
+some later place immediately within the declarative region in which the array
+type is declared. In such a case, the predefined "=" operator is implicitly
+declared at that place, and assignment is allowed after that place.
+@dinss
+A type is a @i<descendant> of the full view of some ancestor of its
+parent type only if the current view it has of its parent is a
+descendant of the full view of that ancestor. More generally, at any
+given place, a type is descended from the same view of an ancestor as
+that from which the current view of its parent is descended. This view
+determines what characteristics are inherited from the ancestor,
+and, for example, whether the type is considered to be
+a descendant of a record type, or a descendant only through record
+extensions of a more distant ancestor.
+
+It is possible for there to be places where a derived
+type is visibly a descendant of an ancestor type, but not a
+descendant of even a partial view of the ancestor type, because the parent
+of the derived type is not visibly a descendant of the ancestor. In
+this case, the derived type inherits no characteristics from that
+ancestor, but nevertheless is within the derivation class of the
+ancestor for the purposes of type conversion, the "covers"
+relationship, and matching against a formal derived type. In this
+case the derived type is considered to be a @i<descendant> of an
+incomplete view of the ancestor.
+
!corrigendum 7.3.2(0)
@dinsc
@@ -540,9 +761,6 @@
The real text is not here.
!corrigendum 7.6.1(13/2)
-!AI-0066-1
-!AI-0142-4
-!AI-0269-1
@drepl
The master of an object is the master enclosing its creation whose
@@ -561,7 +779,28 @@
@fa<aggregate> or function call, which may be the @fa<aggregate> or function
call itself.
+!corrigendum 9.6.1(42/2)
+
+@drepl
+@xindent<Returns, as a number of minutes, the difference between the
+implementation-defined time zone of Calendar, and UTC time, at the time Date.
+If the time zone of the Calendar implementation is unknown, then
+Unknown_Zone_Error is raised.>
+@dby
+@xindent<Returns, as a number of minutes, the result of subtracting the
+implementation-defined time zone of Calendar from UTC time, at the time Date.
+If the time zone of the Calendar implementation is unknown, then
+Unknown_Zone_Error is raised.>
+
+!corrigendum 13.3(38)
+@drepl
+@s9<5 A @fa<component_clause>, Component_Size clause, or a @fa<pragma> Pack can override a
+specified Alignment.>
+@dby
+@s9<5 A @fa<component_clause>, Component_Size clause, or specifying the Pack aspect as True
+can override a specified Alignment.>
+
!corrigendum 13.3(65)
@ddel
@@ -628,6 +867,18 @@
S'Input first reads the discriminants (using the Read attribute of the discriminant
type for each).>
+!corrigendum A.3.5(0)
+
+@dinsc
+[A placeholder to cause a conflict; the real wording is found in the conflict
+file.]
+
+!corrigendum A.4.11(0)
+
+@dinsc
+[A placeholder to cause a conflict; the real wording is found in the conflict
+file.]
+
!corrigendum A.16.1(0)
@dinsc
@@ -785,6 +1036,15 @@
used to identify imported or exported entities in the external
environment.
+!corrigendum B.1(40)
+
+@drepl
+Automatic elaboration of preelaborated packages should be provided when @fa<pragma>
+Export is supported.
+@dby
+Automatic elaboration of preelaborated packages should be provided
+when specifying the Export aspect as True is supported.
+
!corrigendum B.1(51)
@drepl
@@ -824,19 +1084,23 @@
without raising its active priority provided the associated protected unit does not contain
pragma Interrupt_Priority, Interrupt_Handler, or Attach_Handler.
@dby
-Since implementations are allowed to round all ceiling priorities in subrange System.Priority to
-System.Priority'Last (see D.3), an implementation may allow a task of a partition using the
-Non_Premptive_FIFO_Within_Priorities policy to execute within a protected object
+Since implementations are allowed to round all ceiling priorities in subrange System.Priority
+to System.Priority'Last (see D.3), an implementation may allow a task of a partition
+using the Non_Premptive_FIFO_Within_Priorities policy to execute within a protected object
without raising its active priority provided the associated protected unit does not contain
-any calls to Yield_To_Higher, any subprograms with Interrupt_Handler or Attach_Handler specified, nor
-does the unit have aspect Interrupt_Priority specified.
+any subprograms with aspects Interrupt_Handler or Attach_Handler specified, nor does the unit
+have aspect Interrupt_Priority specified. When the locking policy (see D.3) is Ceiling_Locking,
+an implementation taking advantage of this permission shall ensure that a call to Yield_to_Higher
+that occurs within a protected action uses the ceiling priority of the protected object (rather
+than the active priority of the task) when determining whether to preempt the task.
+
!corrigendum D.10(10)
@dinsa
Program_Error is raised upon calling Suspend_Until_True if another task is already
waiting on that suspension object. Suspend_Until_True is a potentially blocking
-operation (see 9.5.1).
+operation (see 9.5.1).
@dinst
The procedure Suspend_Until_True_And_Set_Deadline blocks the calling task until
the state of the object S is True; at that point the task becomes ready with a
@@ -872,7 +1136,33 @@
[A placeholder to cause a conflict; the real wording is found in the conflict
file.]
+!corrigendum E.2(5)
+@drepl
+The various categories of library units and the associated restrictions are described
+in this clause and its subclauses. The categories are related hierarchically in that
+the library units of one category can depend semantically only on library units of
+that category or an earlier one, except that the body of a remote types or remote
+call interface library unit is unrestricted.
+@dby
+The various categories of library units and the associated restrictions are
+described in this clause and its subclauses. The categories are related
+hierarchically in that the library units of one category can depend semantically
+only on library units of that category or an earlier one in the hierarchy, except that
+the body of a remote types or remote call interface library unit is unrestricted, the
+declaration of a remote types or remote call interface library unit may depend
+on preelaborated normal library units that are mentioned only in private with
+clauses, and all categories can depend on limited views.
+
+!corrigendum E.2(6)
+
+@drepl
+The overall hierarchy (including declared pure) is as follows:
+@dby
+The overall hierarchy (including declared pure) is as follows,
+with a lower-numbered category being "earlier in the hierarchy" in the sense of
+the previous paragraph:
+
!ACATS Test
None needed.
@@ -1211,7 +1501,7 @@
****************************************************************
From: Randy Brukardt
-Sent: Saturday, February 3, 2012 12:35 AM
+Sent: Saturday, February 4, 2012 12:35 AM
7.3.2(14-15/3) says:
@@ -1236,3 +1526,1269 @@
****************************************************************
+From: Tucker Taft
+Sent: Saturday, February 4, 2012 11:10 AM
+
+> I can't find any reason for the "explicitly" in this bullet, so I've
+> just deleted it, in which case the rules work and the note is true.
+> But I worry that it was there for some good reason. If the reason was
+> to avoid wrappers, well, we decided that we didn't want to do that (as
+> evidenced by the
+> 7.3.2(22/3) note), so then the word is just wrong.
+
+I have some trouble parsing your last sentence. Could you clarify?
+"We didn't want to do that" -- what is "that"? And "the word is just wrong" --
+what word?
+
+In any case, we spent a lot of time on wording this, and we covered the case of
+inherited primitives in paragraph 12, because when calling an inherited
+primitive, there are view conversions applied, and those view conversions do the
+check (per paragraph 12). Of course some kind of AARM note, or perhaps even a
+user NOTE, might help clarify this case.
+
+> If there was any other reason, I can't figure it out, and I didn't
+> find anything in the AIs to help. Anyone else remember? (Tucker in
+> particular.) More generally, anyone know of a reason not to delete
+> this stray "explicitly"?
+
+See above. I believe it is correct as written, given paragraph 12.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, February 4, 2012 4:17 PM
+
+> I have some trouble parsing your last sentence. Could you clarify?
+> "We didn't want to do that" -- what is "that"? And "the word is just
+> wrong" -- what word?
+
+"the word" is "explicitly" in 7.3.2(15/3). "that" is "avoid wrappers". I realize
+there is a double negative here, but my point is that 7.3.2(22/3) says that we
+expect to need wrappers for inherited subprograms, so any wording that is
+intended to avoid such a need is unnecessary.
+
+> In any case, we spent a lot of time on wording this, and we covered
+> the case of inherited primitives in paragraph 12, because when calling
+> an inherited primitive, there are view conversions applied, and those
+> view conversions do the check (per paragraph 12).
+> Of course some kind of AARM note, or perhaps even a user NOTE, might
+> help clarify this case.
+
+There are view conversions to T. What covers the checks on NT on the way out?
+And if you say the view conversions, then what rule causes the checks on T (in
+the inherited subprogram) on the way out (because we're not (formally) calling
+the T routine, so we don't get to apply the rules associated with T).
+
+> > If there was any other reason, I can't figure it out, and I didn't
+> > find anything in the AIs to help. Anyone else remember? (Tucker in
+> > particular.) More generally, anyone know of a reason not to delete
+> > this stray "explicitly"?
+>
+> See above. I believe it is correct as written, given paragraph 12.
+
+Neither Erhard nor I see how paragraph 12 applies. Please explain how this
+actually works (I realize this has been done before, but please try again).
+
+Specifically, in the note 7.3.2(22/3), what rule triggers the check of the
+invariant of NT for an out parameter (on return from the call))? And why?
+Similarly for the check of the invariant of T (again on return from the call)?
+
+When I read 7.3.2(12/3), it says that a check is made on a view conversion from
+T to an ancestor of T. It then says something about the same check being made on
+in out parameters. But that doesn't happen for an "in out" parameter, because
+the conversion goes from T to NT, and NT is not an ancestor of T. So there is no
+check to be made in that case.
+
+I can easily believe Erhard is wrong, and he got me so confused that I can no
+longer see what the intent is much less whether the rules cover that intent.
+(That's why I didn't quote his original message, I didn't want that effect to
+happen to anyone else.)
+
+But it seems to me that something is missing here. I had thought that it just
+was applying the explicit check to inherited subprograms (that seems to be the
+easiest way to deal with this), but perhaps 12/3 was supposed to do it (but
+doesn't). Or maybe 12/3 has mixed up static and dynamic semantics to the point
+it is incomprehensible...
+
+Anyway, thanks in advance for the clear explanation I'm sure to receive.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, February 4, 2012 5:00 PM
+
+> There are view conversions to T. What covers the checks on NT on the
+> way out? And if you say the view conversions, then what rule causes
+> the checks on T (in the inherited subprogram) on the way out (because
+> we're not
+> (formally) calling the T routine, so we don't get to apply the rules
+> associated with T).
+
+Here is paragraph 12:
+
+ After assigning to a view conversion, outside the immediate scope
+ of T, that converts from T or one or more record extensions (and
+ no private extensions) of T to an ancestor of type T, a check is
+ performed on the part of the object that is of type T; similarly,
+ for passing a view conversion as an out or in out parameter
+ outside the immediate scope of T, this check is performed upon
+ successful return;
+
+I'm not sure what you meant by "NT" above. Is that the ancestor of T from which
+it is inheriting the subprogram? I will assume that, even though usually "NT"
+is meant to signify a *descendant* of T.
+
+Anyway, when calling a subprogram inherited by T from its ancestor T0, if there
+is an invariant that applies to T, then at the point of calling the inherited
+subprogram, what happens is that the primitive of T0 is called, with all
+parameters of type T0 in that primitive of T0 being passed view conversions from
+T to T0. If any of them are OUT or IN OUT parameters, then based on para. 12
+above, on the way back, a check is performed on the T part of the object that is
+identified in the view conversion, which in this case is the whole thing. For
+example:
+
+ type T0 is ...
+ procedure Update(X : out T0);
+
+...
+
+ type T is new T0 with ...
+ with Type_Invariant => Is_Valid(T) = True;
+
+ -- Update inherited
+
+...
+
+ Y : T;
+
+ Update(Y);
+ --> this becomes a call on T0's Update:
+
+ Update(T0(Y))
+
+ --> That "T0(Y)" is a view conversion being
+ --> passed as an OUT parameter, so per para. 12, a
+ --> check on T's invariant is performed
+ --> on Y if the call completes successfully.
+ --> If T0 also has an invariant, then it is checked on T0(Y)
+ --> upon return from the call on T0's Update, and
+ --> if that succeeds, then we would perform T's invariant
+ --> check on Y as a whole.
+
+>>> If there was any other reason, I can't figure it out, and I didn't
+>>> find anything in the AIs to help. Anyone else remember? (Tucker in
+>>> particular.) More generally, anyone know of a reason not to delete
+>>> this stray "explicitly"?
+>>
+>> See above. I believe it is correct as written, given paragraph 12.
+>
+> Neither Erhard nor I see how paragraph 12 applies. Please explain how
+> this actually works (I realize this has been done before, but please try again).
+
+See example above. Let me know if this is not clear.
+
+> Specifically, in the note 7.3.2(22/3), what rule triggers the check of
+> the invariant of NT for an out parameter (on return from the call))? And why?
+> Similarly for the check of the invariant of T (again on return from
+> the call)?
+
+I don't know how NT relates to T. Hopefully you can make appropriate
+substitutions into my example above using T and T0.
+
+> When I read 7.3.2(12/3), it says that a check is made on a view
+> conversion from T to an ancestor of T. It then says something about
+> the same check being made on in out parameters. But that doesn't happen for an "in out"
+> parameter, because the conversion goes from T to NT, and NT is not an
+> ancestor of T. So there is no check to be made in that case.
+
+I believe you are slightly misreading it. The actual parameter is a "view
+conversion" from the descendant type to the ancestor type, (from T to T0 in my
+example) even though upon return, the (conceptual) value conversion actually
+goes the opposite way, namely from T0 back to T. But of course you can't really
+do the reverse as a "value conversion" for a tagged type, since you wouldn't
+know where to come up with the values for the additional components. So there
+is really no conversion going the other way, it is logically more like an
+assignment to the T0 part of the actual parameter, so it is more like:
+
+ T0(Y) := Final_Value_Of_Formal_Param;
+
+So again, the view conversion involved is from T to T0.
+even though the logical flow of data is from an object of type T0 to (the T0
+part) of an object of type T.
+
+View conversions are confusing. I would recommend rereading 4.6(52-56). For a
+tagged type, since they are passed by reference, there is no conversion "back"
+after a call for an OUT parameter. And even if there were, it would have the
+semantics of the assignment I showed above.
+
+> I can easily believe Erhard is wrong, and he got me so confused that I
+> can no longer see what the intent is much less whether the rules cover
+> that intent. (That's why I didn't quote his original message, I didn't
+> want that effect to happen to anyone else.)
+>
+> But it seems to me that something is missing here. I had thought that
+> it just was applying the explicit check to inherited subprograms (that
+> seems to be the easiest way to deal with this), but perhaps 12/3 was
+> supposed to do it (but doesn't). Or maybe 12/3 has mixed up static and
+> dynamic semantics to the point it is incomprehensible...
+>
+> Anyway, thanks in advance for the clear explanation I'm sure to receive.
+
+I hope I have clarified things, but probably not...
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, February 4, 2012 5:54 PM
+
+> I hope I have clarified things, but probably not...
+
+Doesn't look like it. :-(
+
+> I'm not sure what you meant by "NT" above. Is that the ancestor of T
+> from which it is inheriting the subprogram? I will assume that, even
+> though usually "NT" is meant to signify a *descendant* of T.
+
+Erhard was asking about the "note" 7.3.2(22/3) which talks about types NT and T.
+I've mentioned that several times, in parts of my messages that you haven't
+quoted, so I'm not surprised that you missed that.
+
+But I think we need to stick to the T and NT types, so we can understand this in
+terms of the wording that's actually in the RM.
+
+> > Specifically, in the note 7.3.2(22/3), what rule triggers the check
+> > of the invariant of NT for an out parameter (on return from the
+> > call))? And
+why?
+> > Similarly for the check of the invariant of T (again on return from
+> > the call)?
+>
+> I don't know how NT relates to T. Hopefully you can make appropriate
+> substitutions into my example above using T and T0.
+
+That's explained in the note! There's a reason that I specifically mentioned the
+note above!! Erhard (and by corollary, me) wanted to relate the note to the
+rules, and neither of us have been able to do it.
+
+So now we have three people not paying much attention to each other...
+(grumble).
+
+I would have thought that I didn't have to copy large blocks of text out of the
+RM because we can read each other...
+
+"A call of a primitive subprogram of type NT that is inherited from type T needs
+to satisfy the specific invariants of both the types NT and T. A call of a
+primitive subprogram of type NT that is overridden for type NT needs to satisfy
+only the specific invariants of type NT."
+
+Sigh. So I'll try to manually substitute the names of the types in your
+following text and see if it makes any sense.
+
+...
+> Anyway, when calling a subprogram inherited by NT from its ancestor T,
+> if there is an invariant that applies to NT, then at the point of
+> calling the inherited subprogram, what happens is that the primitive
+> of T is called, with all parameters of type T in that primitive of T
+> being passed view conversions from NT to T.
+
+Yup, knew that.
+
+> If any of them are OUT or IN OUT parameters, then based on para. 12
+> above, on the way back, a check is performed on the NT part of the
+> object that is identified in the view conversion, which in this case
+> is the whole thing.
+
+Maybe that's what's supposed to happen, but I can't see that in 7.3.2(12/3).
+Maybe the problem is that it talks about "this check" for in out parameters, but
+the previously described check as nothing to do with this case. The described
+check goes in the other direction to to the one we need here (because we're
+going from T to NT here).
+
+> For example:
+>
+> type T is ...
+> procedure Update(X : out T);
+>
+> ...
+>
+> type NT is new T with ...
+> with Type_Invariant => Is_Valid(NT) = True;
+>
+> -- Update inherited
+>
+> ...
+>
+> Y : NT;
+>
+> Update(Y);
+> --> this becomes a call on T's Update:
+
+No, it doesn't. It's a call on NT's update, that executes the body of T with
+view conversions of the parameters.
+
+Ohhh, having looked this up, I see the 3.4(27/2) actually says this. No wonder
+we have such trouble with overriding, because a model based on real calls has no
+hope of working in face of multiple inheritance and/or null/abstract subprograms
+with no implementation. Never mind that though.
+
+We have AARM notes in 7.3.2 (22.a/3) that try to explain this, but they way miss
+the mark because I don't understand the model either. Perhaps you could try
+clarifying the AARM note to repeat the entire model (it's obvious that hardly
+anyone, even inside the ARG, understands it, so writing notes that assume that
+they do isn't helping much).
+
+The AARM note at least has to mention the call model and have a cross-reference
+to 3.4.
+
+Here's an attempt:
+
+Proof: This follows from the definition of inheritance as view conversions of
+the parameters of the type {and a call to the original routine (see 3.4)}, along
+with {the normal invariant checking rules}[ the rules require checks on such
+view conversions]. {In particular, the call to the original routine takes care
+of any checks needed on type T, and the checks required on view conversions take
+care of any checks needed on type NT, specifically on in out and out
+parameters.} We require this in order that the semantics of an explicitly
+defined wrapper that does nothing but call the original routine is the same as
+that of an inherited routine.
+
+Can this be clearer still??
+
+> Update(T(Y))
+>
+> --> That "T(Y)" is a view conversion being
+> --> passed as an OUT parameter, so per para. 12, a
+> --> check on NT's invariant is performed
+> --> on Y if the call completes successfully.
+> --> If T also has an invariant, then it is checked on T(Y)
+> --> upon return from the call on T's Update, and
+> --> if that succeeds, then we would perform NT's invariant
+> --> check on Y as a whole.
+
+Back to paragraph 12/3 and the note 22/3. The note says that the above is what
+happens, so it's pretty obvious that this is the intent. But I can't see how to
+get this out of paragraph 12/3, beyond your say-so.
+
+...
+> > When I read 7.3.2(12/3), it says that a check is made on a view
+> > conversion from T to an ancestor of T. It then says something about
+> > the same check being made on in out parameters. But that doesn't
+> > happen for an "in out"
+> > parameter, because the conversion goes from T to NT, and NT is not
+> > an ancestor of T. So there is no check to be made in that case.
+>
+> I believe you are slightly misreading it. The actual parameter is a
+> "view conversion" from the descendant type to the ancestor type, (from
+> NT to T in my example) even though upon return, the (conceptual) value
+> conversion actually goes the opposite way, namely from T back to NT.
+> But of course you can't really do the reverse as a "value conversion"
+> for a tagged type, since you wouldn't know where to come up with the
+> values for the additional components. So there is really no
+> conversion going the other way, it is logically more like an
+> assignment to the T part of the actual parameter, so it is more like:
+>
+> T(Y) := Final_Value_Of_Formal_Param;
+>
+> So again, the view conversion involved is from NT to T.
+> even though the logical flow of data is from an object of type T to
+> (the NT part) of an object of type NT.
+>
+> View conversions are confusing. I would recommend rereading
+> 4.6(52-56). For a tagged type, since they are passed by reference,
+> there is no conversion "back" after a call for an OUT parameter. And
+> even if there were, it would have the semantics of the assignment I
+> showed above.
+
+Well, duh, it's obvious that they're confusing.
+
+Even with your roadmap here I'm skeptical. I can't imagine how an ordinary user
+would ever be able to figure out when this would happen (and that's necessary
+for understanding the cause of failures).
+
+At least part of the problem here is all of the emphasis on what the view
+conversion goes to (which is backwards from anything that we care about). I have
+to wonder if we care about any of that in the first place. Are there any view
+conversions from a *private* type (and outside the package) that we would *not*
+care about? I mean, don't we need to do this even for derived scalar types? (If
+T and NT are ultimately scalar types or access types, don't we still want the
+same checks of their invariants?) And you can't convert to a more derived type
+(that would require adding components, which isn't possible). So what am I
+missing
+
+So, I guess what I'm saying, is what is wrong with something like:
+
+After assigning to a view conversion, outside the immediate scope of T, that
+converts an object of type T to some other type, a check is performed on the
+part of the object that is of type T; similarly, for passing a view conversion
+as an out or in out parameter outside the immediate scope of T, this check is
+performed upon successful return;
+
+And even here I'd prefer to get rid of the "from" and "to" (since they're
+confusing beyond belief), unfortunately, I wasn't able to do it. Perhaps we
+could just drop the "to some other type" (irrelevant as previously noted), but
+that seems a bit vague:
+
+After assigning to a view conversion, outside the immediate scope of T, that
+converts an object of type T, a check is performed on the object; similarly, for
+passing a view conversion as an out or in out parameter outside the immediate
+scope of T, this check is performed upon successful return;
+
+(I dropped the whole "the part of the object" here, because it is irrelevant for
+the reverse type conversion -- the check is on the result of that reverse type
+conversion, which is the entire object. You'd need to check only a part if you
+were making the forward check to the ancestor, but if I understand you
+correctly, that is not the part that this rule is covering. To wit: an
+assignment to a view conversion of NT to T assigns just the T part, but the
+check is on the entire NT object.)
+
+By now, I have this completely wrong. Enjoy straightening me out... :-)
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Saturday, February 4, 2012 7:08 PM
+
+Tuck, my original (convoluted?) comment was:
+
+>> ================
+>>> 7.3.2 22/3 I cannot identify the rule that requires the check of the
+>>> specific invariant of type NT for the return from an inherited
+>>> subprogram of T. (It's neither 12/3 nor 14-18/3.
+>>> So, where is the rule?
+>>> Alternatively, this part of the note would need to become a rule.)
+
+I did not think that 12/3 covered the case. The first sentence talks exclusively
+about upcasts. The second says "similarly", so upcasts only.
+
+The note says:
+13 A call of a primitive subprogram of type NT that is inherited from type T
+needs to satisfy the specific invariants of both the types NT and T. A call of a
+primitive subprogram of type NT that is overridden for type NT needs to satisfy
+only the specific invariants of type NT.
+
+(Come to think of it, now the second sentence of the Note becomes very
+mysterious, too, since for a redefinition dispatchingly called via the parent
+method such an upcast would happen on the way out and hence invariants of T
+would be checked.)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, February 5, 2012 12:03 PM
+
+> I did not think that 12/3 covered the case. The first sentence talks
+> exclusively about upcasts. The second says "similarly", so upcasts
+> only.
+
+Oh boy, now we are changing the vocabulary again!
+By "upcast" I presume you mean a view conversion from a descendant to an
+ancestor. The important thing to realize is that a view conversion is
+*writable*. It doesn't really convert the data, it just provides a narrowed view
+of it, so you only see the ancestor part of some descendant. Through a view
+conversion you can willy-nilly change the ancestor part of the descendant
+object, using assignments, passing as OUT parameters, etc.
+
+The challenge is that the type-invariant on a descendant might depend on the
+consistency between data residing in the ancestor part with data in the
+extension part(s) after that. So if someone changes the ancestor part, then we
+need to recheck the various invariants of any descendants.
+
+> The note says:
+> 13 A call of a primitive subprogram of type NT that is inherited from
+> type T needs to satisfy the specific invariants of both the types NT
+> and T. A call of a primitive subprogram of type NT that is overridden
+> for type NT needs to satisfy only the specific invariants of type NT.
+
+OK, sorry I missed the reference to the Note. Thanks for copying it here. So
+what this is saying is that if NT inherits an operation from T rather than
+overriding it, both the T invariant is checked, and then the NT invariant.
+Paragraph 12 ensures that the NT invariant is checked, because a call on an
+inherited subprogram turns into a call on the ancestor's subprogram with
+controlling parameters being view conversions, so [IN] OUT controlling
+parameters which are view conversions will trigger para 12. The normal semantics
+of the subprogram call on the original T subprogram takes care of the check on
+the T invariant.
+
+If you override with a new NT subprogram, then T's invariant isn't checked as
+part of the call on this new subprogram. On the other hand, if inside this
+subprogram there is a call on a primitive of T to update the T "part" of the
+object, then there will be a check on T's invariant at that point. But that is
+buried inside the NT primitive, and we aren't worried about that in this note.
+
+> (Come to think of it, now the second sentence of the Note becomes very
+> mysterious, too, since for a redefinition dispatchingly called via the
+> parent method such an upcast would happen on the way out and hence
+> invariants of T would be checked.)
+
+You are using "upcast" in a way that is totally non-Ada-like here.
+There is *no* separate T-to-NT view conversion "on the way out,"
+on any sort of call. In fact, normally there is absolutely nothing that happens
+"on the way out." All the "damage" has already been done, since tagged types,
+including view conversions thereof, are passed by *reference.* But with
+Type_Invariants we now *do* have something done "on the way out." But the view
+conversion is still syntactically and semantically going from NT to T, even
+though you might logically think of this as some kind of "upcast" back to NT.
+*Don't think about it that way!* You will get yourself totally confused (and
+take Randy along with you ;-).
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Sunday, February 5, 2012 3:32 PM
+
+> Oh boy, now we are changing the vocabulary again!
+> By "upcast" I presume you mean a view conversion from a descendant to
+> an ancestor.
+
+Merely too lazy to spell out "a view conversion, outside the immediate scope of
+T, that converts from T or one or more record extensions (and no private
+extensions) of T to an ancestor of type T". I'll stay lazy and call this
+mouthful an "upcast" in this msg.
+
+> You are using "upcast" in a way that is totally non-Ada-like here.
+> There is *no* separate T-to-NT view conversion "on the way out,"
+> on any sort of call.
+
+My 2 a.m. mistake. I remembered the rule 6.4.1 (17):
+"After normal completion and leaving of a subprogram, for each in out or out
+parameter that is passed by copy, the value of the formal parameter is converted
+to the subtype of the variable given as the actual parameter and assigned to
+it." which for inherited ops is an "upcast" NT->T, but I forgot that
+by-reference types are excepted from being safe at this point and do not require
+"upcast" semantics.
+
+> But the view conversion is still syntactically and semantically going
+> from NT to T, even though you might logically think of this as some
+> kind of "upcast" back to NT. *Don't think about it that way!* You
+> will get yourself totally confused (and take Randy along with you .
+
+O.k., I'll try not to. But I am still trying to understand the model and find
+the rules for it. Here is my example and exegesis....
+
+Type T is tagged private;
+procedure P(X:T);
+
+Type NT is new T;
+ ...
+
+O: T'Class := new NT;
+P(O);
+
+(1) I get different semantics wrt the specific type invariants, depending on
+ whether NT redefines P. This is a bit unusual, but o.k., since these are
+ specific invariants. The semantics are....
+
+(2) When NT redefines P, then I get the specific type invariant checks for NT
+ from the implicit view conversion T->NT on the way in (11/3), and then again
+ from the return of the call (15/3-17/3 all apply), unless it is an "in"
+ parameter (which happens to be the case here). For "in" and "in out"
+ parameters, (12/3) would require the very same check again for a
+ redefinition.
+
+(3) When NT inherits P, then I get the specific type invariant checks for NT
+ from the implicit view conversion T->NT on the way in (11/3), and then the
+ check for T because ...... that is the rule that I had problems finding,
+ since 17/3 and hence all of 14/3-18/3 does not apply -- my O is an "in"
+ parameter.
+
+So where is the rule that makes the check for T in my example?
+(Don't I wish there were! But that is the "other discussion".)
+
+If there isn't one, the note is incorrect (unless, and this is a momentary
+afterthought, "needs to satisfy the invariant" is not equivalent to saying
+"needs to pass the invariant check", but the "other discussion" appears to go
+that way.).
+
+About:
+> The normal semantics of the subprogram call on the original T
+> subprogram takes care of the check on the T invariant.
+which in their entirety are spelled out by 14/3-18/3, right?
+So, no help there.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, February 5, 2012 3:59 PM
+
+> (2) When NT redefines P, then I get the specific type invariant checks
+> for NT from the implicit view conversion T->NT on the way in (11/3),
+> and then again from the return of the call (15/3-17/3 all apply),
+> unless it is an "in" parameter (which happens to be the case here).
+> For "in" and "in out" parameters, (12/3) would require the very same
+> check again for a redefinition.
+
+Now you have confused me. If NT redefines P, then there are no view conversions
+involved. So the only check that is relevant is any invariant on NT itself. T
+is irrelevant at this point. And as you point out below, P has no outputs, so no
+invariant checks.
+
+> (3) When NT inherits P, then I get the specific type invariant checks
+> for NT from the implicit view conversion T->NT on the way in (11/3),
+> and then the check for T because ...... that is the rule that I had
+> problems finding, since 17/3 and hence all of 14/3-18/3 does not apply
+> -- my O is an "in" parameter.
+
+No invariant checks at all on an IN parameter (unless you get us to change
+that). Make the mode "OUT" and then we have something to discuss.
+
+> So where is the rule that makes the check for T in my example?
+> (Don't I wish there were! But that is the "other discussion".)
+
+There are no checks on IN parameters, and the note in 22 certainly should be
+interpreted as implying there are.
+
+> If there isn't one, the note is incorrect (unless, and this is a
+> momentary afterthought, "needs to satisfy the invariant" is not
+> equivalent to saying "needs to pass the invariant check", but the
+> "other discussion" appears to go that way.)
+
+So you are complaining it doesn't repeat all of the earlier discussion? It is
+simply warning the user that above (in 12-21) we talk about the checks
+associated with a call, and the NOTE is saying that if the operation is
+inherited, then you need to worry about both the ancestor and the descendant
+type.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, February 5, 2012 4:09 PM
+
+...
+> O.k., I'll try not to. But I am still trying to understand the model
+> and find the rules for it. Here is my example and exegesis....
+>
+> Type T is tagged private;
+> procedure P(X:T);
+>
+> Type NT is new T;
+> ...
+>
+> O: T'Class := new NT;
+> P(O);
+>
+> (1) I get different semantics wrt the specific type invariants,
+> depending on whether NT redefines P. This is a bit unusual, but o.k.,
+> since these are specific invariants.
+> The semantics are....
+>
+> (2) When NT redefines P, then I get the specific type invariant checks
+> for NT from the implicit view conversion
+> T->NT on the way in (11/3), and then again from the return of
+> the call (15/3-17/3 all apply), unless it is an "in"
+> parameter (which happens to be the case here).
+> For "in" and "in out" parameters, (12/3) would require the very same
+> check again for a redefinition.
+
+When NT redefines P, there are no view conversions anywhere in the calls to the
+redefined P, and thus no checks. Unless you are talking about those occurring in
+an explicit body, and then the checks are on conversions to type T, not NT.
+
+That is, the redefinition of P is:
+
+ procedure P (X : NT) is
+ begin
+ P (T (X));
+ end P;
+
+There are no checks on NT anywhere here.
+
+If X is an in out parameter, there is a check on T on the way in, and checks on
+both T and NT on the way out. The check on T on the way in seems to be a mistake
+(I don't think there should be any checks on the way in), but doesn't seem
+possible to eliminate it.
+
+> (3) When NT inherits P, then I get the specific type invariant checks
+> for NT from the implicit view conversion
+> T->NT on the way in (11/3), and then the check for T because
+> ...... that is the rule that I had problems finding, since
+> 17/3 and hence all of 14/3-18/3 does not apply -- my O is an "in"
+> parameter.
+
+This is an in parameter, so there should be no checks at all. The check from an
+explicit conversion is unnecessary in this case, but as I said, that seems like
+a bug.
+
+Invariant checks are only on the way out of subprograms. There are never any on
+the way in. The only way to get checks on the way in is to explicit write
+something that forces a check (like an explicit conversion).
+
+> So where is the rule that makes the check for T in my example?
+> (Don't I wish there were! But that is the "other discussion".)
+
+There is no check intended, so there is no rule!
+
+> If there isn't one, the note is incorrect (unless, and this is a
+> momentary afterthought, "needs to satisfy the invariant"
+> is not equivalent to saying "needs to pass the invariant check", but
+> the "other discussion" appears to go that way.).
+
+The note is fine, it is only talking about in out and out parameters (there
+being no checks of any kind on in parameters).
+
+****************************************************************
+
+From: Erhard Ploederder
+Sent: Sunday, February 5, 2012 4:35 PM
+
+> Conversions that "cross" T are also checked.
+> That is perhaps what makes para 12 confusing, but it is there for a
+> reason.
+
+right. I worked it through and, apart from the "in" issue, the whole thing
+works. In fact, I had played through the following example, and then deleted it
+from the mail, since it did not add to my case...
+
+
+Type PT is tagged private;
+procedure P(X: in out PT);
+
+type T is new PT;
+ -- inherits P(X: in out T);
+
+Type NT is new T;
+ ...
+
+O: T'Class := new NT;
+P(O);
+
+Now, if NT inherits P, you get checks for PT and NT. If it redefines, checks are
+for NT only.
+
+****************************************************************
+
+From: Erhard Ploederder
+Sent: Sunday, February 5, 2012 4:38 PM
+
+> For "in" and "in out" parameters, (12/3) would require the very same
+> check again for a redefinition.
+Of course, I meant
+> For "out" and "in out" parameters, (12/3) would require the very same
+> check again for a redefinition.
+
+****************************************************************
+
+From: Erhard Ploederder
+Sent: Sunday, February 5, 2012 5:01 PM
+
+> When NT redefines P, there are no view conversions anywhere in the
+> calls to the redefined P
+
+Live and learn. I had it in my mind that a dispatching call achieved the
+"change" from T'Class via T (the spec to which the name binds) to NT (the impl
+dispatched to) by means of a trivially successful view conversion (as it would
+have to, if one mapped the dispatching scheme to an underlying monomorphic type
+system). I was wrong.
+
+****************************************************************
+
+From: Erhard Ploederder
+Sent: Sunday, February 5, 2012 5:09 PM
+
+A version of the note that I would have no problems with would be
+
+13 For a call of a primitive subprogram of type NT that is inherited from type
+T, the specified checks of the specific invariants of both the types NT and T
+are performed. For a call of a primitive subprogram of type NT that is
+overridden for type NT, the specified checks of the specific invariants of only
+type NT are performed.
+
+------ the present version for comparison:
+> 13 A call of a primitive subprogram of type NT that is inherited from
+> type T needs to satisfy the specific invariants of both the types NT
+> and T. A call of a primitive subprogram of type NT that is overridden
+> for type NT needs to satisfy only the specific invariants of type NT.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, February 5, 2012 6:56 PM
+
+Works for me.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, February 5, 2012 3:14 PM
+
+...
+> OK, sorry I missed the reference to the Note.
+
+Yes, I know that. Despite the fact that I mentioned it three times. Grrrr.
+
+...
+> Paragraph 12 ensures that the NT invariant is checked, because a call
+> on an inherited subprogram turns into a call on the ancestor's
+> subprogram with controlling parameters being view conversions, so [IN]
+> OUT controlling parameters which are view conversions will trigger
+> para 12.
+> The normal semantics of the subprogram call on the original T
+> subprogram takes care of the check on the T invariant.
+
+That's what paragraph 12 should say, but it is bogged down in verbal diarrhea;
+it babbles on about things that are irrelevant and thus confuses the issue to
+the point where I'm not even convinced it's right.
+
+So I want to start over with that text. I proposed a rewording in a previous
+message that you didn't read, and since I figure you won't read this one either
+(at least not in detail), I'll explain that in a separate message.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Sunday, February 5, 2012 3:28 PM
+
+> ... So, I guess what I'm saying, is what is wrong with something like:
+>
+> After assigning to a view conversion, outside the immediate scope of
+> T, that converts an object of type T to some other type, a check is
+> performed on the part of the object that is of type T; similarly, for
+> passing a view conversion as an out or in out parameter outside the
+> immediate scope of T, this check is performed upon successful return;
+
+The problem is that if a view conversion goes from a (proper) descendant of T to
+a (proper) ancestor of T, then there are checks as well. So it is not just when
+you convert from T itself. Conversions that "cross" T are also checked. That is
+perhaps what makes para 12 confusing, but it is there for a reason.
+
+>
+> And even here I'd prefer to get rid of the "from" and "to" (since
+> they're confusing beyond belief), unfortunately, I wasn't able to do
+> it. Perhaps we could just drop the "to some other type" (irrelevant as
+> previously noted), but that seems a bit vague:
+>
+> After assigning to a view conversion, outside the immediate scope of
+> T, that converts an object of type T, a check is performed on the
+> object; similarly, for passing a view conversion as an out or in out
+> parameter outside the immediate scope of T, this check is performed
+> upon successful return;
+
+Again, I believe you are losing the checks that arise in view conversions that
+"cross" T, but don't start at T.
+
+> (I dropped the whole "the part of the object" here, because it is
+> irrelevant for the reverse type conversion -- the check is on the
+> result of that reverse type conversion, which is the entire object.
+> You'd need to check only a part if you were making the forward check
+> to the ancestor, but if I understand you correctly, that is not the part that this rule is covering.
+> To wit: an assignment to a view conversion of NT to T assigns just the
+> T part, but the check is on the entire NT object.)
+>
+> By now, I have this completely wrong. Enjoy straightening me out...
+> :-)
+
+See above. I do remember struggling with this wording in Edinburgh, and almost
+every word in para. 12 was debated. So fixing it won't be easy without losing
+something.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, February 5, 2012 3:55 PM
+
+[Editor's note: This message crossed in the mail with Tucker's previous
+message.]
+
+As noted in my last message, now that I understand (again) the intent, it's
+clear to me that 7.3.2(12/3) is far more complex a rule than needed. It should
+be simplified.
+
+[For those of you with limited time, feel free to skip to the end of this
+message to see the payoff. But if you have questions, *read* my message, don't
+ask questions that I've already answered!]
+
+
+Starting from principles. What we're trying to accomplish with these checks is
+essentially:
+
+Outside of the package of type T, any modification of an object of type T should
+be checked that the invariant of T holds after the modification.
+
+OK, let's get more specific about the case of interest:
+
+Outside of the package of type T, any object of type T where all or some part of
+the object is replaced by an object of some other type should be checked that
+the invariant of T holds after the replacement.
+
+Since T has to be a private type, there aren't many cases of this. The case of
+interest involves view conversions.
+
+Still speaking informally, that means we're interested in the following
+case:
+
+Outside of the package of type T, any assignment (implicit or explicit) to a
+view conversion with a source of type T should be checked that the invariant of
+T holds after the assignment.
+
+It's important to note here that the target type of the conversion is completely
+irrelevant. It does not matter what type the replaced part of the object is,
+because we need to check the whole object afterwards. We also don't need to talk
+about "parts", because a view conversion can only change the type of the object
+itself, not that of any components. (There is no view conversion of an array of
+NT becoming an array of T, for instance.)
+
+Even if the only kind of view conversion (I'm not certain) that is relevant is a
+tagged extension conversion, that's irrelevant to both the reason for the check
+and the details of the check. So leave it out!
+
+Similarly, since this check can never have anything to do with parts, leave that
+out too. All of that extra wording just confuses the important issues.
+
+I think we also want to be a bit more explicit about what is being checked (also
+to avoid confusion).
+
+Now, I realize the wording I have above is too informal; the "in out"
+parameter case is not really an assignment at all. So we have to have a separate
+sentence to cover that.
+
+And we need something to handle the visible extension case (but again, this
+should apply to any derived type, not just extensions). The key is to
+think only of conversions between directly related types.
+
+So here's my attempt:
+
+Outside the immediate scope of T:
+ * after assigning to a view conversion that converts an object of T, a check
+ is performed on the object;
+ * after a call that passes a view conversion of an object of T as an out or
+ in out parameter, a check is performed on the actual object.
+For the purposes of determining the need for these checks, each view conversion
+is considered a set of nested view conversions including each visible ancestor
+between the source and target types.
+
+Discussion: The last rule means that if we have:
+ type T is ...
+ type NT is new T ...
+ type NNT is new NT ...
+ Obj : NNT;
+ P (... T(Obj) ...);
+then the checks are applied as if the view conversion was NT(T(Obj)).
+
+I'm sure this can be improved.
+
+The other thing that needs to be improved is the AARM note that tries to explain
+22/3, perhaps if it had been more explicit we would have headed off Erhard's
+original complaint. I put a suggestion into a previous message, and I'm not
+going to confuse the issue including it here.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, February 6, 2012 10:04 PM
+
+> > ... So, I guess what I'm saying, is what is wrong with something like:
+> >
+> > After assigning to a view conversion, outside the immediate scope of
+> > T, that converts an object of type T to some other type, a check is
+> > performed on the part of the object that is of type T; similarly,
+> > for passing a view conversion as an out or in out parameter outside
+> > the immediate scope of T, this check is performed upon successful
+> > return;
+>
+> The problem is that if a view conversion goes from a (proper)
+> descendant of T to a (proper) ancestor of T, then there are checks as
+> well. So it is not just when you convert from T itself. Conversions
+> that "cross" T are also checked.
+> That is perhaps what makes para 12 confusing, but it is there for a
+> reason.
+
+See the message that I was writing at the same time as this one. I covered that
+case.
+
+Note that an important part of the confusion is mentioning the type that we're
+converting to: the wording says that it is an "ancestor", and that seems to
+combine with the other parts of the wording. But it's definitely the case that
+the type we convert to is irrelevant, and shouldn't be mentioned at all, or at
+least should simply say "some other type". Part of the problem with the "from"
+wording is that it seems to imply a need for "to", which we don't care about
+here.
+
+Beyond that, I still stick to my contention that "extensions" are irrelevant for
+the reasons for the rule, and we ought to try to mention them as little as
+possible. Indeed, I much prefer mentioning them at the end in a "similarly"
+clause, rather than confusing everything by sticking them into the main text.
+
+---------
+
+Now for the important part: I think that the semantics described in the existing
+rule is wrong, or (more accurately) different for the inherited and explicitly
+written routines. It's not crystal clear that this should be fixed (all of these
+cases are corner cases to start with), but I wanted to raise the issue.
+
+If we are inheriting a routine from a grandparent, as in:
+
+ type T is tagged private
+ with Invariant => InvT;
+ procedure P (A : in out T);
+ Obj_T : T;
+
+ ...
+
+ type NT is new T ...
+ with Invariant => InvNT;
+ -- Inherits procedure P (A : in out NT); from T
+ Obj_NT : NT;
+ ...
+
+ type NNT is new NT ...
+ with Invariant => InvNNT;
+ -- Inherits procedure P (A : in out NNT); from NT
+ Pbj_NNT : NNT;
+
+We agree that a call P(Obj_NT) is translated to P(T(Obj_NT)), and this evaluates
+both InvT and InvNT when the routine returns (InvT from the normal rules for the
+body, InvNT from the view conversion rule).
+
+I believe that a call P(Obj_NNT) is translated to P(NT(Obj_NNT), which then
+(after applying the previous rule) becomes P(T(NT(Obj_NNT))). That means that
+such a "doubly inherited call" this evaluates all of InvT, InvNT, InvNNT when
+the routine returns (because we have two view conversions here).
+
+This is good because this is the natural implementation; the wrapper for NT's P
+would become the called body for the inherited P for NNT.
+
+OTOH, it's likely that if someone wrote this explicitly, they'd write:
+P(T(Obj_NNT)).
+
+Given the way 7.3.2(12/3) is written, this is *not* the same thing; only InvT
+and InvNNT would be evaluated for this call.
+
+I think it would be better if the semantics included any intervening invariant
+(that is, effectively you would make the checks for each intervening derived
+types). Then T(Obj_NNT) would be exactly equivalent to T(NT(Obj_NNT)). And as I
+noted in my message yesterday, if this is the case, then there is no need to
+special case any extensions (you'll pick up any invariants in the walk from the
+target type to the source type).
+
+What I don't know is what the intended semantics of a "doubly inherited call"
+is. I can't find a compelling reason to insist on evaluating InvNT (in the
+example above), so perhaps the intent was that the "middle" invariant not be
+evaluated. If so, the semantics are wrong for that case, and we need to revisit
+the wording for that reason. (I'd prefer to require it be evaluated, all other
+things being equal, but of course they're rarely equal.)
+
+I'll take another crack at improving this wording, but I'd like to know what the
+intended semantics are.
+
+> See above. I do remember struggling with this wording in Edinburgh,
+> and almost every word in para. 12 was debated. So fixing it won't be
+> easy without
+> losing something.
+
+I think that we lost sight of the big picture in favor of patching up the
+bug-de-jour. The general principle is very simple (outside of the package
+defining T, check anything that might modify an object of type T), and the case
+in question is pretty simple (after changing the result of a view conversion
+with source T, make a check of the invariant of T). The only question is whether
+intervening types need to be checked, or whether talking about types related to
+T is enough.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Tuesday, February 7, 2012 7:01 AM
+
+> I think it would be better if the semantics included any intervening
+> invariant (that is, effectively you would make the checks for each
+> intervening derived types). Then T(Obj_NNT) would be exactly
+> equivalent to T(NT(Obj_NNT)). And as I noted in my message yesterday,
+> if this is the case, then there is no need to special case any
+> extensions (you'll pick up any invariants in the walk from the target type to the source type).
+>
+> What I don't know is what the intended semantics of a "doubly
+> inherited call" is. I can't find a compelling reason to insist on
+> evaluating InvNT (in the example above), so perhaps the intent was
+> that the "middle" invariant not be evaluated.
+
+I fully agree with you (that InvNT should be evaluated). Remember that in OO
+reasoning, an NNT "is a" NT (which "is a" T). Therefore, any invariant for NT
+should hold for NNT.
+
+Imagine that the additional components added by NT depend on the components of
+T. If the invariants for NT are not evaluated, you could create an object whose
+NT part does not obey its invariant.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, February 7, 2012 8:46 AM
+
+One issue that I just thought of has to do with view conversions from a
+class-wide type to an ancestor's specific type. If you assign to such a view
+conversion, it is not clear at compile-time how many type invariants you will
+need to check. I fear this means creating a type-invariant-checking implicit
+dispatching operation. Yuck. For example:
+
+ type T is ... private ...
+ with Type_Invariant => Valid(T);
+
+ type NT is new T with private
+ with Type_Invariant => NT_Valid(NT);
+
+ type NNT is new NT with private
+ with Type_Invariant => NNT_Valid(NNT);
+
+
+ X : T'Class := ...
+
+ T(X) := ...
+ -- How many type-invariant checks need to be performed?
+
+Nasty...
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, February 7, 2012 9:24 AM
+
+> ...I fear this
+> means creating a type-invariant-checking implicit dispatching
+> operation. Yuck.
+
+Doesn't seem SO horrible. I mean, relative to some other implemetation horrors
+I can think of.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, February 7, 2012 9:57 AM
+
+True, but it was totally unexpected as far as I was concerned.
+
+I guess what the compiler will need to do is create an implicit dispatching
+operation which will take two parameters, an object and a level, and check the
+type invariant on the object, and if the level implies it, call the
+corresponding type-invariant-checking routine of its parent type. The level
+would indicate the "extension level" of the target type of the view conversion.
+
+Or I suppose it might want to call its parent type's type-invariant checker
+first if the level number indicates it is appropriate, and then if that passed
+(or was bypassed), check its own.
+
+Not that hard to do but annoying to have to create yet another implicit
+dispatching operation for the oddball case involving class-wide objects.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, February 10, 2012 2:07 AM
+
+> I guess what the compiler will need to do is create an implicit
+> dispatching operation which will take two parameters, an object and a
+> level, and check the type invariant on the object, and if the level
+> implies it, call the corresponding type-invariant-checking routine of
+> its parent type. The level would indicate the "extension level"
+> of the target type of the view conversion.
+
+This seems more complicated than necessary. Here's how I described this for the
+AARM:
+
+ For view conversions involving class-wide types, the exact checks needed may
+ not be known at compile-time. One way to deal with this is to have an implicit
+ dispatching operation that is given the object to check and the tag of the
+ target of the conversion, and which first checks if the passed tag is not for
+ itself, and if not, checks the its invariant on the object and then calls
+ the operation of its parent type. If the tag is for itself, the operation is complete.
+
+This tag comparison is the same as (the much more common) one needed for
+checking type conversions to descendant class-wide types for inclusion. And each
+such routine only makes a single check for each type, it doesn't try to pile all
+of them up, or invent a "extension level". If we have to have a dispatching
+routine, we might as well leverage that.
+
+(BTW, I don't find this that unusual. I think we have more than 10 such routines
+already, what's one more??)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, February 7, 2012 1:09 PM
+
+...
+> I think it would be better if the semantics included any intervening
+> invariant (that is, effectively you would make the checks for each
+> intervening derived types). Then T(Obj_NNT) would be exactly
+> equivalent to T(NT(Obj_NNT)). And as I noted in my message yesterday,
+> if this is the case, then there is no need to special case any
+> extensions (you'll pick up any invariants in the walk from the target type to the source type).
+
+This could also be fixed by eliminating the mention of record extensions vs.
+private extensions in para 12 (which you have been recommending), and require
+the invariant checks on all types that are "crossed" by a view conversion be
+checked:
+
+ After assigning to a view conversion, outside the immediate scope of
+ T, that converts from [T or one or more record extensions (and no
+ private extensions) of T] {a descendant of T (including T itself)} to
+ an ancestor of type T {(other than T itself)}, a check is performed
+ on the part of the object that is of type T; similarly, for passing a
+ view conversion as an out or in out parameter outside the immediate
+ scope of T, this check is performed upon successful return;
+
+> What I don't know is what the intended semantics of a "doubly
+> inherited call" is. I can't find a compelling reason to insist on
+> evaluating InvNT (in the example above), so perhaps the intent was
+> that the "middle" invariant not be evaluated. If so, the semantics are
+> wrong for that case, and we need to revisit the wording for that
+> reason. (I'd prefer to require it be evaluated, all other things being
+> equal, but of course they're rarely equal.)...
+
+It seems that the intermediate invariant should be re-checked, since if you
+change the ancestor part, then you could easily invalidate invariants of every
+descendant.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, February 8, 2012 10:25 PM
+
+> This could also be fixed by eliminating the mention of record
+> extensions vs. private extensions in para 12 (which you have been
+> recommending), and require the invariant checks on all types that are
+> "crossed" by a view conversion be checked:
+>
+> After assigning to a view conversion, outside the immediate scope of
+> T, that converts from [T or one or more record extensions (and no
+> private extensions) of T] {a descendant of T (including T itself)} to
+> an ancestor of type T {(other than T itself)}, a check is performed
+> on the part of the object that is of type T; similarly, for passing a
+> view conversion as an out or in out parameter outside the immediate
+> scope of T, this check is performed upon successful return;
+
+Ah, this is what I trying to get to on Sunday. As usual, your wording is better
+than mine. I'll write up the change this way (replacing last week's work).
+
+I still wonder if the second branch (the in out case) is a bit too vague; it
+never says that it is only talking about view conversions that meet the
+conversion rules of the previous branch. That's kind of important, and it's easy
+to read it that way because the part about being outside of the scope is
+repeated, but not the type part.
+
+Perhaps it would be better to repeat the entire thing and use bullets for the
+non-repeated part:
+
+For a view conversion, outside the immediate scope of T, that converts from a descendant of T
+(including T itself) to an ancestor of type T {(other than T itself), a check is performed on the
+part of the object that is of type T:
+ * after assigning to the view conversion; and
+ * after successful return from a call that passes the view conversion as out or in out parameter.
+
+Now there is no confusion about which cases are included (no vague similarly),
+and there's almost no duplication of wording.
+
+I think this is a big improvement, and is great. :-) What about the rest of
+you??
+
+P.S. I think either of these wordings would benefit from an AARM note that
+explains that a single view conversion could trigger this rule for multiple
+types and thus cause multiple invariant checks.
+
+
+****************************************************************
+
+From: Tullio Vardanega
+Sent: Thursday, February 9, 2012 2:24 AM
+
+The latest formulation is becoming digestible even to the likes of me.
+Perhaps this counts as an indication of convergence ;-)
+
+****************************************************************
Questions? Ask the ACAA Technical Agent