CVS difference for ai05s/ai05-0254-1.txt

Differences between 1.3 and version 1.4
Log of other versions for file ai05s/ai05-0254-1.txt

--- ai05s/ai05-0254-1.txt	2011/07/23 07:12:29	1.3
+++ ai05s/ai05-0254-1.txt	2011/08/17 00:24:13	1.4
@@ -1,4 +1,4 @@
-!standard 6.1.1(0)                                11-07-22    AI05-0254-1/02
+!standard 6.1.1(0)                                11-07-24    AI05-0254-1/03
 !standard 3.9.2(20.2/2)
 !reference AI05-0247-1
 !class Amendment 11-06-16
@@ -11,7 +11,7 @@
 !subject Do we REALLY have contracts right?
 !summary
 
-**TBD.
+Improve the wording proposed in AI05-0247-1.
 
 !question
 
@@ -46,7 +46,7 @@
 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
+to be checked. We need subprograms 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).
@@ -106,14 +106,16 @@
 
 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].
+For any subprogram or entry call (including dispatching calls), the checks
+that are performed that verify specific precondition expressions and specific
+and class-wide postcondition expressions are determined by those for the subprogram
+or entry actually invoked. Note that the class-wide postcondition expressions
+verified by the postcondition check that is part of a call on a primitive
+of type T includes all class-wide postcondition expressions originating
+in any progenitor of T [Redundant: , even if the primitive called
+is inherited from a type T1 and some of the postcondition expressions do
+not apply to the corresponding primitive of T1].
+
 
 Replace 6.1.1(27/3) with:
 
@@ -201,10 +203,33 @@
 Force a conflict; the real text is found in the conflict file.
 
 !ACATS test
+
+An ACATS B-Test to check the newly revised legality rules should be
+constructed.
 
-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.
+ACATS C-Tests should be constructed to ensure that preconditions and
+postconditions are evaluated as specified in this wording (and AI05-0247-1).
+Specifically:
+
+ * Check that the specific precondition and the specific
+   postcondition of an inherited routine are evaluated (even though an
+   overridden routine would not have those specific pre and post conditions).
+
+ * Check that the class-wide preconditions of any (new) progenitors are
+   evaluated for a statically-bound call to an inherited routine.
+
+ * Check that the class-wide postconditions of any (new) progenitors are
+   evaluated for a statically-bound, dispatching, and access-to-subprogram
+   call to an inherited routine (of a type that doesn't have those
+   progenitors).
+
+ * Check that the class-wide preconditions of a dispatching call are those
+   of the nominal call. In particular, check the case where the dispatching
+   call is for type A, and the class-wide precondition is PA; the actual object
+   is type B derived from A with progenitor I, and class-wide precondition of
+   IA is PB, PB is True for the actual object and PA is False. In this case,
+   the precondition should fail on the dispatching call (while an incorrect
+   implementation using the precondition of the invoked call would succeed).
 
 !ASIS
 
@@ -453,6 +478,110 @@
 ****************************************************************
 
 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).
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, July 23, 2011  8:16 AM
+
+No objection.  Or as Bob might say, "shrug."
+
+> I had a note to index 6.1.1(24) as "unspecified". But I wonder if the
+> wording is completely right. This paragraph says:
+> ...
+> "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.
+> ...
+> Any objections???
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, July 23, 2011  8:51 AM
+
+No objection from me, either.  And no shrug, really
+-- although this is hardly important, Randy's proposed change is exactly right.
+
+As to "callable entity": shrug.  But Randy's worry about "call of the callable
+entity" is unwarranted -- just say "call of the entity"
+or "call of that entity", and it's clear you're talking about the callable one
+just mentioned.
+
+Or just leave it alone.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, July 23, 2011  9:03 AM
+
+> No objection from me, either.  And no shrug, really
+> -- although this is hardly important, Randy's proposed change is
+> exactly right.
+
+Oh dear.  Is this something like "putting words in your mouth"?
+Perhaps "putting a shrug in your shoulders"?  ;-)
+
+I agree, Randy's proposed change is the right one.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, July 24, 2011  7:40 PM
+
+> As to "callable entity": shrug.  But Randy's worry about "call of the
+> callable entity" is unwarranted -- just say "call of the entity"
+> or "call of that entity", and it's clear you're talking about the
+> callable one just mentioned.
+>
+> Or just leave it alone.
+
+I'm definitely in "leave it alone" mode. I don't think your suggestion works
+(everywhere). There is at least one paragraph that starts "For any subprogram
+or entry call (including dispatching calls), ...". Changing this to "For any
+callable entity call (including dispatching calls), ..." looks silly, and
+replacing it by "For any call to an entity (including dispatching calls)..."
+seems to me at least to have left out too much information (it leaves one
+wondering what sort of calls are involved).
+
+It's so late in the game that messing with correct wording doesn't seem
+worthwhile, especially when there is plenty of wording that is not quite
+right...
+
+****************************************************************
+
+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
@@ -559,7 +688,63 @@
 
 ****************************************************************
 
