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

Differences between 1.1 and version 1.2
Log of other versions for file ai12s/ai12-0150-1.txt

--- ai12s/ai12-0150-1.txt	2015/01/27 01:58:19	1.1
+++ ai12s/ai12-0150-1.txt	2015/01/27 04:57:08	1.2
@@ -1,5 +1,7 @@
-!standard 7.3.2(5/3)                                   15-01-26  AI05-0150-1/01
+!standard 7.3.2(3/3)                                   15-01-27  AI05-0150-1/02
+!standard 7.3.2(5/3)
 !standard 7.3.2(9/3)
+!standard 7.3.2(22/3)
 !class binding interpretation 15-01-26
 !status work item 15-01-26
 !status received 15-01-26
@@ -40,8 +42,16 @@
 
 !wording
 
-Revise 7.3.2(5/3):
+Modify 7.3.2(4/3) (as modified by AI12-0041-1):
 
+   This aspect shall be specified by an expression, called an invariant
+   expression. Type_Invariant'Class may be specified on a
+   private_type_declaration, a private_extension_declaration, or a
+   full_type_declaration for an interface type.{ Type_Invariant'Class
+   determines a *class-wide type invariant*  for a tagged type.}
+
+Modify 7.3.2(5/3):
+
    [AARM Redundant: Within an invariant expression, the identifier of
    the first subtype of the associated type denotes the current instance
    of the type.] Within an invariant expression [associated with] {for
@@ -56,7 +66,7 @@
    This ensures that the invariant expression is well-defined for any
    type descended from T.]}
 
-Revise 7.3.2(9/3) as follows:
+Modify 7.3.2(9/3):
 
 (In Dynamic Semantics)
 
@@ -64,6 +74,15 @@
    T, then an invariant check is performed at the following places, on
    the specified object(s):
 
+Add after 7.3.2(22/3):
+
+   For an invariant check on a value of type T1 based on a class-wide invariant
+   expression inherited from an ancestor type T, any operations within the
+   invariant expression that were resolved as primitive operations of the
+   (notional) formal derived type NT, are in the evaluation of the invariant
+   expression for the check on T1 bound to the corresponding operations of type
+   T1.
+
 !discussion
 
 Consider two nearly identical hierarchies of types. First:
@@ -206,6 +225,21 @@
 the example above does not match the NT type, so the above problem can't
 happen.
 
+---
+
+We added "non-abstract" to 7.3.2(9/3) because a class-wide invariant cannot
+be reliably enforced on an abstract type, because some of the operations used
+in the original invariant expression might be abstract for an abstract
+descendant. Even if all of the operations are non-abstract for a particular
+abstract descendant, it seems unwise and a potential maintenance trap to have
+the enforcement of the class-wide invariant depend on that.
+
+This does not provide a hole in the checking provided by class-wide type
+invariants, even in the case of a concrete operation inherited by a descendant,
+because the checking on the implicit view conversions that are part of a call
+on an inherited subprogram will make the checks for any object of a concrete
+type. (And there cannot be an object of abstract type!)
+
 !ASIS
 
 No ASIS effect.
@@ -317,3 +351,147 @@
 understand it.
 
 ****************************************************************
