CVS difference for ai05s/ai05-0274-1.txt
--- ai05s/ai05-0274-1.txt 2012/03/10 04:04:36 1.6
+++ ai05s/ai05-0274-1.txt 2012/03/10 04:55:43 1.7
@@ -1,9 +1,10 @@
-!standard 6.1.1(0) 12-02-24 AI05-0274-1/06
+!standard 6.1.1(0) 12-03-09 AI05-0274-1/07
!standard 11.4.2(1/2)
!standard 11.4.2(23/2)
!standard 11.4.2(25/2)
!class Amendment 11-11-11
!status Amendment 2012 11-11-12
+!status ARG Approved 8-1-1 12-02-25
!status work item 11-12-27
!status ARG Approved 6-1-2 11-11-12
!status work item 11-11-11
@@ -22,12 +23,13 @@
invariants and all other assertions.
3. A call on a function with side effects within assertions that affect the
- value of the assertion is a bounded error.
+ value of the assertion may be rejected by the implementation.
4. A call on a function with side effects within assertion expressions and
post-conditions that affect the value of any other assertion expressions
- evaluated for the same subprogram call is a bounded error. (This applies to
- subprogram predicates, type invariants, pre- or postcondition checks.)
+ evaluated for the same subprogram call also may be rejected by the implementation.
+ (This applies to subprogram predicates, type invariants, pre- or postcondition
+ checks.)
5. An implementation permission is added that allows omissions of function calls
that do not contribute to the value of an assertion, regardless of
@@ -49,7 +51,7 @@
SE(Param) and Glob mod 2 = 0
the result may depend on the order of evaluation of the consistuents.
-If there are multiple assertion expreissions that apply at the start (or finish) of
+If there are multiple assertion expressions that apply at the start (or finish) of
a call (which can happen because of inheritance as well as the use of different
kinds of assertions), these affects can occur in one assertion expression because
of a function call in another expression.
@@ -115,16 +117,26 @@
even if the function has side effects.]
An implementation need not allow the specification of an assertion
-expression if the evaluation of the expression has a side-effect such
+expression if the evaluation of the expression has a side effect such
that an immediate reevaluation of the expression could produce a
-different value. Similarly, an implementation need not allow the
-specification of an assertion expession that is associated with a call
-of (or return from) a callable entity C, if the evaluation of the
-expression has a side-effect such that the evaluation of some other
+different value. Similarly, an implementation need not allow the
+specification of an assertion expression that is checked as part of a
+call or on return from a callable entity C, if the evaluation of the
+expression has a side effect such that the evaluation of some other
assertion expression associated with the same call of (or return from) C
could produce a different value than it would if the first expression
had not been evaluated.
+AARM Ramification: This allows an implementation to reject such assertions.
+To maximize portability, assertions should not include expressions that contain
+these sorts of side effects.
+
+----------
+
+As a side effect of this discussion, we've removed hyphens from "side-effect"
+where that appeared in the Standard and AARM (in 1.1.5, 4.4, 7.4, 9.5.3, 10.2.1,
+11.4.2, 12.3, C.6, C.7.2, and H.4 - most of these are AARM notes). These changes
+were not marked (following the same thnking as applied in AI05-0293-1).
!discussion
@@ -147,15 +159,13 @@
We decided this for pre- and postconditions early at the Denver meeting. It
should be true for invariants, predicates, and general assertions as well. Note
that the rules do not preclude anything that isn't outright dangerous.
-Memo-functions are legitimate.
-
- (as long as the memo-state is not itself queried by the
-assertion expression).
+Memo-functions are legitimate (as long as the memo-state is not itself queried
+by the assertion expression).
-At the Houston meeting, we decided any restriction on side-effects
+At the Houston meeting, we decided any restriction on side effects
should be compile-time restrictions, rather than bounded errors. It was
felt that raising Program_Error at run time due to an inappropriate
-side-effect could make programs less safe.
+side effect could make programs less safe.
Technically, this is inconsistent with the behaviour of Pragma Assert in Ada 2005,
in that assertions with side effects that affect the outcome of the assertion are
@@ -214,28 +224,12 @@
@s8<@i<Bounded (Run-Time) Errors>>
It is a bounded error to invoke a potentially blocking operation (see
-9.5.1) during the evaluation of an assertion expression. If the bounded error is
+9.5.1) during the evaluation of an assertion expression associated with
+a call on, or return from, a protected operation. If the bounded error is
detected, Program_Error is raised. If not detected, execution proceeds normally,
but if it is invoked within a protected action, it might result in deadlock or a
(nested) protected action.
-It is a bounded error in an assertion expression to alter the value of any
-variable that could alter the value of the assertion expression. If the bounded
-error is detected, Program_Error is raised. Otherwise, execution proceeds
-normally with the affected assertion, but the assertion expression need not hold
-if immediately reevaluated.
-
-It is a bounded error in an assertion expression associated with a call of or
-return from a callable entity @i<C> to alter the value of any variable that could
-alter the value of any other such assertion expression of the callable entry @i<C>.
-If the bounded error is detected, Program_Error is raised. Otherwise, execution
-proceeds normally with the affected assertion expressions. Possible
-consequences of not detecting the bounded error are that the value denoted by
-@i<X>'Old for any @fa<prefix> @i<X> might no longer denote the value denoted by @i<X>
-at the beginning of the subprogram call with the affected postcondition, or that a
-condition that evaluated to true is no longer true after evaluation of the
-affected precondition or postcondition.
-
!corrigendum 11.4.2(25/2)
@dinsa
@@ -245,6 +239,17 @@
value of the assertion expression, an implementation is permitted to omit the
function call. This permission applies even if the function has side
effects.
+
+An implementation need not allow the specification of an assertion
+expression if the evaluation of the expression has a side effect such
+that an immediate reevaluation of the expression could produce a
+different value. Similarly, an implementation need not allow the
+specification of an assertion expression that is checked as part of a
+call or on return from a callable entity @i<C>, if the evaluation of the
+expression has a side effect such that the evaluation of some other
+assertion expression associated with the same call of (or return from) @i<C>
+could produce a different value than it would if the first expression
+had not been evaluated.
!ACATS Test
Questions? Ask the ACAA Technical Agent