+From: Tucker Taft
+Sent: Saturday, July 23, 2011  8:22 AM
+
+Your proposed wording seems reasonable to me.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, July 23, 2011  4:29 PM
+
+> 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.
+
+I suggest leaving out "enumeration literal".  It's not really a piece of syntax
+that gets resolved (e.g. if there's some other True lying around we don't use
+that).  It's the True of boolean that live in Standard, and just saying "True"
+seems clear enough.
+
+Otherwise, I agree with the above wording.
+
+> 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
+
+"routines" --> "subprograms"?
+
+> 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).
+
+****************************************************************
+
 From: Randy Brukardt
+Sent: Sunday, July 24, 2011  7:33 PM
+
+> I suggest leaving out "enumeration literal".  It's not really a piece
+> of syntax that gets resolved (e.g. if there's some other True lying
+> around we don't use that).  It's the True of boolean that live in
+> Standard, and just saying "True" seems clear enough.
+
+I don't agree, as this is subject to full conformance in following Legality
+Rules and being clear that we're not talking about the value True but rather a
+specific expression True is important. (Full conformance depends on the specific
+declaration involved.) Indeed, I worry that this is still too sloppy and we
+really ought to say "enumeration literal True declared in package Standard (see
+A.1)". Probably a To Be Honest would be good enough for that.
+
+****************************************************************
+
+From: Randy Brukardt
 Sent: Saturday, July 23, 2011  1:53 AM
 
 The wording approved at the meeting for 6.1.1(26/3) says:
@@ -623,35 +808,362 @@
 
 ****************************************************************
 
+From: Tucker Taft
+Sent: Saturday, July 23, 2011  8:22 AM
+
+> 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].
+
+
+I would prefer:
+
+    For any subprogram or entry call (including dispatching calls), the checks
+    that are performed for specific precondition expressions and all
+    postcondition expressions 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 verifies class-wide postcondition
+    expressions inherited from progenitors of T ...
+
+This finesses the whole issue of whether it is considered one check or two,
+since the plural "checks" is correct either way.  It also emphasizes "all"
+instead of simply allowing it to be implicit in the use of the unqualified term
+"postcondition check."  It also avoids the notion that an expression is
+"included" in a check, since it is really the evaluation of the expression and
+the check that it is true that is included in the check, and the term "verify"
+means exactly that.
+
+
+> 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.
+
+Not real happy with that, especially the "apply solely because" part.
+How about:
+
+    For any subprogram or entry call (including dispatching calls), the checks
+    that are performed that verify specific precondition expressions and
+    specific and class-wide postcondition expressions are determined by those
+    for the subprogram or entry actually invoked.  Note that the class-wide
+    postcondition expressions verified by the postcondition check that is part
+    of a call on a primitive of type T includes all class-wide postcondition
+    expressions originating in any progenitor of T [Redundant: , even if the
+    primitive called is inherited from a type T1 and some of the postcondition
+    expressions do not apply to the corresponding primitive of T1].
+
+****************************************************************
+
 From: Randy Brukardt
-Sent: Saturday, July 23, 2011  2:07 AM
+Sent: Sunday, July 24, 2011 11:36 PM
 
