CVS difference for ai05s/ai05-0254-1.txt
--- ai05s/ai05-0254-1.txt 2011/06/20 04:55:19 1.2
+++ ai05s/ai05-0254-1.txt 2011/07/23 07:12:29 1.3
@@ -1,6 +1,9 @@
-!standard 6.3.2(0) 11-06-16 AI05-0254-1/01
+!standard 6.1.1(0) 11-07-22 AI05-0254-1/02
+!standard 3.9.2(20.2/2)
!reference AI05-0247-1
!class Amendment 11-06-16
+!status Amendment 2012 11-07-22
+!status ARG Approved 9-0-3 11-06-25
!status work item 11-06-16
!status received 11-06-05
!priority High
@@ -13,7 +16,7 @@
!question
The fixes made in AI05-0247-1 have some ARG members uncomfortable.
-Should we reconsider? (No.)
+Should we reconsider? (Only the wording.)
!proposal
@@ -21,11 +24,108 @@
!wording
-** TBD.
+Modify 3.9.4(20.4/3):
-!discussion
+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 class-wide postconditions may apply -- see 6.1.1)}.
+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.
+
+Modify 6.1.1(3/3):
+
+This aspect specifies a class-wide precondition for a callable entity and its
+descendants; it shall be specified by an expression, called a class-wide
+precondition expression. If not specified for an entity, {then if no other
+class-wide precondition applies to the entity,} the class-wide precondition
+expression for the entity is the enumeration literal True.
+
+Add a new AARM Ramification after 6.1.1(3/3):
+
+If other class-wide preconditions apply to the entity and no class-wide
+precondition is specified, no class-wide precondition is defined for the entity;
+of course, the class-wide preconditions (of ancestors) that apply are still going
+to be checked. We need routines that don't have ancestors and don't specify a
+class-wide precondition to have a class-wide precondition of True, so that adding
+such a precondition to a descendant has no effect (necessary as a dispatching call
+through the root routine would not check any class-wide precondition).
+
+Replace 6.1.1(10-12/3) with:
+
+If a type T has an implicitly declared subprogram P inherited from a parent type T1
+and a homograph (see 8.3) of P from a progenitor type T2, and
+
+* the corresponding primitive subprogram P1 of type T1 is neither null nor abstract; and
+
+* the class-wide precondition expression True does not apply to P1 (implicitly or
+ explicitly); and
+
+* there is a class-wide precondition expression that applies to the corresponding primitive
+ subprogram P2 of T2 that does not fully conform to any class-wide precondition that applies to P1,
+
+then:
+
+* If the type T is abstract the implicitly declared subprogram P is *abstract*.
+
+* Otherwise, the subprogram P *requires overriding* and shall be overridden with a
+ nonabstract subprogram.
+
+
+Modify 6.1.1(23/3):
+
+The {checks are performed in an arbitrary order}[order of performing the checks
+is not specified], and if any of the
+class-wide precondition expressions evaluate to True, it is not specified
+whether the other class-wide precondition expressions are evaluated. {The
+precondition checks and any check for elaboration of the subprogram body are
+performed in an arbitrary order}[It is not
+specified whether any check for elaboration of the subprogram body is
+performed before or after the precondition checks]. It is not specified whether
+in a call on a protected operation, the checks are performed before or after
+starting the protected action. For a task or protected entry call, the checks
+are performed prior to checking whether the entry is open.
+
+Modify 6.1.1(24/3):
+
+If the assertion policy in effect at the point of a subprogram or entry
+declaration is Check, then upon successful return from a call of the
+subprogram or entry, prior to copying back any by-copy *in out* or *out*
+parameters, the postcondition check is performed. This consists of the
+evaluation of the specific and class-wide postcondition expressions that apply
+to the subprogram or entry. If any of the postcondition expressions
+evaluate to False, then Ada.Assertions.Assertion_Error is raised.
+The {postcondition expressions are evaluated in an arbitrary order}[order of
+performing the checks is not specified], and if any
+postcondition expression evaluates to False, it is not specified whether any other
+postcondition expressions are evaluated. {The postcondition check and constraint checks
+associated with copying back @b<in out> or @b<out> parameters are performed in an
+arbitrary order}[It is not specified whether any constraint checks associated with
+copying back in out or out parameters are performed before or after the postcondition
+checks].
+
+Replace 6.1.1(26/3) with:
+
+For any subprogram or entry call (including dispatching calls), the specific
+precondition check and the postcondition check [Redundant: (which checks both specific
+and class-wide postcondition expressions, if any)] that are performed are determined by
+those of the subprogram or entry actually invoked. The postcondition
+check that is performed on a call of a primitive of type T includes class-wide
+postcondition expressions that apply solely because they are defined for primitives of
+progenitors of T [Redundant: , even if the primitive is inherited from a type T1 and
+these postconditions do not apply to the corresponding primitive of T1].
+
+Replace 6.1.1(27/3) with:
+
+The class-wide precondition check for a call to a subprogram or entry consists
+solely of checking the class-wide precondition expressions that apply to the denoted
+callable entity (not necessarily the one that is invoked).
+
+For a call via an access-to-subprogram value, all precondition and postcondition checks
+performed are determined by the subprogram or entry denoted by the prefix of the Access
+attribute reference that produced the value.
-[The following is the editor's take:]
+!discussion
The broad changes made in AI05-0247-1 are necessary to preserve LSP, to
allow programmers and compilers to trust contracts, and to allow static
@@ -54,7 +154,7 @@
about False -- neither seem like a good idea.
The details of the wording to accomplish that were very hard to arrive at,
-and possibly could use more polishing.
+and needed more polishing.
However, these cases are not at all important to the success or failure of
Ada 2012. Indeed, they are just short of a pathology; still, we need to have
@@ -80,15 +180,37 @@
Of course, the programmer could be unlucky and have a collision of unrelated
routines. In that case, something will have to be renamed, and we surely will
-not want the inherited routine (it will be wrong for one use or the other).
+not want the inherited routine to come through unchanged (it will be wrong for
+one use or the other).
It is very unlikely that none of these things will happen, and everything is
-perfect -- and that is the only case where the rules that we adopt would matter.
+perfect -- and that is the only case where the rules that we adopt for collisions
+of preconditions and postconditions matter.
+
+!corrigendum 3.9.2(20.2/2)
+
+@drepl
+Force a conflict; the real text is found in the conflict file.
+@dby
+Nothing interesting.
+
+!corrigendum 6.1.1(0)
+@dinsc
+Force a conflict; the real text is found in the conflict file.
+
!ACATS test
-** TBD.
+An ACATS B-Test to check the legality rules should be constructed. Possibly,
+an ACATS C-Test should be constructed to ensure that postconditions are
+evaluated as specified in this wording.
+
+!ASIS
+
+Any ASIS impact should be have been handled as part of the original
+precondition/postcondition AI (AI05-0145-2) - this AI only affects dynamic
+semantics and legality rules and neither of those are concerns of ASIS.
!appendix
@@ -144,4 +266,392 @@
****************************************************************
+From: Tucker Taft
+Sent: Saturday, June 25, 2011 3:43 AM
+
+6.1.1 paras 10-12:
+
+ If a type T inherits homographs from a parent type T1 and a progenitor
+ type T2, and
+
+ * the corresponding primitive subprogram P1 of type T1 is neither null nor abstract; and
+ * a class-wide precondition applies to the corresponding primitive subprogram P2 of
+ T2 that does not fully conform to any class-wide precondition that applies to P1,
+
+ then:
+
+ * If the type is abstract the implicitly declared subprogram P is *abstract*.
+
+ * Otherwise, the subprogram P *requires overriding* and shall be overridden
+ with a nonabstract subprogram.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, June 25, 2011 4:00 AM
+
+6.1.1 paras 10-12 again:
+
+ If a type T inherits homographs from a parent type T1 and a progenitor
+ type T2, and
+
+ * the corresponding primitive subprogram P1 of type T1 is neither null nor abstract; and
+ * the class-wide precondition True does not apply to P1; and
+ * a class-wide precondition applies to the corresponding primitive subprogram P2 of
+ T2 that does not fully conform to any class-wide precondition that applies to P1,
+
+ then:
+
+ * If the type T is abstract the implicitly declared subprogram P is *abstract*.
+
+ * Otherwise, the subprogram P *requires overriding* and shall be overridden
+ with a nonabstract subprogram.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, June 25, 2011 4:04 AM
+
+6.1.1 paras 10-12 (one more time):
+
+ If a type T has an implicitly declared subprogram P inherited
+ from a parent type T1 and a homograph of P from a
+ progenitor type T2, and
+
+ * the corresponding primitive subprogram P1 of type T1 is neither null nor
+ abstract; and
+ * the class-wide precondition True does not apply to P1; and
+ * a class-wide precondition applies to the corresponding primitive
+ subprogram P2 of T2 that does not fully conform to any class-wide
+ precondition that applies to P1,
+
+ then:
+
+ * If the type T is abstract the implicitly declared subprogram P is
+ *abstract*.
+
+ * Otherwise, the subprogram P *requires overriding* and shall be overridden
+ with a nonabstract subprogram.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, June 25, 2011 4:08 AM
+
+6.1.1 (26) and (27):
+
+ For any subprogram or entry call (including dispatching calls), the
+ specific precondition and postcondition checks that are performed are
+ determined by those of the subprogram or entry actually invoked. The
+ class-wide postcondition check that is performed on a call of a
+ primitive of type T includes class-wide postconditions inherited from
+ progenitors of T [Redundant: , even if the primitive is inherited from
+ a type T1 and these postconditions do not apply to the corresponding
+ primitive of T1].
+
+We now take you to 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 class-wide postconditions may apply -- see
+ 6.1.1)}. 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.
+
+Back to 6.1.6(27):
+
+ For a call via an access-to-subprogram value, the class-wide precondition
+ check performed is determined by the subprogram or entry denoted by the
+ prefix of the Access attribute reference that produced the value. In
+ contrast, the class-wide precondition check for other calls to a subprogram
+ or entry consists solely of checking the class-wide preconditions that apply
+ to the denoted entity (not necessarily the one that is invoked).
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, June 25, 2011 4:27 AM
+
+6.1.1(27) again (now 2 paragraphs):
+
+ The class-wide precondition check for a call to a subprogram
+ or entry consists solely of checking the class-wide preconditions that apply
+ to the denoted callable entity (not necessarily the one that is invoked).
+
+ For a call via an access-to-subprogram value, all precondition and
+ postcondition checks performed are determined by the subprogram or entry
+ denoted by the prefix of the Access attribute reference that produced the
+ value.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, July 22, 2011 10:41 PM
+
+I had a note to index 6.1.1(24) as "unspecified". But I wonder if the wording is
+completely right. This paragraph says:
+
+If the assertion policy in effect at the point of a subprogram or entry
+declaration is Check, then upon successful return from a call of the subprogram
+or entry, prior to copying back any by-copy in out or out parameters, the
+postcondition check is performed. This consists of the evaluation of the
+specific and class-wide postcondition expressions that apply to the subprogram
+or entry. If any of the postcondition expressions evaluate to False, then
+Ada.Assertions.Assertion_Error is raised. The order of performing the checks is
+not specified, and if any postcondition expression evaluates to False, it is not
+specified whether any other postcondition expressions are evaluated. It is not
+specified whether any constraint checks associated with copying back in out or
+out parameters are performed before or after the postcondition checks.
+
+"The order of performing the checks is not specified" is not the usual way of
+saying this. Usually we would say "The checks are performed in an arbitrary
+order". That's important as "arbitrary order" has a definition (1.1.4(18)) and
+is used in other rules.
+
+However, I have to wonder if there was any intent to avoid 1.1.4(18) with this
+wording. I would guess not (Tucker is not usually that clever without
+documenting that cleverness; and I know that my earlier rewrite of this
+paragraph did not change this aspect). In particular, 6.4.1(6.17/3) does not
+apply to pre/postcondition checks whether or not "arbitrary order" is used (the
+precondition and postcondition expressions are not "direct constituents" of the
+subprogram call that caused them to be checked).
+
+So I would suggest that the last two sentences here be replaced by:
+
+The checks are performed in an arbitrary order, and if any postcondition
+expression evaluates to False, it is not specified whether any other
+postcondition expressions are evaluated. The postcondition checks and constraint
+checks associated with copying back in out or out parameters are performed in an
+arbitrary order.
+
+Any objections???
+
+P.S. An unrelated aside: as 6.4.1(6.17/3) might apply to every place in the
+standard that talks about "arbitrary order", I indexed all such places as
+"arbitrary order, allowed", and added an AARM note after 6.4.1(6.17/3) to
+suggest using the index to find those places, while noting that not all will
+apply (for instance, ones solely associated with checks or finalization won't
+trigger this rule).
+
+P.P.S. I suspect a similar rewording will be needed somewhere in the
+type_invariant section 7.3.2(0) -- I'll worry about that when I get to it in the
+next few days.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Saturday, July 23, 2011 12:38 AM
+
+Side question:
+> If the assertion policy in effect at the point of a subprogram or
+> entry
+...
+
+"subprogram or entry" is used several times in this paragraph. Why not use
+"callable entity", which is defined (6(2)) to mean exactly that?
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, July 23, 2011 12:40 AM
+
+I'm worried about the fact that class-wide preconditions have a default value of
+True if not specified.
+
+That's absolutely necessary for the conformance rules of 6.1.1(10-13/3) to work.
+For instance, the revised wording from the recent meeting includes the following
+bullet:
+
+* there is a class-wide precondition that applies to the corresponding primitive
+ subprogram P2 of T2 that does not fully conform to any class-wide precondition
+ that applies to P1,
+
+We need the class-wide precondition to be True by default to catch cases like
+the following:
+
+ package P1 is
+ type T1 is tagged private;
+ function Is_OK (Obj : T1) return Boolean;
+ procedure P (Obj : in out T1)
+ with Precondition'Class => Is_OK (Obj);
+ end P1;
+
+ package P2 is
+ type T2 is interface;
+ procedure P (Obj : in out T2); -- No class-wide precondition specified here.
+ end P2;
+
+ with P1, P2;
+ package P3 is
+ type T is new P1.T1 and P2.T2 with ...;
+ -- Inherits P1.P here.
+ end P3;
+
+This violates the rule above as True (the class-wide precondition of P2.P) does
+not conform to any class-wide precondition of P1.P (the only one is Is_OK
+(Obj)). If instead P2.P has no class-wide precondition, we'd need a more complex
+rule to detect this case (and we'd also need a more complex second bullet to
+except any subprogram that has any class-wide precondition of True).
+
+Perhaps an even more important reason that we need True to be the default is so
+that every tagged primitive has at least one class-wide precondition. If a
+routine like P2.P had no class-wide precondition, it would be possible to add
+one later for a descendant, which by definition would be stronger and would
+violate LSP.
+
+Also note that class-wide preconditions are not inherited in any way; checking a
+preconditions involves checking the class-wide preconditions of yourself and of
+all ancestors. So each subprogram has a single, unique class-wide precondition.
+
+However, this does not work in the common case that all we want for an extension
+is the same precondition as it's parent:
+
+ with P1;
+ package P3 is
+ type T3 is new P1.T1 with private;
+ overriding
+ procedure P (Obj : in out T2);
+ end P2;
+
+Here the language says that the class-wide precondition of P3.P is True. This is
+almost certainly not what we want (we probably just want to use the parent's
+class-wide precondition). True would of course eliminate the precondition of the
+parent from consideration. What we really want is for this routine to have no
+class-wide precondition of it's own.
+
+Note that none of the other contracts have this problem (extra True class-wide
+postconditions have no effect, and specific ones aren't inherited anyway).
+
+One solution would be to not have a default value from class-wide preconditions,
+but then the wording of 6.1.1(10-13/3) will have to be totally redone, and other
+wording would also have to be changed to avoid problems with later adding of
+preconditions to descendants.
+
+A better (maybe?) solution would be for the value of True to be the default if
+and only if no other class-wide precondition "applies" to the subprogram; if any
+other class-wide precondition applies, then there is no class-wide precondition
+directly for this entity (of course, the class-wide preconditions that come from
+ancestors still apply).
+
+This would require wording like (6.1.1(3/3)):
+
+This aspect specifies a class-wide precondition for a callable entity and its
+descendants; it shall be specified by an expression, called a class-wide
+precondition expression. If not specified for an entity, then if no other
+class-wide precondition applies to the entity, the class-wide precondition
+expression for the entity is the enumeration literal True.
+
+AARM Ramification:
+If other class-wide preconditions apply to the entity and no class-wide
+precondition is specified, no class-wide precondition is defined for the entity;
+of course, the class-wide preconditions (of ancestors) that apply are still
+going to be checked. We need routines that don't have ancestors and don't
+specify a class-wide precondition to have a class-wide precondition of True, so
+that adding such a precondition to a descendant has no effect (necessary as a
+dispatching call through the root routine would not check any class-wide
+precondition).
+
+[I think I prefer to not say anything normative about the unspecified/"applies"
+case; the entire explanation of the Ramification is necessary to avoid
+confusion, and that is just too much verbiage.]
+
+Can this be done better??
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, July 23, 2011 1:53 AM
+
+The wording approved at the meeting for 6.1.1(26/3) says:
+
+For any subprogram or entry call (including dispatching calls), the specific
+precondition and postcondition checks that are performed are determined by those
+of the subprogram or entry actually invoked. The class-wide postcondition check
+that is performed on a call of a primitive of type T includes class-wide
+postconditions inherited from progenitors of T [Redundant: , even if the
+primitive is inherited from a type T1 and these postconditions do not apply to
+the corresponding primitive of T1].
+
+The major problem here is that there is no such thing as a "specific
+postcondition check" or a "class-wide postcondition check". There are specific
+and class-wide postcondition *expressions*, but there is just a single
+postcondition check that covers everything (see 6.1.1(24)).
+
+This was the definition that Tucker had originally given the check, and (unlike
+the precondition cases), there was no semantic reason to split it up (they all
+work the same way, raise an exception if False). So it remains a single check.
+The second sentence here seems to be structured to recognize this reality (it
+seems to indicate that there is only a single class-wide postcondition check,
+which is bizarre as there never was any such model).
+
+We could fix this by defining these as separate checks, but that would explode
+6.1.1(24) from one paragraph into four (if the precondition wording is any
+guide.
+
+Alternatively, we could return the wording somewhat closer to its original form
+(but note this is the wording that Erhard found confusing - I added a
+parenthetical remark to clarify):
+
+ For any subprogram or entry call (including dispatching calls), the specific
+ precondition check and the postcondition check [Redundant: (which checks both
+ specific and class-wide postcondition expressions, if any)] that are performed
+ are determined by those of the subprogram or entry actually invoked. The
+ postcondition check that is performed on a call of a primitive of type T
+ includes class-wide postcondition expressions inherited from progenitors of T
+ [Redundant: , even if the primitive is inherited from a type T1 and these
+ postconditions do not apply to the corresponding primitive of T1].
+
+A second (minor) problem is that class-wide postcondition expressions are not
+"inherited"; they "apply", so the phrase "includes class-wide postconditions
+inherited from progenitors of T" is nonsense in normative text. (And "class-wide
+postconditions" is a term that is not defined at all). We could say something
+like "includes class-wide postconditions expressions that apply solely because
+they are defined for primitives of progenitors of T", but that seems pretty
+wordy. Still, I don't have a better idea. That gives:
+
+ For any subprogram or entry call (including dispatching calls), the specific
+ precondition check and the postcondition check [Redundant: (which checks both
+ specific and class-wide postcondition expressions, if any)] that are performed
+ are determined by those of the subprogram or entry actually invoked. The
+ postcondition check that is performed on a call of a primitive of type T
+ includes class-wide postcondition expressions that apply solely because they
+ are defined for primitives of progenitors of T [Redundant: , even if the
+ primitive is inherited from a type T1 and these postconditions do not apply to
+ the corresponding primitive of T1].
+
+Any improvements will be appreciated.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, July 23, 2011 2:07 AM
+
+> Side question:
+> > If the assertion policy in effect at the point of a subprogram or
+> > entry
+> ...
+>
+> "subprogram or entry" is used several times in this paragraph. Why not
+> use "callable entity", which is defined
+> (6(2)) to mean exactly that?
+
+I didn't write this, but I suspect that it's because this wording talks about
+calls quite a bit, and "call of the callable entity" is not particularly
+readable.
+
+And I don't find "callable entity" much more readable than "subprogram or entry"
+(assuming there is no problem with other conjunctions, which doesn't seem to
+happen in this paragraph). In my own writing, I'd almost always use "subprogram
+or entry" (or just forget entry altogether, can't do that in the standard of
+course). A savings of 4 characters per use doesn't make up for using "bigger"
+words and an unfamiliar term.
+
+I did a quick and sloppy check of the AARM, and found 43 occurrences of
+"callable entity" (several in index entries) and 29 occurrences of "subprogram
+or entry". I didn't make any effort to see which is used more in the normative
+text, but it seems that each is acceptable.
+
+I don't feel strongly, of course, so if there is a groundswell, I'll change it
+(and should do so in all 29 places, I think).
+
+****************************************************************
Questions? Ask the ACAA Technical Agent