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

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

From: Randy Brukardt
Sent: Tuesday, December 27, 2011  8:18 PM

Another thought on the "bounded error" AI:

Steve voted against this AI, because "because he thinks this notion of 'affects'
is too imprecise" (as recorded in the minutes). That's a weird statement,
because the final wording doesn't include the word "affects" at all -- the final
wording is "could alter". Still, let's ignore that and look at his actual
concern (which I admit I didn't do during the meeting; my excuse was that I was
too busy taking notes [at least that sounds plausible :-)]).

Our intent with this rule is that compilers would not try to enforce it (that
is, try to detect the error). However, it certainly is true that a complier
*could* try to enforce it. Moreover, other tools (such as a SPARK-like prover)
surely need to know whether this rule is violated (they are unlikely to allow
bounded errors to persist in programs that they check). So it should be possible
to determine, with knowledge of the entire program, whether or not the rule is
violated.

I was thinking about adding an AARM TBH note to clarify. But then I realized I
don't really know what the rule is. Specifically, Steve gave an example that is
questionable. But I don't think we ever clearly decided whether or not his
example was a bounded error (that is, does it trigger the new rule). That's not
going to work.

Steve gave the following example:

   Incb(X) and X > 0

where Incb increments its parameter. In this case, the side-effect only "could
alter" the result of the expression if the value of X = 0. So is the rule
triggered or not?

The problem with this example is that it is illegal by 6.4.1(6.18/3); the
parameter to Incb has to be "in out" if X is to be modified (since an integer is
a by-copy type), and that triggers the "Taft" order-of-evaluation checks. Since
the arguments to "and" can be evaluated in either order, the expression is
illegal on its face (and the reason is in large part the fact that the
side-effect "could alter" the result -- what a tangled web we weave!). So there
is no point in talking about it.

But it is easy enough to write a similar example that is legal; just make the
entity global and hidden. So let's write a more complete example:

    Glob : Natural := 0;

    function Incb (P : in Natural) return Boolean is
    begin
        Glob := Glob + P;
        return P > 0;
    end Incb;

    procedure Bar (Param : in out Natural)
        with Pre => Incb(Param) and Glob > 0;

In this case, the expression value will only be altered if Glob = 0 and Param /=
0 when Bar is called AND the function is called after evaluating "Glob > 0" (the
language allows evaluating these operands in either order).

Now, the rule in question is:

"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."

Does this expression qualify? There seem to be at least four possible answers:

(1) This expression does qualify. The only requirement is that there exist some
set of values where the value would be altered. This seems to be the intent
expressed by wording ("can alter"). However, taken literally, it could only
apply to an expression that has parts that can be evaluated in an arbitrary
order. That's because the value of the expression cannot change (even in the
face of a side-effect) if the order is specified. For instance, if we change
"and" to "and then" in the above expression, the value is always going to be the
same.

(2) This expression qualifies IFF Glob = 0 and Param /= 0. That is, the bounded
error only occurs when the values actually cause the value to be altered. In
this case, the normative wording should say "alters" rather than "can alter".
This would be a rule that would be simple to verify if it applies, but it also
would be extremely narrow (and also subject to the "and then" issue).

Neither of these seems to be what was really intended. I've been ignoring the
last sentence in this rule because it does nothing but describe the normal
execution and a possible consequence. That consequence talks about the
expression being immediately reevaluated; but note that that consequence can
happen even for expressions that do not trigger either reading of the rule (that
is, expressions using "and then" rather than "and").

The problem with the rule as written is that it only talks about the altering
the value of {the current evaluation of} the assertion expression. If we want to
include some imaginary other evaluation of the expression, we had better say
that explicitly. Indeed, Tucker had suggested that something about "immediate
reevaluation" be part of the normative wording, that didn't happen for some
reason. Imagining that it is part of the normative wording gives us two more
answers:

