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

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

--- ai05s/ai05-0274-1.txt	2012/02/14 03:34:35	1.5
+++ ai05s/ai05-0274-1.txt	2012/03/10 04:04:36	1.6
@@ -1,4 +1,4 @@
-!standard  6.1.1(0)                              12-02-13    AI05-0274-1/05
+!standard  6.1.1(0)                              12-02-24    AI05-0274-1/06
 !standard 11.4.2(1/2)
 !standard 11.4.2(23/2)
 !standard 11.4.2(25/2)
@@ -100,62 +100,32 @@
 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.
-
-[** Editor's note: There is some agreement that the above is too vague. After
-discussion with Tucker, the best I was able to come up with was:
-
-    It is a bounded error if within an assertion expression (directly or
-    indirectly) there is a function call F that alters the value of a variable
-    that is read (directly or indirectly) in some construct C that is part
-    of the assertion expression but is not part of F.
-
-But this is slightly too strong; it probably disallows a shared global logging
-facility if used in multiple function calls used in the same assertion
-expression. Also, the "that is read" is a bit clunky; but J-P objected
-[correctly] to talking about the name of the variable.
-
-Note that too strong of a rule probably is irrelevant to Ada implementations
-(which are unlikely to enforce this), but might matter to tools trying to
-prove the absence of exceptions (which means proving the absence of bounded
-errors).
-
-We should try to polish this some more, and probably consider if the next
-paragraph needs improvement as well. **]
-
-
-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.
+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; it might result in deadlock or a (nested) protected
+action.
 
 ---------
 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.]
+If the result of a function call in an assertion expression is not
+needed to determine the value of the expression, an implementation is
+permitted to omit the function call. Redundant:[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 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
+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.
 
+
 !discussion
 
 1. Wording for the Assertion_Policy is updated to extend its effects to pre- and
@@ -172,25 +142,34 @@
 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.
+   value of the assertion can be disallowed by the implementation.
 
 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).
+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
+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.
+
 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.
+now at risk of being rejected at compile time. 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.)
+   subprogram call can be disallowed by the implementation.  (This applies to 
+   subprogram predicates, type invariants, pre- or postcondition checks.)
 
-We decided this at the Denver meeting after intensive discussions.
+We decided to restrict such calls at the Denver meeting after intensive discussions.
+At the Houston meeting we decided to make these compile-time errors, rather
+than bounded run-time errors.  This was felt to be safer.
 
 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