CVS difference for ai05s/ai05-0250-1.txt
--- ai05s/ai05-0250-1.txt 2011/06/20 04:55:19 1.2
+++ ai05s/ai05-0250-1.txt 2011/07/28 06:05:20 1.3
@@ -1,10 +1,13 @@
-!standard 7.3.2(0) 11-06-15 AI05-0250-1/01
+!standard 7.3.2(0) 11-07-27 AI05-0250-1/02
+!standard 3.9.2(20.2/2)
!class Amendment 11-06-15
+!status Amendment 2012 11-07-27
+!status ARG Approved 10-0-1 11-06-26
!status work item 11-06-15
!status received 11-06-15
!priority Low
!difficulty Easy
-!subject Thoughts on type invariants.
+!subject Thoughts on type invariants
!summary
TBD.
@@ -28,29 +31,154 @@
!proposal
-** TBD.
+(See wording.)
!wording
-** TBD.
+Modify 3.9.4(20.4/3):
+otherwise, the action is the same as the action for the corresponding operation of
+the parent type or progenitor type from which the operation was inherited
+{except that additional invariant checks (see 7.3.2) and class-wide
+postcondition checks (see 6.1.1) may apply)}. If there is more than one
+such corresponding operation, the action is that for the operation that is not a
+null procedure, if any; otherwise, the action is that of an arbitrary one of the
+operations.
+
+In 7.3.2(2/3), replace
+
+ Type_Invariant may be specified on a private_type_declaration or a
+ private_extension_declaration.
+
+with
+
+ Type_Invariant may be specified on a private_type_declaration, on a
+ private_extension_declaration, or on a full_type_declaration that
+ declares the completion of a private type or private extension.
+
+Add an AARM Note after 7.3.2(3/3):
+
+ Reason: A class-wide type invariant cannot be hidden in the private part, as
+ the creator of an extension needs to know about it in order to conform to it
+ in any new or overriding operations. On the other hand, a specific type
+ invariant is not inherited, so that no operation outside of the original
+ package needs to conform to it; thus there is no need for it to be visible.
+
+Add before 7.3.2(7/3):
+
+ [Redundant: If the Type_Invariant aspect is specified for a type T,
+ then the invariant expression applies to T.]
+
+Replace 7.3.2(9-16/3) by
+
+ * After successful default initialization of an object of type T,
+ the check is performed on the new object;
+
+ * After successful conversion to type T, the check is performed on
+ the result of the conversion;
+
+ * 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;
+
+ * After a successful call on the Read or Input stream attribute of
+ the type T, the check is performed on the object initialized by
+ the stream attribute;
+
+ * Upon successful return from a call on any subprogram or entry that:
+
+ - is explicitly declared within the immediate scope of type T
+ (or by an instance of a generic unit, and the generic is
+ declared within the immediate scope of type T), and
+
+ - is visible outside the immediate scope of type T or overrides
+ an operation that is visible outside the immediate scope of T, and
+
+ - has a result with a part of type T, or one or more IN OUT or
+ OUT parameters with a part of type T, or an access to variable
+ parameter whose designated type has a part of type T.
+
+ the check is performed on each such part of type T.
+
+Modify 7.3.2(17/3):
+
+The invariant check consists of the evaluation of each invariant expression
+that applies to T, on each of the objects specified above. If any of these
+evaluate to False, Ada.Assertions.Assertion_Error is raised at the point of
+the object initialization, conversion, or call. If a given call requires more
+than one evaluation of an invariant expression, either for multiple objects
+of a single type or for multiple types with invariants, [the order of ]the
+evaluations {are performed in an arbitrary order}[is not specified],
+and if one of them evaluates to False, it
+is not specified whether the others are evaluated. Any invariant check is
+performed prior to copying back any by-copy in out or out parameters.
+{Invariant checks, any postcondition check, and any constraint checks associated
+with by-copy in out or out parameters are performed in an arbitrary order.}
+[It is not specified whether any constraint checks associated with by-copy in
+out or out parameters are performed before or after any invariant checks. It is
+not specified whether any postcondition checks are performed before or after any
+invariant checks.]
+
+Replace 7.3.2(18/3) by:
+
+The invariant checks performed on a call are determined by the subprogram or
+entry actually invoked, whether directly, as part of a dispatching call, or as
+part of a call through an access-to-subprogram value.
+
+Add after 7.3.2(19/3):
+
+Note: A call of a primitive subprogram of type NT that is inherited from type T
+will need to satisfy the specific invariants of both the types NT and T. A call
+of a primitive subprogram of type NT that is redefined for type NT need to
+satisfy only the specific invariants of type NT.
+
+
!discussion
+
+Item (1) is addressed in the wording proposal above.
-** TBD.
+For item (2), it seems premature to define such restrictions. Implementations
+can define their own; and we'll revisit this next time.
-[Editor's note: For (3), the language *does* make such a distinction, but it
+For item (3), the language *does* make such a distinction, but it
makes it between subprograms, not calls. Subprograms declared in the visible
part are external, others are internal. This also seems right: A called
subprogram doesn't know who is its caller, so if it is externally callable, it
-needs to ensure the invariant is true on return.
+needs to ensure the invariant is true on return. This seems right, so no
+change is needed now.
+
+The change to 7.3.2(17/3) is to use the "arbitrary order" wording used by the
+rest of the standard.
+
+The remaining changes are to clarify when checks are and are not performed, and
+to fix holes caused by view conversions.
-The mail from Yannick Moy suggests that this is in fact the correct solution. So
-we probably want no action on (3).]
+!corrigendum 3.9.2(20.2/2)
+@drepl
+Force a conflict; the real text is found in the conflict file.
+@dby
+Nothing interesting.
+
+!corrigendum 7.3.2(0)
+
+@dinsc
+
+Force a conflict; the real text is found in the conflict file.
+
!ACATS test
+
+Create ACATS C-Tests to ensure that the invariant checks are made in all of
+the defined cases.
-** TBD.
+!ASIS
+No ASIS impact (beyond the original AI).
+
!appendix
From: Steve Baird
@@ -504,14 +632,425 @@
From: Yannick Moy
Sent: Friday, June 17, 2011 2:01 AM
->>> ... What would be the problem with this (simple) rule enforcing
+>>> ... What would be the problem with this (simple) rule enforcing
>>> invariant only on external subprograms?
->
+>
>> As Randy pointed out, this is exactly what Ada 2012 does.
->
-> But thanks for confirming that we have it right already. It's one less
+>
+> But thanks for confirming that we have it right already. It's one less
> thing to worry about. :-)
thanks for the good news that I'll transmit with pleasure to our customer!
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, June 20, 2011 2:32 PM
+
+>> It would be useful to have the option of specifying the Invariant
+>> aspect with the full declaration of the type instead of only at the
+>> declaration of the partial view of the type.
+
+> It certainly makes perfect sense to make the Invariant private, since
+> it is really something to support the implementation, not the client.
+
+There seems to be general support for this idea.
+
+Just so that we have a concrete proposal to discuss (whether in Edinburgh or
+later), here is a proposed wording change.
+
+====
+
+!wording
+
+In 7.3.2(2/3), replace
+
+ Type_Invariant may be specified on a private_type_declaration or a
+ private_extension_declaration.
+
+with
+
+ Type_Invariant may be specified on a private_type_declaration, on a
+ private_extension_declaration, or on a full_type_declaration which
+ declares the completion of a private type or private extension.
+
+In 7.3.2(3/3), replace
+
+ Type_Invariant'Class may be specified on a private_type_declaration
+ or a private_extension_declaration.
+
+with
+
+ Type_Invariant'Class may be specified on a private_type_declaration,
+ on a private_extension_declaration, or on a full_type_declaration
+ which declares the completion of a private type or private extension.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Saturday, June 25, 2011 3:35 AM
+
+This is how I understand the most recently proposed principles:
+
+Within the full view of a type, its class-invariants are not checked.
+
+Reason: As plain assigments to visible components could violate the invariants
+without any checking preventing it, it makes no sense to check invariants, if
+said changes are effected by calls on some subprograms.
+
+Within a partial view of the declared type of a variable, all
+(redundant: dispatching or non-dispatching) calls on primitive operations of
+this type with the variable as controlling/first argument check all
+class-invariants of the actual type of the object denoted by the variable. (In
+addition, any non-class invariant is checked - presumably the one that matches
+the view for the call.)
+
+Reason: It should be guaranteed that despite potential up-casts (i.e., view
+conversions) and even in the presence of statically bound calls, the invariants
+of the object cannot be violated by the completed call.
+
+-------------------------
+
+Other questions (which may or may not be answered already by the RM:
+
+Are invariants and post-conditions checked when the call completes with an
+exception? Presumably not, but where does it say that?
+
+Why aren't invariants checked upon entry as well? They are supposed to hold
+there, too. For types that have visible components this would make a lot of
+sense. For fully private types, they are guaranteed by the last call.
+
+How do class-wide operations play here?
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Saturday, June 25, 2011 6:44 AM
+
+This is how I understand the most recently proposed principles ( further amended
+to make them work reasonably):
+
+Within the full view of a type, its class-invariants are not checked.
+
+Reason: As plain assigments to visible components could violate the invariants
+without any checking preventing it, it makes no sense to check invariants, if
+said changes are effected by calls on some subprograms instead.
+
+(Possible variation, if deemed easier to implement or safer: the
+class-invariants of the static view of the subprogram are checked.)
+
+Within a partial view of a type, all (redundant: dispatching or non-dispatching)
+calls on subprograms whose body has a full view of this type and has an actual
+parameter of the type check all class-invariants of the actual type of the
+object denoted by the parameter. Multiple such parameters cause multiple such
+checks. (In addition, any non-class invariant is checked - presumably the one
+that comes with the body of the subprogram, whichever it might be.)
+
+Reason: It should be guaranteed that despite potential up-casts and even in the
+presence of statically bound calls, the invariants of the type of the !object!
+cannot be violated by the completed call.
+
+-------------------------
+
+Other questions (which may or may not be answered already by the RM:
+
+Are invariants and post-conditions checked when the call completes with an
+exception? Presumably not, but where does it say that?
+
+Why aren't invariants checked upon entry as well? They are supposed to hold
+there, too. For types that have visible components this would make a lot of
+sense. For fully private types, they are guaranteed by the last call and hence
+could be optimized away.
+
+When can the checks be optimized away? (even in the presence of
+unchecked_* stuff?)
+
+(How do class-wide operations play? They are included in the above, as are any
+other subprograms that have visibility to the type's details.)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, June 25, 2011 10:26 AM
+
+Replace the 7.3.2(10-16/3) with:
+
+ Static Semantics
+
+ [Redundant: If the Type_Invariant aspect is specified for a type T,
+ then the invariant expression applies to T.]
+
+ [Redundant: If the Type_Invariant'Class aspect is specified for a tagged type
+ T, then the invariant expression applies to all descendants of T.]
+
+ Dynamic Semantics
+
+ If one or more invariant expressions apply to a type T, and the
+ Assertion_Policy (see 11.4.2) at the point of the partial view declaration for
+ T is Check, then an invariant check is performed at the following places, on
+ the specified object(s):
+
+ * After successful default initialization of an object of type T,
+ the check is performed on the new object;
+
+ * After successful conversion to type T, the check is performed on
+ the result of the conversion;
+
+ * 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;
+
+ * After a successful call on the Read or Input stream attribute of
+ the type T, the check is performed on the object initialized by
+ the stream attribute;
+
+ * Upon successful return from a call on any subprogram or entry that:
+
+ - is explicitly declared within the immediate scope of type T
+ (or is a part of an instance of a generic unit declared within
+ the immediate scope of type T), and
+
+ - is visible outside the immediate scope of type T or overrides
+ an operation that is visible outside the immediate scope of T,
+
+ - has a result with a part of type T, or one or more IN OUT or
+ OUT parameters with a part of type T, or an access to variable
+ parameter whose designated type has a part of type T.
+
+ the check is performed on each such part of type T.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, June 26, 2011 4:25 AM
+
+Modify 3.9.2(20.4):
+
+otherwise, the action is the same as the action for the corresponding operation
+of the parent type or progenitor type from which the operation was inherited
+{except that additional invariant checks (see 7.3.2) and class-wide
+postcondition checks (see 6.1.1) may apply}. If there is more than one such
+corresponding operation, the action is that for the operation that is not a null
+procedure, if any; otherwise, the action is that of an arbitrary one of the
+operations.
+
+Delete 7.3.2(18/3).
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Sunday, June 26, 2011 4:51 AM
+
+Proposed Wording:
+
+Note: A call on a primitive subprogram of type NT that is inherited from type T
+will need to satisfy the specific invariants of both the types NT and T. A call
+on a primitive subprogram of type NT that is redefined for type NT will need to
+satisfy only the specific invariants of the type NT.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Monday, June 27, 2011 1:54 AM
+
+> Other questions (which may or may not be answered already by the RM:
+>
+> Are invariants and post-conditions checked when the call completes
+> with an exception? Presumably not, but where does it say that?
+
+I guess that's the meaning of "successful return" in:
+
+ * Upon successful return from a call on any subprogram or entry that: [...]
+
+> Why aren't invariants checked upon entry as well? They are supposed to
+> hold there, too. For types that have visible components this would
+> make a lot of sense. For fully private types, they are guaranteed by
+> the last call.
+
+AI says:
+
+> The invariant checks are performed as postcondition checks to ensure
+> that violations are caught as soon as possible. Presumably the
+> invariants could also be enforced as preconditions, but those checks
+> would in general be redundant, and the failures would be harder to
+> track down since the call that actually created the problem would be
+> harder to identify.
+
+I would add as an important benefit that invariant is not checked at all on
+calls to functions taking only IN parameters. This is crucial to be able to have
+calls to (public) functions or expression functions in invariants. Otherwise
+you'd get an infinite loop.
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Monday, June 27, 2011 2:02 AM
+
+The AI wording you sent does not contain the proposed amendment sent by Steve on
+2011/06/20, to allow invariants being defined on full_type_declaration for a
+private type. (with the possibility of direct component access in the invariant)
+
+Does that mean this amendment was not adopted?
+
+BTW, the example in !proposal should mention Type_Invariant, not Invariant.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, June 30, 2011 2:33 PM
+
+...
+> The AI wording you sent does not contain the proposed amendment sent
+> by Steve on 2011/06/20, to allow invariants being defined on
+> full_type_declaration for a private type.
+> (with the possibility of direct component access in the invariant)
+>
+> Does that mean this amendment was not adopted?
+
+No, it means that Tuck started with an obsolete AI rather than the current
+wording of the Standard as amended by the first day of the meeting.
+
+It will be the editor's job (that is, me) to merge all of the various decisions
+into a single whole.
+
+In this case, there was some concern about whether Type_Invariant'Class should
+be required to be visible (because it affects child types), while there is no
+reason for specific Type_Invariants to be visible. Deciding that was deferred,
+and I'm not sure that we ever actually decided that (I didn't see a decision in
+a quick scan of my notes).
+
+We ought to do that. ;-)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, July 27, 2011 9:36 PM
+
+Actually, after reading my notes carefully, what happened is that we immediately
+decided to adopt Steve's wording of June 20th (changing "which" to "that") for
+Type_Invariant only (not Type_Invariant'Class, since descendants need to know
+about it in order to write operations correctly). That happened in the first 30
+minutes of the meeting.
+
+We then spent the entire remainder of the 3 day meeting changing type invariants
+(doing other things in between discussions), not concluding until there was 30
+minutes left in the meeting. By then, we'd totally forgotten about the initial
+decision.
+
+I'm going to presume that we still intend this change (I can't think of any
+reason why not), so anyone that disagrees should speak up.
+
+P.S. I didn't actually explain the change:
+
+In 7.3.2(2/3), replace
+
+ Type_Invariant may be specified on a private_type_declaration or a
+ private_extension_declaration.
+
+with
+
+ Type_Invariant may be specified on a private_type_declaration, on a
+ private_extension_declaration, or on a full_type_declaration that
+ declares the completion of a private type or private extension.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, July 1, 2011 8:17 AM
+
+> !standard 7.3.2 (00) 10-10-19 AI05-0146-1/08
+
+This AI is inconsistent about the name of the aspect -- Invariant versus
+Type_Invariant. IMHO it should be Invariant, because "Type_" is just noise --
+you can see from the syntax that it applies to the type it's attached to.
+
+If we had package invariants, they should be called Invariant, too, not
+Package_Invariant.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, July 1, 2011 6:54 PM
+
+> > !standard 7.3.2 (00)
+> 10-10-19 AI05-0146-1/08
+>
+> This AI is inconsistent about the name of the aspect -- Invariant
+> versus Type_Invariant.
+
+No, it's not. The !wording consistently uses Type_Invariant. The examples are
+just plain wrong, and all that means is that someone forgot to update them. Big
+deal.
+
+In any case, this AI is not going to be changed, because it is already WG 9
+approved. AI05-0250-1 will include the changes we approved at the meeting.
+
+> IMHO it should be
+> Invariant, because "Type_" is just noise -- you can see from the
+> syntax that it applies to the type it's attached to.
+
+Huh? We use exactly the same syntax for subtype predicates. They don't apply to
+the type, only the subtype.
+
+The whole point of saying "Type_Invariant" is to make it clear that this is
+type-related, as opposed to predicates, which are subtype-related. These use the
+same syntax and are allowed on some of the same declarations (and conceivably
+could be used at the same time on a declaration). Recall that the name of the
+predicates was "Subtype_Predicate" before we split them into static and dynamic
+versions -- these really should be Static_Subtype_Predicate and
+Dynamic_Subtype_Predicate, but those are too long. There was a lot of confusion
+about the difference between these two, and we wanted to make it crystal clear
+which was which. That need has not gone away (even if the ARG itself is more
+comfortable with the distinction).
+
+In any case, we just spent 1/3 of the recent meeting talking about "type
+invariants", and that would have been the perfect time to raise this issue. I
+have to assume you really don't feel that strongly about it or you would have
+had to say something! It's now effectively too late, in that with the holidays
+and summer vacations, it will be impossible to have a discussion with everyone
+involved. (And e-mail discussions tend to be dominated by a handful of people.)
+And quite frankly, naming discussions are interminable and a bad use of my (and
+everyone else's) limited time. (30 messages = 1 hour of my time on average.)
+
+> If we had package invariants, they should be called Invariant, too,
+> not Package_Invariant.
+
+Perhaps, but there is no possibility of confusion there (there isn't any such
+thing as a subpackage). And in any case, we don't have package invariants and
+are unlikely to ever have them (the semantic problems aren't suddenly going to
+disappear at some point in the next 5 years), so what they might be called seems
+irrelevant.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, July 1, 2011 5:54 AM
+
+>...(30 messages = 1
+> hour of my time on average.)
+
+That's an interesting statistic. I get about 300 emails per day, mostly on
+report@adacore.com. (That's week days; I think it's less than 100 on weekend
+days.) So if I spent 1 hour per 30, I'd spend 10 hours a day doing nothing but
+reading and filing email. Yikes!
+
+****************************************************************
+
+From: John Barnes
+Sent: Saturday, July 2, 2011 9:50 AM
+
+And the Rat says Type_Invariant, so that's that.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, July 2, 2011 11:30 AM
+
+Hmm, this could save Randy and the rest of us a lot of trouble. Let's just go
+by what's in the Rat, and forget about this silly RM document.
****************************************************************
Questions? Ask the ACAA Technical Agent