CVS difference for ai05s/ai05-0274-1.txt
--- ai05s/ai05-0274-1.txt 2011/12/23 07:06:43 1.2
+++ ai05s/ai05-0274-1.txt 2011/12/23 07:16:51 1.3
@@ -1,7 +1,9 @@
-!standard 6.1.1(0) 11-11-12 AI05-0274-1/02
+!standard 6.1.1(0) 11-11-12 AI05-0274-1/03
!standard 11.4.2(1/2)
!standard 11.4.2(23/2)
!class Amendment 11-11-11
+!status Amendment 2012 11-11-12
+!status ARG Approved 6-1-2 11-11-12
!status work item 11-11-11
!status received 11-11-11
!priority Medium
@@ -17,12 +19,13 @@
to the section on assertion policy, since they should apply to type
invariants and all other assertions as well.
-3. Calls on functions with side-effects within assertions that affect the value
- of the assertion of the same subprogram are a bounded error.
+3. A call on a function with side-effects within assertions that affect the
+ value of the assertion is a bounded error.
-4. Calls on functions with side-effects within pre- and post-conditions that
- affect the value of any other pre- or postcondition of the same subprogram
- are a bounded error.
+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.)
5. An implementation permission is added that allows omissions of function calls
that do not contribute to the value of an assertion, regardless of
@@ -35,7 +38,8 @@
'Old should be the value at the beginning of a subprogram, not something else
(non-deterministically) in the presence of side-effects? (Yes.)
-Should assertion-affecting side-effects be allowed in assertions? (No.)
+Should assertion-affecting side-effects be bounded errors in assertions?
+(Yes.)
Should unneeded function calls in assertions be evaluated regardless? (No).
@@ -54,15 +58,15 @@
with:
-Pragma Assert is used to assert the truth of a Boolean expression at any point
+Pragma Assert is used to assert the truth of a boolean expression at a point
within a sequence of declarations or statements.
-Assert pragmas, pre- and postconditions (see 6.1.1), and type invariants (see
-7.3.2) are collectively referred to as assertions; their boolean expressions are
-referred to as assertion expressions.
+Assert pragmas, subtype predicates (see 3.2.4), pre- and postconditions (see
+6.1.1), and type invariants (see 7.3.2) are collectively referred to as
+assertions; their boolean expressions are referred to as assertion expressions.
Pragma Assertion_Policy is used to control whether assertions are to be ignored
-by the implementation, checked at run-time, or handled in some
+by the implementation, checked at run time, or handled in some
implementation-defined manner.
-------------
@@ -72,49 +76,44 @@
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
+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
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 affects the value of the assertion expression. If the bounded
+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
after the assertion.
-It is a bounded error in a pre- or postcondition of subprogram P to alter the
-value of any variable that affects the value of any pre- or postcondition
-expression of subprogram P. If the bounded error is detected, Program_Error is
-raised. Otherwise, execution proceeds normally with the affected pre- or
-postcondition expressions. Possible consequence of the bounded error are that
-the values denoted by X'Old for any prefix X might no longer denote the value
-denoted by 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 pre- or postcondition.
+AARM Note: The intended effect is that an immediate reevalation of the affected
+assertion expression yields the same result.
+
+It is a bounded error in an assertion expression associated with a call of or
+return from a callable entity C to alter the value of any variable that could
+alter the value of any other such assertion expression of the callable entry C.
+If the bounded error is detected, Program_Error is raised. Otherwise, execution
+proceeds normally with the affected assertion expressions. Redundant:[Possible
+consequences of not detecting the bounded error are that the value denoted by
+X'Old for any prefix X might no longer denote the value denoted by 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 pre- or postcondition.]
+
+AARM Note: The intended effect is that an evaluation of the involved assertion
+expressions (subtype predicates, type invariants, pre- and postconditions) in
+any order yields identical results.
---------
Add an implementation permission in 11.4.2
If the result of a function call in an assertion is not needed to determine the
-value of the assertion expression, the function call need not be executed. This
-permission applies even if the function not only returns a value but has
-additional effects.
-
-<<< The following is for discussion >>>
-
-In addition, the implementation may omit a call on such a subprogram and simply
-reuse the results produced by an earlier call on the same subprogram, provided
-that none of the parameters nor any object accessible via access values from
-the parameters have any part that is of a type whose full type is an immutably
-limited type, and the addresses and values of all by-reference actual
-parameters, the values of all by-copy-in actual parameters, and the values of
-all objects accessible via access values from the parameters, are the same as
-they were at the earlier call. This permission applies even if the subprogram
-produces other side effects when called.
+value of the assertion expression, an implementation is permitted to omit the
+function call. Redundant:[This permission applies even if the function has side
+effects.]
-
!discussion
1. Wording for the Assertion_Policy is updated to extend its effects to pre- and
@@ -130,19 +129,22 @@
The reasons are obvious for type invariants. Might as well fix it for
assertions, too, where the same issue applies.
-3. Calling on functions with side-effects within assertions that affect the
- value of the assertion of the same subprogram are a bounded error.
-
-We decided this for pre- and postconditions at the Denver meeting. It should be
-true for invariants 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 queried by the 'Old attribute.
+3. A call on a function with side-effects within assertions that affect the
+ value of the assertion is a bounded error.
-4. Calling on functions with side-effects within pre- and post-conditions that
- affect the value of any other pre- or postcondition of the same subprogram
- are a bounded error.
+We decided this for pre- and postconditions early at the Denver meeting. It
+should be true for invariants 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 queried by the 'Old attribute).
+
+Technically, this is inconsistent with the behaviour of Pragma Assert in Ada2005, in that assertions with side effects that affect the outcome of the assertion are now at risk to get Program_Error. However, this is considered a really good thing to happen
.
+
+4. A call on a function with side-effects within assertion expressions 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.)
-We decided this at the Denver meeting.
+We decided this at the Denver meeting after intensive discussions.
5. An implementation permission is added that allows omissions of function calls
that do not contribute to the value of an assertion, regardless of
@@ -168,6 +170,7 @@
!ASIS
+No ASIS effect.
!appendix
@@ -463,6 +466,164 @@
are a bounded error.
We decided this at the Denver meeting.
+
+5. An implementation permission is added that allows omissions of function calls
+ that do not contribute to the value of an assertion, regardless of
+ side-effects of the function.
+
+We decided this at the Denver meeting.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Saturday, November 12, 2011 2:15 PM
+
+[Editor's note: This is, with a few corrections, version /03 of the AI.]
+
+!standard 6.1.1
+!standard 11.4.2
+!standard 7.3.2
+!class binding interpretation
+!status received
+!priority Medium
+!difficulty Easy
+!qualifier Omission
+!subject Fixes to assertion evaluation semantics
+
+!summary
+
+1. Wording for the Assertion_Policy is updated to extend its effects to pre- and
+ postconditions and type invariants.
+
+2. The bounded error situations that apply to pre- and postconditions are moved
+ to the section on assertion policy, since they should apply to type
+ invariants and all other assertions as well.
+
+3. A call on a function with side-effects within assertions that affect the
+ value of the assertion is a bounded error.
+
+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.)
+
+5. An implementation permission is added that allows omissions of function calls
+ that do not contribute to the value of an assertion, regardless of
+ side-effects of the function.
+
+!question
+
+Should Assertion_Policy really only apply to Assert pragmas? (No.)
+
+'Old should be the value at the beginning of a subprogram, not something else
+(non-deterministically) in the presence of side-effects? (Yes.)
+
+Should assertion-affecting side-effects be bounded errors in assertions?
+(Yes.)
+
+Should unneeded function calls in assertions be evaluated regardless? (No).
+
+!recommendation
+
+(See summary and wording.)
+
+!wording
+
+Change 11.4.2 1/2 (old version:)
+"Pragma Assert is used to assert the truth of a Boolean expression at any point
+within a sequence of declarations or statements. Pragma Assertion_Policy is used
+to control whether such assertions are to be ignored by the implementation,
+checked at run-time, or handled in some implementation-defined manner."
+
+to read:
+
+Pragma Assert is used to assert the truth of a boolean expression at a point
+within a sequence of declarations or statements.
+
+Assert pragmas, subtype predicates (see 3.2.4), pre- and postconditions (see
+6.1.1), and type invariants (see 7.3.2) are collectively referred to as
+assertions; their boolean expressions are referred to as assertion expressions.
+
+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.
+
+-------------
+
+ 1. Delete 6.1.1. 36/3. (replicated below)
+ 2. Insert the following in 11.4.3 after 23/2.
+
+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
+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
+after the assertion.
+
+AARM Note: The intended effect is that an immediate reevalation of the affected
+assertion expression yields the same result.
+
+It is a bounded error in an assertion expression associated with a call of or
+return from a callable entity C to alter the value of any variable that could
+alter the value of any other such assertion expression of the callable entry C.
+If the bounded error is detected, Program_Error is raised. Otherwise, execution
+proceeds normally with the affected assertion expressions. Redundant:[Possible
+consequences of not detecting the bounded error are that the value denoted by
+X'Old for any prefix X might no longer denote the value denoted by 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 pre- or postcondition.]
+
+AARM Note: The intended effect is that an evaluation of the involved assertion
+expressions (subtype predicates, type invariants, pre- and postconditions) in
+any order yields identical results.
+
+---------
+Add an implementation permission in 11.4.2
+
+If the result of a function call in an assertion is not needed to determine the
+value of the assertion expression, an implementation is permitted to omit the
+function call. Redundant:[This permission applies even if the function has side
+effects.]
+
+!discussion
+
+1. Wording for the Assertion_Policy is updated to extend its effects to pre- and
+ postconditions and type invariants.
+
+This is a simple fix. The old words made the Pragma apply only the Assert
+pragmas, not to pre/postconditions or invariants.
+
+2. The bounded error situations that apply to pre- and postconditions are moved
+ to the section on assertion policy, since they should apply to type
+ invariants and all other assertions as well.
+
+The reasons are obvious for type invariants. Might as well fix it for
+assertions, too, where the same issue applies.
+
+3. A call on a function with side-effects within assertions that affect the
+ value of the assertion is a bounded error.
+
+We decided this for pre- and postconditions early at the Denver meeting. It
+should be true for invariants 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 queried by the 'Old attribute).
+
+Technically, this is inconsistent with the behaviour of Pragma Assert in Ada2005, in that assertions with side effects that affect the outcome of the assertion are now at risk to get Program_Error. However, this is considered a really good thing to happen
.
+
+4. A call on a function with side-effects within assertion expressions 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.)
+
+We decided this at the Denver meeting after intensive discussions.
5. An implementation permission is added that allows omissions of function calls
that do not contribute to the value of an assertion, regardless of
Questions? Ask the ACAA Technical Agent