-> Side question:
-> > If the assertion policy in effect at the point of a subprogram or
-> > entry
-> ...
+I wasn't happy about having to fix it in order to finish that AI, especially at
+2 am. And it surely wasn't my best work (whose is at the end of a long day?).
+
+Anyway, I think this is fine and addresses the problems with the previous
+version. I'll use it pending any further suggestions.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Monday, July 25, 2011  5:55 AM
+
+> 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.
+
+I found it "syntactically" strange that we should state omission of subsequent
+checks only for postconditions and not for constraint checks. The previous
+wording applied to both checks. To fix this, here is a suggested rewrite:
+
+-------------
+The evaluation of the postcondition expressions and any constraint checks
+associated with copying back in out or out parameters are performed in an
+arbitrary order. If any postcondition expression evaluates to False or any
+constraint check fails, it is not specified whether any other checks are
+evaluated.
+--------------
+
+Note that I replaced "postcondition check" by "evaluation of the p.c.e."
+The reason is that the manual defined "the postcondition check" as the
+combination of these evaluations (see the first two sentences of 6.1.1. (24/3).
+Incidently, 22/3 and 23/3 have the same problem for the class-wide precondition
+check. It ought to be fixed there, too.
+
+Sideremark: Maybe the term "xx-condition check" should be used for the
+evaluation of any inidividual xx-condition expression that applies, rather than
+to any combination of them. It would make the wording simpler.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, July 25, 2011  8:20 AM
+
+> I'm definitely in "leave it alone" mode.
+
+Good.
+
+>... I don't think your suggestion works  (everywhere).
+
+My suggestion was for this paragraph alone.
+
+I forgot to reply to this part of your earlier message:
+
+> 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).
+
+I am strongly opposed to changing 29 places where wording already exists from
+Ada 2005 and before!  JPR suggested a minor change to this particular paragraph,
+which IMHO should have no bearing on 29 others.  I'm all for consistency, but
+you pointed out that we use both "callable entity" and "subp or entry" all over,
+so lets live with that.
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Monday, July 25, 2011  9:07 AM
+
+> I am strongly opposed to changing 29 places where wording already
+> exists from Ada 2005 and before!  JPR suggested a minor change to this
+> particular paragraph, which IMHO should have no bearing on 29 others.
+> I'm all for consistency, but you pointed out that we use both
+> "callable entity" and "subp or entry" all over, so lets live with
+> that.
+
+Agreed.
+
+What happened is that I looked at that paragraph, asked myself "Oh, he didn't
+use 'callable entity', is there some subtle difference between 'callable entity'
+and 'subp or entry' ?", checked and saw there was none, and therefore suggested
+to use the proper term.
+
+If there are 29 of these, forget it.
+
+(apparently the term "callable entity" did not exist in Ada83, it was introduced
+with Ada 95, with probably no backward patch)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, July 25, 2011  9:52 AM
+
+> (apparently the term "callable entity" did not exist in Ada83, it was
+> introduced with Ada 95, with probably no backward patch)
+
+Right, it didn't exist in Ada 83.
+
+I invented the term "callable entity", because I thought it would simplify
+things, and as far as I remember, I intended to switch over to this term
+everywhere.  I don't know why there are still occurrences of "subprogram or
+entry":  I missed some?  Or some got added since Ada 9X?  Or during Ada 9X, by
+people I failed to inform about it? Or the wording works better with "subprogram
+or entry" in some places?
+
+Anyway, I don't think we should worry about "fixing" this little inconsistency.
+
+Note that I've gotting closer to the "if it ain't broke, don't fix it"
+philosophy, for the RM, since Ada 9X days.  In those days, I was itching to fix
+anything that looked like a bug.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Monday, July 25, 2011  6:04 AM
+
+> 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).
+
+Indeed.
+
+And as far as the rest of Randy's message goes, that merely enforces my earlier
+sideremark about the meaning of "check". We ought to define the xx-checks to
+mean the evaluation of any new or "applying" xx expression plus the raising of
+the exception as needed. All other texts could then talk in term of failing of
+sucessful checks as for all the other checking that goes on.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, July 25, 2011  6:30 AM
+
+"applying" ==> "applicable".
+"sucessful" ==> "successful"
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, July 25, 2011  9:47 PM
+
+> And as far as the rest of Randy's message goes, that merely enforces
+> my earlier sideremark about the meaning of "check".
+> We ought to define the xx-checks to mean the evaluation of any new or
+> "applying" xx expression plus the raising of the exception as needed.
+> All other texts could then talk in term of  failing of sucessful
+> checks as for all the other checking that goes on.
+
+"Check" in Ada *never* includes the raising of an exception. See the many, many
+places in the Ada Standard where we say "xxx_Error is raised if this check
+fails". (Some examples: 13.11.4(27/3), 4.6(57), 4.8(10.1/3), ...)
+
+And as far as the rest of it goes, that's exactly what it says. At least, I
+can't see any substantive difference. The only thing we care about (or should
+care about, IMHO) is that the postcondition check can be made before or after
+the parameters are copied back. There is no need for more flexibility than that.
+
+In any case, what you're asking for is a near complete rewrite of the dynamic
+semantics sections of 6.1.1 (and also of 7.3.2, type invariants, which uses the
+same wording). Most likely, the rewrite will introduce a new batch of bugs.
+(There have been plenty in the existing wording.) And you're asking for it to be
+inconsistent with the rest of the Standard. So I'd much prefer to use editor's
+discression and ignore this suggestion.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, July 25, 2011  9:28 PM
+
+> > 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.
 >