+
+From: Tucker Taft
+Sent: Monday, January 26, 2015  9:10 PM
+
+>> Here is a new AI, carved off of AI12-0133 (which dealt with
+>
+> You mean AI12-0113-1 (you doubled the wrong digit).
+
+Oops.
+
+>> Pre'Class), to deal with name resolution of current instances within
+>> a Type_Invariant'Class expression.  It steals liberally from the
+>> Pre'Class AI.
+>
+> In looking at this, you don't have any wording corresponding to the
+> wording in 6.1.1(37/3):
+>
+> {Any operations within a class-wide postcondition expression that were
+> resolved as primitive operations of the (notional) formal derived type
+> NT, are in the evaluation of the postcondition bound to the
+> corresponding operations of the type identified by the controlling tag of the call on S.
+> [Redundant: This applies to both dispatching and non-dispatching calls
+> on S.]}
+>
+> It would need that we'd need wording like this somewhere (probably in
+> or after 7.3.2(22/3), although we have to be careful since not all
+> invariant checks are associated with a call. Maybe something like:
+>
+> {For any invariant check associated with the return from a call on a
+> primitive subprogram S, any operations within a class-wide type
+> invariant expression that were resolved as primitive operations of the
+> (notional) formal derived type NT, are in the evaluation of the type
+> invariant bound to the corresponding operations of the type identified
+> by the controlling tag of the call on S. [Redundant: This applies to
+> both dispatching and non-dispatching calls on S.]. Similarly, a type
+> invariant check associated with a view conversion from a specific type
+> T are bound to the corresponding operations of the type identified by
+> the type T.}
+
+Not sure why you have the first part.  Why isn't this more general.  E.g.:
+
+{For an invariant check on a value of type T1 based on a class-wide invariant expression inherited from an ancestor type T, any operations within the invariant expression that were resolved as primitive operations of the (notional) formal derived type NT,
 are in the evaluation of the invariant expression for the check on T1 bound to the corresponding operations of type T1.}
+
+> [We also probably would need to define "class-wide type invariant",
+> which not currently a term, but one I want to use every time I write
+> wording or notes for this clause.] So add something to 7.3.2(3/4), perhaps:
+>
+>      "Type_Invariant'Class determines a *class-wide type invariant*
+> for a tagged type."
+
+OK.
+
+> ===
+>
+> 7.3.2(9/3) seems to represent an unrelated bug in Type_Invariants that
+> you just noticed in trying to match the other wording. Probably should
+> say a few words about it in the !discussion.
+
+Oops, yes I meant to mention why I inserted "nonabstract."
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, January 26, 2015  9:25 PM
+
+...
+> > {For any invariant check associated with the return from a call on a
+> > primitive subprogram S, any operations within a class-wide type
+> > invariant expression that were resolved as primitive operations of
+> > the
+> > (notional) formal derived type NT, are in the evaluation of the type
+> > invariant bound to the corresponding operations of the type
+> > dentified by the controlling tag of the call on S. [Redundant: This
+> > applies to both dispatching and non-dispatching calls on S.].
+> > Similarly, a type invariant check associated with a view conversion
+> > from a specific type T are bound to the corresponding operations of
+> > the type identified by the type T.}
+>
+> Not sure why you have the first part.  Why isn't this more general.
+
+Because I couldn't figure out how to do that. That's why we keep you around.
+:-)
+
+> E.g.:
+>
+> {For an invariant check on a value of type T1 based on a class-wide
+> invariant expression inherited from an ancestor type T, any operations
+> within the invariant expression that were resolved as primitive
+> operations of the (notional) formal derived type NT, are in the
+> evaluation of the invariant expression for the check on T1 bound to
+> the corresponding operations of type T1.}
+
+Look good to me.
+
+> > [We also probably would need to define "class-wide type invariant",
+> > which not currently a term, but one I want to use every time I write
+> > wording or notes for this clause.] So add something to 7.3.2(3/4),
+perhaps:
+> >
+> >      "Type_Invariant'Class determines a *class-wide type invariant*
+> > for a tagged type."
+>
+> OK.
+>
+> > ===
+> >
+> > 7.3.2(9/3) seems to represent an unrelated bug in
+> Type_Invariants that
+> > you just noticed in trying to match the other wording.
+> Probably should
+> > say a few words about it in the !discussion.
+>
+> Oops, yes I meant to mention why I inserted "nonabstract."
+
+Could I get a few words from you? I wrote a novella when I tried it in my
+e-mail.
+
+(I'll update the AI this way, if you prefer. And 90% of ARG members prefer to
+let Randy do the work. ;-)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, January 26, 2015  10:31 PM
+
+> Could I get a few words from you? I wrote a novella when I tried it in
+> my e-mail.
+
+How about at the very end:
+
+   We added "non-abstract" to 7.3.2(9/3) because a class-wide invariant cannot
+   be reliably enforced on an abstract type, because some of the operations used
+   in the original invariant expression might be abstract for an abstract
+   descendant.  Even if all of the operations are non-abstract for a particular
+   abstract descendant, it seems unwise and a potential maintenance trap to have
+   the enforcement of the class-wide invariant depend on that.
+
+> (I'll update the AI this way, if you prefer. And 90% of ARG members
+> prefer to let Randy do the work. ;-)
+
+Thanks.
+
+****************************************************************
+

Questions? Ask the ACAA Technical Agent