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

Differences between 1.3 and version 1.4
Log of other versions for file 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