-> "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 found it "syntactically" strange that we should state omission of
+> subsequent checks only for postconditions and not for constraint
+> checks.
+
+The wording you quoted is wrong anyway, there is only one postcondition check.
+(I've fixed that in the wording used in the Standard; it's quite different than
+what was in my e-mail.) In any case, what the permission does is allows omitting
+part of the check once it has been determined it fails.
+
+A compiler never has to make other checks once one fails -- if we need to say
+that explicitly here, there would be a hundred other places in the standard
+where we would need to say the same thing. And if none of the checks fails, they
+all have to be made. (Constraint checks can't have side effects anyway, so it's
+not clear to me that anyone can tell whether they are made when they succeed.)
+
+For one example, the (normal) wording for copy back of parameters (in
+6.4.1(17)) says:
+
+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.
+These conversions and assignments occur in an arbitrary order.
+
+There is nothing here about omitting checks if one fails. I don't see any reason
+that we need to add such wording for postconditions or anywhere else for that
+matter.
 
-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.
+From: Erhard Ploedereder
+Sent: Tuesday, July 26, 2011  4:43 AM
 
-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.
+> There is nothing here about omitting checks if one fails. I don't see
+> any reason that we need to add such wording for postconditions or
+> anywhere else for that matter.
+
+Well, my point was that it was there before your rewrite. In the end, we want
+short-circuit semantics for the pre-/postcondition checks, no specified order of
+the term evaluations and (arguably?) no specified order with constraint checks
+on entry and exit.
+
+> there is only one postcondition check
+
+Definitely NOT true in the version of the RM in Edinburgh, which knows of two
+postcondition checks: 6.1.1. says
+" ... precondition checks are performed as follows:
+ The specific precondition check begins with ...
+ The class-wide precondition check begins with ....
+
+Now, I don't like that for all the reasons that you cite, but I would go in the
+opposite direction and make each expression a check. Then the "no more checks
+once the exception is raised" indeed takes care of short-circuit semantics
+without the need for extra words.
 
-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).
+****************************************************************
+
+From: Randy Brukardt
+Sent: Tuesday, July 26, 2011  5:12 PM
+
+> > There is nothing here about omitting checks if one fails. I
+> don't see
+> > any reason that we need to add such wording for postconditions or
+> > anywhere else for that matter.
+>
+> Well, my point was that it was there before your rewrite.
+
+OK, and my point was that we don't need it, so it doesn't matter if it is there or not.
+
+> In
+> the end, we want short-circuit semantics for the pre-/postcondition
+> checks, no specified order of the term evaluations and (arguably?) no
+> specified order with constraint checks on entry and exit.
+
+Right.
+
+> > there is only one postcondition check
+>
+> Definitely NOT true in the version of the RM in Edinburgh, which knows
+> of two postcondition checks:
+> 6.1.1. says
+> " ... precondition checks are performed as follows:
+> . The specific precondition check begins with ...
+> . The class-wide precondition check begins with ....
+
+Umm, I said there was only one POSTcondition check, and you responded with two
+rules about PREcondition checks. Those aren't related (yes, there are multiple
+precondition checks, but we were not talking about that rule). [Aside: One of
+the big mistakes that we made early on with pre- and postconditions was assuming
+that the rules for them could be the same; it turns out that they are wildly
+different and very little about them should be the same. That was the lesson of
+AI05-0247-1.]
+
+> Now, I don't like that for all the reasons that you cite, but I would
+> go in the opposite direction and make each expression a check. Then
+> the "no more checks once the exception is raised" indeed takes care of
+> short-circuit semantics without the need for extra words.
+
+I think you are so confused now that it would be better if you started over with
+the entire clause and reviewed it as a whole (and then decide whether you think
+there are any problems). On top of that, you don't even have the current
+wording. So I suggest you review the entire clause when the review version of
+the Standard comes out in a week or so and we can take this discussion up again
+(if necessary) once you've done that.
+
+(I need to get the rest of the Standard done so everyone can review it - the
+deadline for starting that review is upon us and I still have a number of days
+of work to finish.)
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent