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

--- ai05s/ai05-0274-1.txt	2011/12/23 06:26:03	1.1
+++ ai05s/ai05-0274-1.txt	2011/12/23 07:06:43	1.2
@@ -1,42 +1,155 @@
-!standard  6.1.1(0)                              11-11-11    AI05-0274-1/01
+!standard  6.1.1(0)                              11-11-12    AI05-0274-1/02
+!standard 11.4.2(1/2)
+!standard 11.4.2(23/2)
 !class Amendment 11-11-11
 !status work item 11-11-11
 !status received 11-11-11
-!priority Low
+!priority Medium
 !difficulty Medium
 !subject Side-effects during assertion evaluation
 
 !summary
 
-Define side-effects in a pre/postcondition to be a bounded error.
+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. Calls on functions with side-effects within assertions that affect the value
+   of the assertion of the same subprogram are 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.
+
+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.
+
 !problem
+
+Should Assertion_Policy really only apply to Assert pragmas? (No.)
 
-Calling a function that has some side effect from a precondition or
-postcondition can have some unusual effects.
+'Old should be the value at the beginning of a subprogram, not something else
+(non-deterministically) in the presence of side-effects? (Yes.)
 
-For instance, if F is a function that increments I, then in
-   F'Old + I'Old
-the value of I might not be the value that it had when the subprogram was
-entered.
+Should assertion-affecting side-effects be allowed in assertions? (No.)
 
+Should unneeded function calls in assertions be evaluated regardless? (No).
+
 !proposal
 
 (See summary.)
 
 !wording
 
-Add before 6.1.1(36/3):
+Replace 11.4.2(1/2):
 
-It is a bounded error in a pre- or postcondition to invoke a subprogram that
-alters the value of any variable that is not locally declared in the
-subprogram. If the bounded error is detected, Program_Error is raised. If not
-detected, execution proceeds normally, but values denoted by X'Old for any
-prefix X may no longer denote the value denoted by X at the beginning of the
-subprogram with the affected pre- or postcondition.
+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.
+
+with:
+
+Pragma Assert is used to assert the truth of a Boolean expression at any 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.
+
+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) (moved below)
+  2. Insert the following after 11.4.2(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 affects 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.
+
+---------
+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.
 
+
 !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. 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.
+
+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 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.
+
 !example
 
 (See problem.)
@@ -88,3 +201,274 @@
 is voided.
 
 ****************************************************************
+
+From: Robert Dewar
+Sent: Friday, November 11, 2011  6:37 PM
+
+> It is a bounded error in a pre- or postcondition to invoke a
+> subprogram that alters the value of any variable *that is not locally
+> declared in the subprogram*. If the bounded error is detected,
+> Program_Error is raised. If not detected, execution proceeds normally,
+> but values denoted by X'Old for any prefix X may no longer denote the
+> value denoted by X at the beginning of the subprogram with the affected pre-
+> or postcondition.
+
+I don't like this being a bounded error, it forbids the use of memo functions in
+pre and post conditions and that seems silly. Let's not go out of our way to
+save people from themselves at the expense of hampering others!
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Friday, November 11, 2011  6:55 PM
+
+In 6.1.1 insert before 36/3:
+
+It is a bounded error in a precondition to invoke a subprogram that alters the
+value of any variable *that is not locally declared in the subprogram* so that
+the value of the postcondition expression is affected. If the bounded error is
+detected, Program_Error is raised. If the bounded error is not detected, 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.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Friday, November 11, 2011  7:12 PM
+
+In 6.1.1 insert before 36/3:
+
+It is a bounded error in a pre- or postcondition to invoke a subprogram that
+alters the value of any variable *that is not locally declared in the
+subprogram* so that the value of the postcondition expression is affected by the
+altered variable. If the bounded error is detected, Program_Error is raised. If
+the bounded error is not detected, 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.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Friday, November 11, 2011  7:32 PM
+
+In 6.1.1 insert before 36/3:
+
+It is a bounded error in a pre- or postcondition of subprogram S to invoke a
+subprogram that alters the value of any variable *that is not locally declared
+in the subprogram* and whose value affects the value of any pre- or
+postcondition expression of subprogram S. If the bounded error is detected,
+Program_Error is raised. Otherwise, execution proceeds normally with the
+affected pre- or postcondition expressions.
+
+One possible consequence of the bounded error is 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.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, November 11, 2011  7:43 PM
+
+If the value of an Old attribute_reference is not needed, then the
+implementation is permitted to omit the declaration of the corresponding
+implicitly-declared constant.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, November 11, 2011  7:48 PM
+
+Ah, the old "is not needed" phrase, what exactly does that mean in this case,
+for instance if some clever prover can prove that the postcondition is always
+true, then you don't need the declaration right?
+
+hmmmm ....
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, November 11, 2011  7:50 PM
+
+As was noted in discussion here in Denver, it means the same thing that it has
+meant for years in 10.2.1(18).
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Saturday, November 12, 2011  6:37 AM
+
+Small improvement, to my taste (because that's the one that really convinced
+me):
+
+Possible consequences of the bounded error include that a precondition that
+evaluates to True might not be True anymore at the beginning of S, and 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.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Saturday, November 12, 2011 12:04 PM
+
+Sorry, fixed a few typos. Randy, thisis the version on the stick..
+
+[Editor's note: This is, with a few corrections, version /02 of the AI. The
+previous version, which was the same except with a few additional typos,
+was discarded.]
+
+------
+!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. Calls on functions with side-effects within assertions that affect the value
+   of the assertion of the same subprogram are 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.
+
+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 allowed in assertions? (No.)
+
+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 any 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.
+
+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 affects 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.
+
+---------
+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.
+
+
+!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. 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.
+
+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 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.
+
+****************************************************************
+