CVS difference for ai05s/ai05-0290-1.txt
--- ai05s/ai05-0290-1.txt 2012/03/17 03:38:53 1.3
+++ ai05s/ai05-0290-1.txt 2012/03/17 04:18:16 1.4
@@ -1,5 +1,15 @@
-!standard 3.2.4(0) 12-02-25 AI05-0290-1/03
+!standard 3.2.4(0) 12-02-26 AI05-0290-1/04
+!standard 6.1.1(0)
!standard 7.3.2(0)
+!standard 11.4.2(5/2)
+!standard 11.4.2(6/2)
+!standard 11.4.2(7/2)
+!standard 11.4.2(9/2)
+!standard 11.4.2(10/2)
+!standard 11.4.2(17/2)
+!standard 11.4.2(18/2)
+!standard 11.5(7.2/2)
+!standard 11.5(25)
!class Amendment 12-02-14
!status Amendment 2012 12-02-14
!status work item 12-02-14
@@ -9,9 +19,12 @@
!subject Improved control over assertions
!summary
-** TBD **
+The pragma Assertion_Policy is expanded to allow control of assertion
+expressions in a way that is very similar to pragma Suppress.
-!proposal
+A perceived problem with Pragma Suppress for inlined calls is fixed.
+
+!problem
When assertions (particularly predicates and preconditions) are used in
3rd party libraries of packages (which can also describe reusable code
@@ -26,303 +39,187 @@
However, assertions used to make internal correctness checks (such as
postconditions and invariants) are less important - actions of the client
should not be able to cause these to fail.
-
-As such, there should be some separation between these types of assertions.
-
-We make the following proposals:
-
-Proposal #1: The assertion policy in effect at the point of the declaration of a
- subtype with a predicate is the one used to determine whether it is checked
- or not (rather than the assertion policy at the point of the check, as it is
- currently proposed in the draft Standard).
-
-Reason: It should be possible for the body of a subprogram to be able to
- assume that checks are on for all calls to that subprogram. The rules for
- preconditions (and invariants and postconditions as well) already determine
- whether checks are made by the policy at the point of the subprogram
- declaration, which gives this property. It's weird that predicates are
- different.
-
-
-Proposal #2: If the invoked subprogram and denoted subprogram of a dispatching
- call have different assertion policies, it is unspecified which is used for
- a class-wide invariant.
-
-Reason: This is fixing a bug; invariants and postconditions should act the
- same and this is the rule used for postconditions (otherwise, the compiler
- would always be required to make checks in the body in case someone might
- turn off the checks elsewhere, not something we want to require).
+Hence, there needs to be fine control over the checks of various kinds
+of assertions. Control for any but the Assert Pragma cannot be
+sensibly based on a policy in effect at the point of the check. For
+example, this would make invariant checks to be performed only occasionally.
+The proposal that the policy in effect at the time of the aspect specification
+controls all its checks.
-Proposal #3: Provide an additional assertion policy "Check_External_Only". In
- this policy, Preconditions and Predicates are checked, and others
- (Postconditions, type invariants, and pragma asserts) are ignored.
-
-Reason: Once unit testing is completed for a package,
- assertions that are (mostly) about checking the correctness of a body are
- not (necessarily) needed. However, assertions that are (mostly) about
- checking the correctness of calls are needed so long as new calls are being
- written and tested (which is usually so long as the package is in use). So
- it makes sense to treat these separately.
-
-
-Proposal #4: There is a boolean aspect "Always_Check_Assertions" for packages
- and subprograms. If this aspect is True, the assertions that belong to and
- are contained in the indicated unit are checked, no matter what assertion
- policy is specified.
-
-Reason: There ought to be a way for a program unit to declare that it
- requires assertion checks on for proper operation. This ought to include
- individual subprograms. This as an aspect since it applies to
- a program unit (package or subprogram), but a pragma would also work. This
- aspect (along with pragma Unsuppress) would allow a library like Claw to not
- only say in the documentation (that no one ever reads) that turning off
- checks and assertions is not supported, but also to declare that fact to the
- compiler and reader (so checks are in fact not turned off unless some
- non-standard mode is used).
-
- Note that we have a similar capability for constraint checks (pragma
- Unsuppress), and it seems unfortunate to have more control over those
- checks (which are cheaper and thus less necessary to turn off).
-
-Alternative to #4: An alternative would be to push this to runtime. In
- particular, if we defined an attribute 'Assertions_Checked (allowed
- on subtypes and subprograms, returns True if the Assertion_Policy
- is Check for the declaration of the indicated entity), then the
- subprogram can defend itself without any extra runtime cost.
-
- If we in addition defined an attribute 'Pre_Check that explicitly
- invoked the precondition and predicate checks on the parameters of
- a subprogram, then bulletproofing a subprogram would just require
- writing:
- if not Sub'Assertions_Checked and then Sub'Pre_Check then
- raise Assertion_Error with "Failed preconditions with checking off";
- end if;
- This would not generate any code if assertion checking is on (as the
- checking code would be known to be dead at compile-time and would be
- removed by any barely competent compiler).
-
- It's interesting to note that a subprogram so protected would probably
- run faster with precondition checking on, as in that case the compiler
- could optimize out unnecessary checks at compile-time at the call site
- when checks are on, but with them off, they're generated inside of the
- body and are immune to optimization. That's why the original proposal
- is preferred (the cost doesn't change when checks are turned off).
-
-=====================
-
-Since this AI was created, a number of additional issues/proposals have been
-made in e-mail. Since these proposals provide possible solutions for some of
-the issues described above, they're briefly outlined here. (Note that these are
-all related.)
-
-Issue #1: All assertions are described as "checks" other than subtype
-predicates. This should be normalized (they call should be checks, or none
-should).
-
-Issue #2: If these are checks, should pragma Suppress work on them? If so,
-Suppress(All_Checks) should suppress assertions. Tucker reports that Sofcheck
-derived compilers always have worked this way (but there is an incompatibility
-for pragma Assert if it did not do so in the past).
-
-Issue #3: If these are checks, should there be check names for assertions
-(as a group, or individually, or both)? Note that having such control and
-individual check names would solve the problems that Proposals #3 and #4 are
-intended to solve (because pragma Unsuppress would serve the needed purpose
-for #4, and Suppress(Post_Check) and the like would provide the effect of #3.
-
-Issue #4: If suppress acts on assertions, can that a failed but unchecked
-assertion make the program erroneous? (The answer appears to be no.)
-
-Issue #5: How does suppress interact with Assertion_Policy? In particular,
-can Assertion_Policy override Suppress (one hopes not, or the solution
-to Proposal #4 goes away). Perhaps Assertion_Policy Ignore should be considered
-equivalent to Suppress (All_Assertion_Checks).
+!proposal
-Issue #6: Suppress is a "permission" to not check, while Assertion_Policy is
-a "requirement" to not check. The Suppress mechanism is more attractive.
+(See wording.)
!wording
-** TBD **
+Modify 2.8(3-4) as follows:
- We will need to define the terms "class-wide invariant" and "specific
- invariant", since we keep finding ourselves talking about them and the
- parallel with preconditions (where these are defined terms) makes it even
- more likely that everyone will use them. Best to have a definition. This
- will simplify the wording for #2.
-
+ pragma_argument_association ::=
+ [pragma_argument_identifier =>] name
+ | [pragma_argument_identifier =>] expression
+{ | [pragma_argument_aspect_mark =>] name
+ | [pragma_argument_aspect_mark =>] expression }
+
+ In a pragma, any pragma_argument_associations without a
+ pragma_argument_identifier {or pragma_argument_aspect_mark} shall
+ precede any associations with a pragma_argument_identifier {or
+ pragma_argument_aspect_mark}.
+
+
+-------------
+
+modify 3.2.4() to:
+
+ The *predicate* of a subtype consists of {the "and" of} all predicate
+ specifications that apply {to it and occur at a point where the
+ assertion policy in effect requires the corresponding
+ Static_Predicate or Dynamic_Predicate check}[, and-ed together]; if
+ {there are} no {such} predicate specifications[ apply], the predicate
+ is True [Redundant: (in particular, the predicate of a base subtype
+ is True)].
+
+delete 3.2.4 22/3.
+
+
+
+-------------
+
+Modify 6.1.1 31/3 to:
+
+If required by the Pre or Pre'Class assertion policies (see 11.4.2) in
+effect at the point of a corresponding aspect specification applicable to a
+given subprogram or entry, then upon a call of the subprogram or entry, after
+evaluating any actual parameters, precondition checks are performed as
+follows:
-Proposal from Erhard during ARG Meeting #46. [Other parts of AI need updating.]
-This replaces parts of 11.4.2.
+Modify 6.1.1. 35/3 to:
+
+If required by the Post or Post'Class assertion policies (see 11.4.2) in
+effect at the point of a corresponding aspect specification applicable
+to a given subprogram or entry, 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.
+
+delete 6.1.1 40/3
+-------------
+
+Modify 7.3.2 9/3 to:
+
+If required by the Type_Invariant or Type_Invariant'Class assertion
+policies (see 11.4.2) in effect at the point of a corresponding aspect
+specification applicable to a type T, then an invariant check is
+performed at the following places, on the specified object(s):
+Delete 7.3.2 23/3
-Pragma Assertion_Policy is used to control whether assertions are to be ignored
-by the implementation, checked at run time, or handled in some
-implementation-defined manner.
+Replace 11.4.2, 5/2 - 7/2 by:
The form of a pragma Assertion_Policy is as follows:
pragma Assertion_Policy(policy_identifier);
- pragma Assertion_Policy(assertion_kind => policy_identifier
- {, assertion_kind => policy_identifier});
+pragma Assertion_Policy(assertion_kind => policy_identifier
+ {, assertion_kind => policy_identifier});
-Pragma Assertion_Policy is allowed only immediately within a declarative_part,
-immediately within a package_specification, or as a configuration pragma.
+Pragma Assertion_Policy is allowed only immediately within a
+declarative_part, immediately within a package_specification, or as a
+configuration pragma.
+
+-----
+
+Replace 11.4.2, 9/2 and 9/2a by:
+
+The assertion_kind of a pragma Assertion_Policy shall be one of
+Assert, Static_Predicate, Dynamic_Predicate, Pre, Pre'Class, Post,
+Post'Class, Type_Invariant, Type_Invariant'Class, or some
+implementation defined aspect_mark. The policy_identifier shall be
+Ignore or Check or some implementation defined identifier.
-Legality Rules
-
-The assertion_kind shall be one of Assert, Static_Predicate, Dynamic_Predicate,
-Pre, Pre'Class, Post, Post’Class, Type_Invariant, Type_Invariant'Class, or some
-implementation defined aspect_mark. The policy_identifier shall be Ignore or
-Check or some implementation defined policy identifier.
-
[AARM:
Implementation defined: Implementation-defined policy_identifiers and
aspect_marks allowed in a pragma Assertion_Policy.]
+
+------
+Replace 11.4.2, 10/2 by:
-Static Semantics
+Pragma Assertion_Policy determines for each assertion kind named in
+the argument associations whether assertions of the given kind are to be
+enforced by a run-time check. The policy_identifier Check requires that
+assertion expressions of the given kind be checked that they evaluate
+to True at the points specified for the given kind; the policy_identifier
+Ignore requires that the assertion expression not be evaluated,
+and instead be treated as though it is simply the expression True.
+If no assertion_kinds are specified in the pragma, the specified policy
+applies to all assertion kinds.
+
+Pragma Assertion_Policy applies to the named assertion kinds in a
+specific region, and applies to all assertion expressions specified
+in that region. A Pragma
+Assertion_Policy given in a declarative_part or immediately within a
+package_specification applies from the place of the pragma to the end
+of the innermost enclosing declarative region. The region for a Pragma
+Assertion_Policy given as a configuration pragma is the declarative
+region for the entire compilation unit (or units) to which it applies.
+
+If a Pragma Assertion_Policy applies to a generic_instantiation, then
+the Pragma Assertion_Policy also applies to the entire instance.
+
+If multiple Assertion_Policy pragmas apply to a given construct for a given
+assertion kind, the assertion policy is determined by the one in the
+innermost enclosing declarative region specifying a policy for the
+assertion kind. If no such Assertion_Policy pragma exists, the policy
+is implementation defined.
-Pragma Assertion_Policy determines for each assertion kind named in the argument
-associations whether or not the assertion kind is to be enforced by a run-time
-check. The policy_identifier Check requires the run-time check; the
-policy_identifier Ignore suppresses the check. If no assertion_kinds are
-provided in the pragma, the specified policy applies to all assertion kinds.
-
-Pragma Assertion_Policy applies to the named assertion kinds in a specific
-region, and applies to all entities in that region. A Pragma Assertion_Policy
-given in a declarative_part or immediately within a package_specification
-applies from the place of the pragma to the end of the innermost enclosing
-declarative region. The region for a Pragma Assertion_Policy given as a
-configuration pragma is the declarative region for the entire compilation unit
-(or units) to which it applies.
-
-If a Pragma Assertion_Policy applies to a generic instantiation, then the Pragma
-Assertion_Policy also applies to the instance. If a Pragma Assertion_Policy
-applies to a call to a subprogram for which aspect Inline is True, then the
-Pragma Assertion_Policy also applies to the inlined subprogram body.
-
-If multiple Assertion_Policy pragmas apply to a construct and an assertion kind,
-the assertion policy is determined by the one in the smallest enclosing
-declarative region specifying a policy for the assertion kind. If no such
-Assertion_Policy pragma exists, the policy is implementation-defined. <<< I
-would love to make it Check!!! in analogy that checks are always enabled out of
-the box>>>
[AARM:
Implementation defined: The default assertion policy.]
+----------
-Dynamic Semantics
+Delete 11.4.2., 17/2.
-Whether or not an assertion expression is checked at run-time is determined as
-follows:
+----------
-For pragma Assert, the check is performed in accordance with the Assert policy
-in effect at the place of the pragma Assert.
+Change 11.4.2, 18/2 to:
-For subtype predicates, the check is performed in accordance with the
-Static_Predicate and Dynamic_Predicate policies in effect at the place of the
-predicate aspect specification.
-
-For type invariants, the check is performed in accordance with the
-Type_Invariant and Type_Invariant'Class policies in effect at the place of the
-invariant aspect specification.
-
-For preconditions, the check is performed in accordance with the Pre and
-Pre'Class policies in effect at the place of the explicit declaration of the
-subprogram.
-
-For postconditions, the check is performed in accordance with the Post and
-Post'Class policies in effect at the place of the explicit declaration of the
-subprogram.
-
-
-18/2
-An assertion policy specifies how a pragma Assert is interpreted by the
-implementation. If the assertion policy is Ignore at the point of a pragma
-Assert, the pragma is ignored. If the assertion policy is Check at the point of
-a pragma Assert, the elaboration of the pragma consists of evaluating the
-boolean expression, and if the result is False, evaluating the Message argument,
-if any, and raising the exception Assertions.Assertion_Error, with a message if
-the Message argument is provided.
+If required by the Assert assertion policy in effect at the place of
+the pragma Assert, the elaboration of the pragma consists of
+evaluating the boolean expression, and if the result is False,
+evaluating the Message argument, if any, and raising the exception
+Assertions.Assertion_Error, with a message if the Message argument is
+provided.
-11.5:
+----------
-25
-All_Checks
+<<< Note to Editor: 11.5 7.2/3, the inline part was deleted as part of
+these discussions.>>>
+shorten 11.5 7.2/3 to:
-Represents the union of all checks; suppressing All_Checks suppresses all
-checks. In addition, All_Checks suppresses all checks of assertion expressions.
+If a checking pragma applies to a generic instantiation, then the
+checking pragma also applies to the entire instance.
-Erroneous Execution
-26
-If a given check has been suppressed, and the corresponding error situation
-occurs, the execution of the program is erroneous.
+-------------
-!discussion
-For #1: The subtype declaration should be the determining
- point, as that is similar to that for preconditions. A predicate is a
- subtype property, so having it depend on some unrelated subprogram
- declaration seems bizarre. In addition, that would require
- having a different determination for predicate checks in other contexts
- (aggregate components, object initializations, etc.) Finally, using the
- subtype declaration should be enough, as a subprogram body always knows the
- location of the subtype declarations used in its parameters profiles.
+------------
-For #2: The proposal applies only to class-wide invariants, as the
- specific invariants only can be determined for the actually invoked
- subprogram (so there is no point in applying them at the call site rather
- than in the body). We could generalize this to cover all invariants, but the
- freedom doesn't seem necessary (and "unspecified" scares some users).
+modify 11.5 25 to:
+
+All_Checks
-For #3: There might be a better name for this checking mode. One proposal
- was "Check_Pres_Only" which is a trick as "Pre"s here means PREconditions
- and PREdicates. But that could be confused with the Pre aspect only, which
- is not what we want.
-
- It has been suggested that calls that are fully internal to a package
- ought to be exempted from this check. This seems to the author to have
- been a strawman set up to prove that since we can't get this separation
- perfect, we shouldn't do it at all. But that makes little sense; at
- worst, there will be extra checks that can't fail, and the user will always
- have the option of turning off all assertion checks if some are left on that
- are intolerable. The proposed rule is simple, and errs on the side of
- leaving checks on that might in fact be internal. It seems good enough
- (don't let best be the enemy of better)!
+Represents the union of all checks; suppressing All_Checks suppresses
+all checks. In addition, an implementation is allowed (but not
+required) to behave as if a pragma Assertion_Policy(Ignore) applies to
+any region to which pragma Suppress(All_Checks) applies.
+
+===========================================
+
+
+!discussion
-For #4: It could be argued that applying pragma Assertion_Policy(Check) as part
- of a library. There are four problems with this: first, a configuration
- pragma only applies to the units with which it actually appears (not
- necessarily children or subunits). That means it has to be repeated with
- every unit of a set. Secondly, since the default assertion policy is
- implementation-defined, there would be no clear difference between requiring
- assertions for correct operation and just wanting assertions checked (for
- testing purposes). Third, this requires checking for the entire library (as
- a configuration pragma cannot be applied to an individual subprogram, as
- Suppress and Unsuppress can). That might be too much of a requirement for
- some uses. Finally, as a configuration pragma, the pragma cannot be part of
- the library [package] (it has to appear outside). That makes it more likely
- that it get separated from the unit, and less likely that the requirement be
- noted by the reader. None of these are compelling by themselves, but as a
- set it seems to suggest something stronger is needed.
-
- Having a special assertion policy for this purpose (say "Always_Check")
- doesn't seem sufficient because it still has the previously noted issues
- caused by the pragma being a configuration pragma.
-
- In the absence of some mechanism to force these checks, paranoid
- programmers will simply refuse to use preconditions and predicates,
- simply because writing the checks as normal Ada code eliminates the
- possibility of some clueless client turning them off (and then asking for
- extensive and expensive support as to why their application failed).
- Since predicates and preconditions provide better and more formal
- documentation than comments can, it would be unfortunate to discourage
- their use by a segment of the programming population.
!ACATS Test
@@ -3756,5 +3653,45 @@
> So it's not so obvious.
It was obvious when I wrote it!
+
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, February 25, 2012 10:43 PM
+
+Here is a new version from Erhard and Tuck of an AI on pragma Assertion_Policy.
+[This is version /04 of the AI - Editor.]
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, February 25, 2012 11:08 PM
+
+Comments:
+
+(1) Shouldn't "assertion_kind" be "assertion_aspect_mark"? That is, why use words to
+repeat here what is specified in 2.8 and 13.1.1? (Still will need the list of them,
+of course.)
+
+(2) Then the wording would be about "assertion aspects" rather than "assertion kinds".
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Sunday, February 26, 2012 11:32 AM
+
+Two more places to fix (fairly easily):
+4.6. 51/3
+6.1.1. 19/3
+
+Apply the boilerplate...
+If requires by the <respective> assertion policies in effect at < > ,
+
+---------------
+
+(I checked for all occurrences of assertion policy in the RM and AARM)
+
+4.9. 34/3 is another, but it is ok as is.
****************************************************************
Questions? Ask the ACAA Technical Agent