!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 !status work item 11-11-11 !status received 11-11-11 !priority Medium !difficulty Medium !subject Side-effects during assertion evaluation !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. 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. !problem 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(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. 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 (See summary.) !wording Replace 11.4.2(1/2): 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 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) (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 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 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 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 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, type invariants, and predicates. 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 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 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, 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 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 side effects of the function. We decided this at the Denver meeting. !example (See problem.) !corrigendum 6.1.1(0) @dinsc 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; their boolean expressions are referred to as @i. 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> 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 to alter the value of any variable that could alter the value of any other such assertion expression of the callable entry @i. 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'Old for any @fa @i might no longer denote the value denoted by @i 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 would have minimal value. !ASIS No ASIS effect. !appendix From: Erhard Ploedereder Sent: Friday, November 11, 2011 5:49 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*. 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. A better text for *...* would be *whose lifetime exceeds the duration of the subprogram call", but I am not sure that the terminology is set up. ------------------ and in case this fails, and Steve deletes the first sentence of the definition of 'Old, add a Note If subprograms with side-effects are called inside pre- or postconditions, the expectation that X'Old denotes the value of X at the beginning of the subprogram is no longer justified. and if Steve does not delete the first sentence: If subprograms with side-effects are called inside pre- or postconditions, the guarantee that X'Old denotes the value of X at the beginning of the subprogram 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. **************************************************************** 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 side-effects of the function. We decided this at the Denver meeting. **************************************************************** 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!! ;-) ****************************************************************