CVS difference for ai05s/ai05-0262-1.txt
--- ai05s/ai05-0262-1.txt 2011/11/02 05:28:27 1.6
+++ ai05s/ai05-0262-1.txt 2011/11/09 03:33:03 1.7
@@ -1015,10 +1015,10 @@
!corrigendum 9.10(7)
@drepl
-@xbullet<If A1 is the action of issuing an entry call, and A2 is part of the corresponding
+@xbullet<If A1 is the action of issuing an entry call, and A2 is part of the corresponding
execution of the appropriate @fa<entry_body> or @fa<accept_statement>.>
@dby
-@xbullet<If A1 is the action of issuing an entry call, and A2 is part of the corresponding
+@xbullet<If A1 is the action of issuing an entry call, and A2 is part of the corresponding
execution of the appropriate @fa<entry_body> or @fa<accept_statement>;>
@@ -1841,6 +1841,254 @@
Post'Class
This aspect specifies a class-wide postcondition for an operation of a tagged
type and its descendants; ...
+
+****************************************************************
+
+From: Adam Beneschan
+Sent: Thursday, July 28, 2011 4:20 PM
+
+!topic Assertion_Policy and inherited subprograms with preconditions
+!reference 6.1.1(26,28)
+!from Adam Beneschan 11-07-28
+!discussion
+
+6.1.1(26) says, "For any subprogram or entry call (including
+dispatching calls), the specific precondition check and the
+postcondition check that is performed is determined by those of the
+subprogram or entry actually invoked".
+
+Does this imply that the Assertion_Policy that is in effect is also
+determined by the subprogram actually invoked?
+
+pragma Assertion_Policy(Check);
+package Pack1 is
+ type T1 is tagged record
+ F1 : Integer;
+ end record;
+ procedure Op1 (Obj : T1; Value : Integer)
+ with Pre => Is_Prime(Value);
+end Pack1;
+
+pragma Assertion_Policy(Ignore);
+package Pack2 is
+ type T2 is new Pack1.T1 with record
+ F2 : Integer;
+ end record;
+-- procedure Op1 (Obj : T1; Value : Integer) is inherited and
+-- not overridden
+end Pack1;
+
+Suppose we call Pack2.Op1. Is the precondition check on Value
+performed?
+
+6.1.1(28) talks about "the assertion policy in effect at the point of
+a subprogram declaration". Here, Ignore is the policy in effect at
+the implicit declaration of Pack2.Op1. However, how 6.1.1(28) is
+applied in this case depends on how "call on that subprogram" is
+interpreted: is "that subprogram" the one denoted by the call
+(Pack2.Op1), or the one whose body is invoked (Pack1.Op1)? I'm not
+clear on whether 6.1.1(26) or 3.9.2(20.4) answer this sufficiently.
+
+If the answer is that the Ignore policy applies when Pack2.Op1 is
+called, this means that Pack2.Op1 (probably) can't simply be
+implemented by having calls to Pack2.Op1 be direct calls to Pack1.Op1.
+The Implementation Note in 6.1.1(27.c) says (I think) that specific
+preconditions must be checked inside the subprogram body. But we're
+not allowed to perform those checks if Pack2.Op1 is called. So it
+looks to me that a primitive operation of a tagged type that has a
+specific precondition (such as Pack1.Op1) needs to be implemented in
+two parts---the body will check the precondition, and then call
+another Op1_Work routine that does the actual work---because Pack1.Op1
+could be inherited in a package with an Ignore policy, and we'd want
+Pack2.Op1 to be implemented as a call to Op1_Work without the checks.
+Is that pretty much correct? Is that the intent?
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, August 3, 2011 8:45 PM
+
+> Does this imply that the Assertion_Policy that is in effect is also
+> determined by the subprogram actually invoked?
+
+Of course, nothing else makes sense.
+
+> pragma Assertion_Policy(Check);
+> package Pack1 is
+> type T1 is tagged record
+> F1 : Integer;
+> end record;
+> procedure Op1 (Obj : T1; Value : Integer)
+> with Pre => Is_Prime(Value);
+> end Pack1;
+>
+> pragma Assertion_Policy(Ignore);
+> package Pack2 is
+> type T2 is new Pack1.T1 with record
+> F2 : Integer;
+> end record;
+> -- procedure Op1 (Obj : T1; Value : Integer) is inherited and
+> -- not overridden
+> end Pack1;
+>
+> Suppose we call Pack2.Op1. Is the precondition check on Value
+> performed?
+>
+> 6.1.1(28) talks about "the assertion policy in effect at the point of
+> a subprogram declaration". Here, Ignore is the policy in effect at
+> the implicit declaration of Pack2.Op1.
+> However, how 6.1.1(28) is applied in this case depends on how "call on
+> that subprogram" is
+> interpreted: is "that subprogram" the one denoted by the call
+> (Pack2.Op1), or the one whose body is invoked (Pack1.Op1)?
+> I'm not clear on whether 6.1.1(26) or 3.9.2(20.4) answer this
+> sufficiently.
+
+Since parts of these clause were extensively rewritten during the June meeting,
+I'm not sure what rules you are referring to or whether they even are in the
+Standard anymore. I didn't see anything that answers this question even remotely
+adequately.
+
+> If the answer is that the Ignore policy applies when
+> Pack2.Op1 is called, this means that Pack2.Op1 (probably) can't simply
+> be implemented by having calls to Pack2.Op1 be direct calls to
+> Pack1.Op1.
+> The Implementation Note in 6.1.1(27.c) says (I think) that specific
+> preconditions must be checked inside the subprogram body. But we're
+> not allowed to perform those checks if
+> Pack2.Op1 is called. So it looks to me that a primitive operation of
+> a tagged type that has a specific precondition (such as Pack1.Op1)
+> needs to be implemented in two parts---the body will check the
+> precondition, and then call another Op1_Work routine that does the
+> actual work---because
+> Pack1.Op1 could be inherited in a package with an Ignore policy, and
+> we'd want
+> Pack2.Op1 to be implemented as a call to Op1_Work without the checks.
+> Is that pretty much correct? Is that the intent?
+
+Well, this interpretation clearly violates Dewar's Rule (that the Standard never
+says anything silly). Assuming that *every* primitive operation (which might be
+inherited) has to be compiled in two parts if it has any pre or post-conditions
+because some other unit *might* be compiled with Ignore surely qualifies as
+silly!
+
+What the Standard means to say, however, is a difficult problem IMHO and will
+need to wait for an Ada 2012 AI. (There are other such topics.) My feeling is
+that Ignore should be treated like Suppress -- it is a *permission* to not make
+a check, not a *requirement* to not make a check. Suppress is that way in part
+because of cases like this - sometimes checks are suppressed on code inherited
+from a unit that does not have checks suppressed - in such cases, the compiler
+can do what it wants. I think the same ought to apply here. Compilers aren't
+going to leave checks that they can easily eliminate just because of laziness -
+there clearly is a performance hit to making the checks - so I don't think that
+the Standard has to require behavior here.
+
+(That's especially true as these checks are in the same "seatbelt" category as
+other checks, depending on them being eliminated should be a rarity. It's silly
+to turn off checks unless you absolutely have to for performance reasons; the
+results should never vary either way.)
+
+The alternative of rewording the standard to say that it is the subprogram that
+is invoked that determines whether or not the checks are performed would require
+completely rewriting the entirety of 6.1.1(24-33/3) [Draft 13 numbers]. (The
+text would have to say that the checks are always performed, but the evaluation
+of expressions does not happen if Ignore is set for the declaration. Or
+something like that. That's not the model currently worded.)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, August 3, 2011 9:09 PM
+
+I would recommend something simple, namely that if the policy differs between
+the explicit declaration of the subprogram actually invoked, the implicit
+declaration of some inherited subprogram, and the declaration through which a
+dispatching call is made, it is implementation-defined which policy applies.
+
+I don't agree that "Ignore" and/or "Check" can be treated merely as "advice."
+But I do agree that if one of the relevant declarations says Check and one says
+Ignore, either behavior should be permitted. This will allow implementations
+maximum freedom in terms of where they do the checks, which I think is
+important.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Wednesday, August 3, 2011 9:43 PM
+
+I don't find much different between these (I find it hard to believe that
+compilers would make checks that they don't have to make, unless there is some
+important implementation reason). But this would be fine to me. But how to
+accomplish that??
+
+(1) Do you really mean "implementation-defined" (which would require
+ documentation of the choice -- that would seem hard to provide as the choice
+ might depend on the calling sequence (which might depend on the parameter
+ types and or modes), inlining, generic instances, dispatching,
+ access-to-subprograms, inheritance, and overriding. (Hopefully not the phase
+ of the moon, but it's close.) I'd think "unspecified" would be better.
+
+(2) If you agree with the above, perhaps all we need is a To Be Honest (or do we
+ need "Adam Clarification:" in the AARM? ;-):
+
+ To Be Honest: If the assertion policy for the declaration of a callable
+ entity differs from that of the subprogram actually invoked or from that of
+ any subprogram from which it is inherited, whether a precondition or
+ postcondition check is executed is unspecified.
+
+(3) Or we could put the above text (or something like it) directly after
+ 6.1.1(33/3) [the last paragraph in the dynamic semantics, the one that talks
+ about the Ignore policy].
+
+(4) Or we could write the above as an Implementation Permission.
+
+We can probably do any of the above as a last-minute fix; none of them would
+have much chance of breaking anything (none would apply if Ignore wasn't used).
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, August 3, 2011 9:50 PM
+
+> (1) Do you really mean "implementation-defined" (which would require
+> documentation of the choice -- that would seem hard to provide as the
+> choice might depend on the calling sequence (which might depend on the
+> parameter types and or modes), inlining, generic instances,
+> dispatching, access-to-subprograms, inheritance, and overriding.
+> (Hopefully not the phase of the moon, but it's close.) I'd think "unspecified" would be better.
+
+I could live with either one. Unspecified is certainly easier to implement!
+
+>
+> (2) If you agree with the above, perhaps all we need is a To Be Honest
+> (or do we need "Adam Clarification:" in the AARM? ;-):
+>
+> To Be Honest: If the assertion policy for the declaration of a
+> callable entity differs from that of the subprogram actually invoked
+> or from that of any subprogram from which it is inherited, whether a
+> precondition or postcondition check is executed is unspecified.
+
+I think it probably should be normative.
+>
+> (3) Or we could put the above text (or something like it) directly
+> after
+> 6.1.1(33/3) [the last paragraph in the dynamic semantics, the one that
+> talks about the Ignore policy].
+
+Yes, this seems like the right place.
+>
+> (4) Or we could write the above as an Implementation Permission.
+
+I don't think it makes sense as a permission, since without the paragraph, the "correct" implementation isn't really defined.
+Normally an implementation permission allows an implementation to do something that to some degree goes against the "official"
+semantics. But here, we seem to agree that the "official"
+semantics aren't well defined when policies differ.
+>
+> We can probably do any of the above as a last-minute fix; none of them
+> would have much chance of breaking anything (none would apply if
+> Ignore wasn't used).
+
+Agreed, or just make it an early Ada 2012 AI.
****************************************************************
Questions? Ask the ACAA Technical Agent