Version 1.4 of ai05s/ai05-0274-1.txt

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!! ;-)

****************************************************************