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

--- ai05s/ai05-0290-1.txt	2012/02/19 03:34:30	1.2
+++ ai05s/ai05-0290-1.txt	2012/03/17 03:38:53	1.3
@@ -1,4 +1,4 @@
-!standard  3.2.4(0)                               12-02-18    AI05-0290-1/02
+!standard  3.2.4(0)                               12-02-25    AI05-0290-1/03
 !standard  7.3.2(0)
 !class Amendment 12-02-14
 !status Amendment 2012 12-02-14
@@ -109,16 +109,6 @@
     body and are immune to optimization. That's why the original proposal
     is preferred (the cost doesn't change when checks are turned off).
 
-Proposal #5: There is an optional "exception" clause on predicates and
-    preconditions. This specifies the exception that will be raised on the
-    failure of the check.
-
-Reason: We want to encourage the conversion of comments to
-    predicates/preconditions in existing libraries. However, changing the
-    exception raised may be an unacceptable incompatibility. By allowing
-    the exception to be raised to be specified, the specification can remain
-    unchanged while additional information is given to tools.
-
 =====================
 
 Since this AI was created, a number of additional issues/proposals have been
@@ -162,6 +152,117 @@
     more likely that everyone will use them. Best to have a definition. This
     will simplify the wording for #2.
 
+
+
+Proposal from Erhard during ARG Meeting #46. [Other parts of AI need updating.]
+This replaces parts of 11.4.2.
+
+
+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.
+
+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 is allowed only immediately within a declarative_part,
+immediately within a package_specification, or as a configuration pragma.
+
+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.]
+
+
+Static Semantics
+
+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
+
+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.
+
+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.
+
+11.5:
+
+25
+All_Checks
+
+Represents the union of all checks; suppressing All_Checks suppresses all
+checks. In addition, All_Checks suppresses all checks of assertion expressions.
+
+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
@@ -222,33 +323,6 @@
     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.
-
-For #5:
-Example: Imagine the following routine in GUI library:
-
-    procedure Show_Window (Window : in out Root_Window);
-       -- Shows the window.
-       -- Raises Not_Valid_Error if Window is not valid.
-
-We would like to be able to use a predicate to check the comment. With the
-"exception" clause we can do this without changing the semantics:
-
-    subtype Valid_Root_Window is Root_Window
-       with Dynamic_Predicate =>
-           Is_Valid (Valid_Root_Window) exception Not_Valid_Error;
-
-    procedure Show_Window (Window : in out Valid_Root_Window);
-       -- Shows the window.
-
-If we didn't have the "exception" clause here, using the predicate would
-change the exception raised on this failure. That could cause the exception
-to fall into a different handler than currently, which is likely to not be
-acceptable.
-
-Similarly, the various Containers packages in Ada could use predicates in
-this way to make some of the needed checks; but that can only be done if the
-semantics remains unchanged (raising Program_Error and Constraint_Error,
-not Assertion_Error).
 
 !ACATS Test