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

Differences between 1.3 and version 1.4
Log of other versions for file ai05s/ai05-0274-1.txt

--- ai05s/ai05-0274-1.txt	2011/12/23 07:16:51	1.3
+++ ai05s/ai05-0274-1.txt	2012/01/05 06:19:33	1.4
@@ -1,6 +1,7 @@
-!standard  6.1.1(0)                              11-11-12    AI05-0274-1/03
+!standard  6.1.1(0)                              11-12-22    AI05-0274-1/04
 !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 6-1-2  11-11-12
@@ -17,31 +18,52 @@
 
 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.
+   invariants and all other assertions.
 
-3. A call on a function with side-effects within assertions that affect the
+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
+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.
+   side effects of the function.
 
 !problem
 
-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.)
+Calling a function that has some side effect from a precondition or
+postcondition can have some unusual effects.
 
-Should assertion-affecting side-effects be bounded errors in assertions?
-(Yes.)
+For instance, if F is a function that increments I, then in
+   F'Old + I'Old
+the value of I'Old might not be the value that it had when the subprogram was
+entered (if it was evaluated after the call to F).
+
+Similarly, if Glob is a global variable that is incremented by function SE,
+then in
+   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
+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.
+
+Finally, if the value of an assertion can be determined by some other means than
+evaluation, it still might be necessary to evaluate unneeded functions in case
+they have any side effects.
+
+All of these are potentially problems, and outside of the intention for
+assertions. We should adopt some way (a Bounded Error, perhaps) of discouraging
+users for writing and depending on side effects in assertions.
 
-Should unneeded function calls in assertions be evaluated regardless? (No).
+
+In addition, the wording in 11.4.2(1/2) says that Assertion_Policy applies
+(only) to Assert pragmas. That clearly is not the intent and should be fixed.
 
 !proposal
 
@@ -86,11 +108,8 @@
 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.
+if immediately reevaluated.
 
-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.
@@ -107,7 +126,7 @@
 any order yields identical results.
 
 ---------
-Add an implementation permission in 11.4.2
+Add after 11.4.2(25/2): [Implementation permissions]
 
 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
@@ -117,29 +136,33 @@
 !discussion
 
 1. Wording for the Assertion_Policy is updated to extend its effects to pre- and
-   postconditions and type invariants.
+   postconditions, type invariants, and predicates.
 
-This is a simple fix. The old words made the Pragma apply only the Assert
-pragmas, not to pre/postconditions or invariants.
+This is a simple fix. The old words made the Pragma apply only to the Assert
+pragma, not to pre/postconditions, invariants, or predicates.
 
 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.
+The reasons are obvious for type invariants and predicates. 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
+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
.
+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 queried by the
+'Old attribute).
+
+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
+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
+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.)
@@ -148,7 +171,7 @@
 
 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.
+   side effects of the function.
 
 We decided this at the Denver meeting.
 
@@ -162,7 +185,66 @@
 
 Force a conflict; the real text is found in the conflict file.
 
+!corrigendum 11.4.2(1/2)
+
+@drepl
+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. 
+@dby
+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), preconditions and postconditions
+(see 6.1.1), and type invariants (see 7.3.2) are collectively referred to as
+@i<assertions>; their boolean expressions are referred to as @i<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.
+
+!corrigendum 11.4.2(23/2)
+
+@dinsa
+The procedures Assertions.Assert have these effects independently of the assertion policy in effect.
+@dinss
+@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
+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
+Implementations may define their own assertion policies. 
+@dinst
+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. This permission applies even if the function has side
+effects.
+
+
 !ACATS Test
 
 ACATS tests could be constructed to see if the bounded error is detected, but these
@@ -616,7 +698,10 @@
 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
.
+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
@@ -633,3 +718,172 @@
 
 ****************************************************************
 