(3) This expression does qualify, and would even if "and" is replaced by "and
then". The only requirement is that there exist some set of values where the
value of a subsequent immediate evaluation would be altered. The normative
wording should be what Tucker suggested during the meeting: "...that could alter
the value of the expression on a immediate subsequent evaluation". Or perhaps:
"...that could alter the value of the assertion expression, immediately or on a
immediate subsequent evaluation". (I can imagine an expression where the value
changes because of a side-effect, but an immediate re-evaluation would get the
original answer - likely because the result type of Boolean has only two
possible answers. Surely that should be covered.) This is a broad rule, covering
the majority of possible side-effects (only the most benign would be allowed; a
straight memo function surely would not be a bounded error, nor would saving
values for logging, but I find it hard to imagine what else would not).

(4) Same as above, but using "alters" rather than "can alter". That is, the
bounded error only occurs if the value is in fact affected (directly or on an
immediate subsequent evaluation). "and" or "and then" usually would not make a
difference. This is a narrower rule, and it would make almost no sense for a
compiler to try to detect it (which I thought was a goal) - it would have to do
so at runtime (or is that run-time or run time ;-).

I'm pretty sure we meant either (3) or (4), but it is not clear to me which is
intended (nor do my meeting notes clarify anything). Note that either (3) or (4)
requires changing the approved wording -- I agree with Steve that the current
wording is too vague. And I don't think it reflects our intent (neither (1) nor
(2) being our intent -- but I can't get that out of reading the rule).

Beyond that, it's not clear whether we need a wording change for the second rule
(the one about the multiple assertion expressions evaluated on entry or exit
from a subprogram). It suffers from a similar problem, but there it is less
likely that there would be a difference from an "immediate reevaluation", and
far more likely that there would be a change in some other expression, so maybe
fixing the first one is sufficient.

Thoughts??

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

From: Tucker Taft
Sent: Tuesday, December 27, 2011  9:07 PM

Perhaps we should make the wording as similar as possible to the new rules
restricting side-effect due to function [IN] OUT parameters, but make it fully
general, rather than limiting it to statically recognizable situations.

Our statically checkable rule is:

If a construct C has two or more direct constituents that are names or
expressions whose evaluation may occur in an arbitrary order, at least one of
which contains a function call with an in out or out parameter, then the
construct is legal only if:

   For each name N that is passed as a parameter of mode in out or out to some inner
   function call C2 (not including the construct C itself), there is no other name anywhere
   within a direct constituent of the construct C other than the one containing C2, that is
   known to refer to the same object.

-----

We could perhaps use this as a model, but use a much simpler,
but non-statically-checkable rule.   E.g.:

    It is a bounded error if within an assertion expression (directly
    or indirectly) there is a construct that updates an object whose
    value possibly contributes to the value of the expression (directly or
    indirectly).

I'll admit it isn't very precise, but perhaps it is adequate.

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

From: Randy Brukardt
Sent: Tuesday, December 27, 2011  9:24 PM

Isn't this too strong? It seems to ban memo functions because the memo value
"possibly contributes to the value of the expression" (if it is used rather than
recalculating the function value), and it is "updated" by the call to the memo
function. The wording here doesn't say anything about the value that possibly
contributes being different in some sense, and that seems necessary to allow
memo functions (which clearly have a side-effect, but that effect does not
change the result of the function).

It does allow functions that log their calls (as that does not contribute to the
result), but I don't think that is enough to satisfy everyone.

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

From: Tucker Taft
Sent: Tuesday, December 27, 2011  9:58 PM

How about something like:

   It is a bounded error if within an assertion expression (directly or
   indirectly) there is a construct that changes the value of an object whose
   original value possibly contributes to the value of the expression (directly
   or indirectly).

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

From: Randy Brukardt
Sent: Tuesday, December 27, 2011  10:44 PM

Much better. The remaining question is what "possibly contributes" means. I
think the intent is fairly clear (the value appears directly or indirectly
somewhere else in the expression; it doesn't matter if that part is executed or
not). [In the case of the rule having to do with multiple expressions, it
appears in one of the other expressions; even easier.]

But I can imagine Steve or Adam arguing about something like:

     Pre => SE and then False and then Glob > 0

where SE modifies Glob. One certainly can argue that Glob does not contribute in
this expression. Of course, then one modifies False to a named constant and then
to a static expression known to be False and then to a non-static expression
that the compiler can prove to be False, and we've gone down the slippery slope
to Hades.