+From: Randy Brukardt
+Sent: Friday, December 23, 2011  2:45 AM
+
+Some comments on this AI (I'm fixing it up while finishing up the minutes from
+Denver):
+
+[The interesting question is the last one.]
+
+> !class binding interpretation
+
+This has to be an Amendment AI as it is directly modifying other Amendment AIs.
+There is no way it would apply to Ada 2005 code!
+
+> !question
+
+As an Amendment AI, we have a !problem rather than a !question.
+
+Moreover, all of these "questions" are too sparse to be able to determine the
+problem without reading the minutes (which I expect very few to actually do). So
+I've rewritten the entire section.
+
+> Should Assertion_Policy really only apply to Assert pragmas? (No.)
+
+Has to at least mention 11.4.2(1/2).
+
+> 'Old should be the value at the beginning of a subprogram, not
+> something else (non-deterministically) in the presence of
+> side-effects? (Yes.)
+
+This makes no sense to me, and especially the answer. There is nothing in the
+text of the AI that makes the 'Old be "the value at the beginning of the
+subprogram" in the presence of side-effects. What the AI says is that having
+side-effects that could affect the value of 'Old (among other things) is a
+bounded error, and it then mentions the possibility that 'Old has some other
+value if the bounded error happens. Nothing in that is going to make "Yes." to
+the above question; it *should* be the case, but we're not going to do anything
+at all to make it the case. So if someone actually makes this mistake, 'Old very
+might be "something else (non-deterministically).
+
+I replaced all of these questions by some of the examples from the meeting,
+which make it much clearer what the concerns are that led to these rules. And
+that's what's needed when people who were not at the meeting are trying to
+figure out what we did and why.
+
+Here's the replacement !proposal:
+
+Calling a function that has some side effect from a precondition or
+postcondition can have some unusual effects.
+
+For instance, if F is a function that increments I, then in
+   F'Old + I'Old
+the value of I'Old might not be the value that it had when the subprogram was
+entered (if it was evaluated after the call to F).
+
+Similarly, if Glob is a global variable that is incremented by function SE, then
+in
+   SE(X) and Glob mod 2 = 0
+the result may depend on the order of evaluation of the constituents.
+
+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.
+
+Finally, if the value of an assertion can be determined by some other means than
+evaluation, it still might be necessary to evaluate unneeded functions in case
+they have any side effects.
+
+All of these are potentially problems, and outside of the intention for
+assertions. We should adopt some way (a Bounded Error, perhaps) of discouraging
+users for writing and depending on side effects in assertions.
+
+In addition, the wording in 11.4.2(1/2) says that Assertion_Policy applies
+(only) to Assert pragmas. That clearly is not the intent and should be fixed.
+
+
+[End replacement !proposal] **********
+
+...
+> 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.
+
+I fear this wording is not specific enough to capture the intent (at least as I
+understand it).
+
+We intended that this apply to the group of preconditions and predicates that
+get evaluated for a call before the body starts executing, and similarly for the
+group of postconditions/invariants/predicates (for out parameters) that get
+evaluated at the end of a call during the return.
+
+But one could imagine (as I did during several re-readings of this text) that
+the assertions associated with a call are all of the assertions evaluated at any
+time during that call. Another possible reading is that it applies to all of
+call assertions (both inbound and outbound) that are associated with a
+particular entity.
+
+I don't think we intended either of those, because it is not hard to imagine
+side-effects that only affect much later assertions (such as a side-effect in a
+precondition that after the execution of the body, which then affects the value
+of a postcondition expression). And if we wanted those cases to be included, we
+could have used a much simpler rule:
+
+"It is a bounded error in an assertion expression to alter the value of any
+variable that could alter the value of any other assertion expression."
+
+But I'm pretty certain that we thought that this was going way too far. (Steve
+thought we went too far as it was.)
+
+I can see three solutions to this:
+
+(1) We really intended something close to the simpler wording I gave above. Then
+    we should simplify the wording. (But I don't think this was the intent.)
+
+(2) We could just add a large AARM note explaining what we meant, probably with
+    an example. This probably would be good enough for everyone other that
+    Robert, who apparently refuses to read the AARM. :-) I'm not sure how best
+    to write that note, however.
+
+(3) Or we could fix the wording to really say what we mean. I don't have a
+    proposal right now, it's too late tonight.
+
+Tell me how you think I should fix this (if at all).
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, December 23, 2011  3:24 AM
+
+...
+> (2) We could just add a large AARM note explaining what we meant, 
+> probably with an example. This probably would be good enough for 
+> everyone other that Robert, who apparently refuses to read the AARM. 
+> :-) I'm not sure how best to write that note, however.
+
+I stuck in the following AARM note:
+
+The rule above is intended to apply to all of the assertion expressions that are evaluated
+at the start of call (and similarly for the assertion expressions that are evaluated
+during the return from a call), but not other assertions actually given in the body, nor
+between the expressions given at the start and end. Specifically, a side effect in a
+function called from a precondition expression that changes the result of a postcondition
+expression of the same subprogram does not trigger this rule. 
+
+I hope that's enough. Tell me if you disagree.
+
+                Randy.
+
+P.S. Merry Christmas!!
+
+P.P.S. The call "SE(X)" in my rewritten proposal was a total accident, "X"
+was the parameter name in Steve's (illegal) example from the meeting, and I named the
+function SE as short for Side Effect. I didn't realize what it looked like until now.
+Very Merry Christmas!! ;-)
+
+****************************************************************

Questions? Ask the ACAA Technical Agent