Maybe we should just talk about the variable directly. That's what the wording
you were trying to copy did. How about:

    It is a bounded error if within an assertion expression (directly or
    indirectly) there is a construct C that alters the value of a variable whose
    original value could be used (directly or indirectly) in some other
    construct C2 that is part of the assertion expression but is not part of C.

["could be used" doesn't sound much better to me]

or maybe:

    It is a bounded error if within an assertion expression (directly or
    indirectly) there is a construct C1 that alters the value of a variable
    whose original value possibly contributes (directly or indirectly) to the
    value of some other construct C2 that is part of the assertion expression
    but is not part of C1.

[there's that phrase again. Still doesn't work.]

or maybe even (copying even more of the other rule):

    It is a bounded error if within an assertion expression (directly or
    indirectly) there is a construct C1 that alters the value of a variable
    whose name appears (directly or indirectly) in some other construct C2 that
    is part of the assertion expression but is not part of C1.

Humm. This latter version seems to reintroduce the memo-function problem,
because even local variables are included:
    Save_Memo1_Result : Natural;
    Same_Memo1_Param  : Natural;
    function Memo1 (P : Natural) return Natural is
        Temp : Natural;
    begin
        if Save_Memo1_Param = P then
            return Save_Memo1_Result;
        else
            Temp := ...;
            Save_Memo1_Param := P;
            Save_Memo1_Result := Temp;
            return Temp;
        end if;
    end Memo1;
Here Temp would trigger the bounded error, even though it is obviously not
relevant.

Is it possible for a variable to be altered anywhere other than in a function
(and still be part of an expression)? If not, perhaps we can consider the entire
function as "the construct" and avoid this problem.

    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
    whose name appears (directly or indirectly) in some construct C that is part
    of the assertion expression but is not part of F.

Now we're allowing local variables (because they can't be part of some other
construct not in the function), and memo variables as well (because they should
only appear in that one function).

Still, I'm not that confortable with this. It seems to disallow a shared global
logging facility - perhaps that isn't important enough to worry about.

It's amazing that we know pretty much what we want the rule to be, but we can't
seem to write it unambiguously enough to communicate that. Hope the above will
inspire another try...

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

From: Jean-Pierre Rosen
Sent: Wednesday, December 28, 2011  2:31 AM

>        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 whose
>        name appears (directly or indirectly) in some construct C that is
>        part of the assertion expression but is not part of F.

"whose name appears" can't be right, or I'll call the renaming police...

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

From: Robert Dewar
Sent: Wednesday, December 28, 2011  6:34 AM

> Isn't this too strong? It seems to ban memo functions because the memo
> value "possibly contributes to the value of the expression" (if it is
> used rather than recalculating the function value), and it is
> "updated" by the call to the memo function. The wording here doesn't
> say anything about the value that possibly contributes being different
> in some sense, and that seems necessary to allow memo functions (which
> clearly have a side-effect, but that effect does not change the result of the function).
>
> It does allow functions that log their calls (as that does not
> contribute to the result), but I don't think that is enough to satisfy
> everyone.

Well I wouldn't worry too much, if the rule ends up being over strenuous, no
reasonable implementation will behave badly.

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

From: Randy Brukardt
Sent: Thursday, December 28, 2011  12:04 AM

I originally thought that as well, because no implementation is going to try too
hard to enforce these rules. (Our purpose in adding them is more as a stern
warning to people writing Ada code and to allow aggressive optimizations here.)

But the situation is different for tools. If you have a tool that tries to prove
exception absence (SPARK does this, and I would hope that there are or will be
more general tools of this type), one prong of that is to prove the absence of
any bounded errors. (As the occurrence of a bounded error can cause a
Program_Error to be raised.) Such tools (unless they are strongly tied to a
single implementation) will have to assume the worst (that is, that some
implementation implements the rules literally and detects all such bounded
errors). [Even in the case where no known implementation detects the bounded
error, some future version could.] In which case, a rule which is too strenuous
can be harmful (even if no implementation actually implements that part of the
rule).

So I would much rather have the rule be "just right", and if we have to err, it
ought to be on the side of being a bit looser than ideal.

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