!standard  11.4.2(27/3)                             12-05-02    AC95-00232/00
!class Amendment 12-05-02
!status received no action 12-05-02
!status received 12-03-27
!subject Side effects in assertions
!summary

!appendix

From: Robert Dewar
Sent: Tuesday, March 27, 2012  2:25 AM

I must say that the whole business of trying to prevent side effects in
assertions/preconditions/postconditions etc seems very misguided to me.
Fortunately it is very unlikely that any real implementations will pay attention
to this!

It is just likely to preclude useful stuff and cause theoretical uncertainty.

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

From: Randy Brukardt
Sent: Tuesday, March 27, 2012  6:11 PM

I should know better than to wade into this one (especially as I'm not
completely convinced of the approach and because its essentially irrelevant at
this point, we're not going to change anything in the Ada 2012 Standard as the
result of a discussion), but:

(1) This is really an attempt to define what users should not expect to work.
"Significant" side-effects should not be expected to work in assertions, since
they violate all of the principles of assertions (most importantly: adding or
ignoring an assertion should never make a program less safe).

For example, in:

     procedure Foo
        with Pre => A is
        pragma Assert (A);
     begin

If evaluating A changes something such that the pragma Assert fails, there is a
significant problem with "A". Such an expression is necessarily tricky (if
useful) or downright dangerous, and it harms the understandability of the code
(the predicate doesn't hold inside the subprogram). It potentially harms
analysis and optimization of the code as well.

We really do not want people writing such assertion expressions.

Similarly, in:

    subtype S
       with Dynamic_Predicate => F(S);
    procedure Bar (P : S)
       with Pre => G(S);

Here, it is important that the order of evaluation of the expressions does not
matter. In particular, if F(S) and then G(S) gets a different result from G(S)
and then F(S), then whether or not Bar can be called is indeterminate. That is
bad, and again we want to strongly discourage such assertion expressions.

Any time either of these situations are violated, the effect of the code is hard
to predict. In particular, many bad things can happen: X'Old does not reflect
the value of X at the start of the subprogram; predicates and preconditions
don't hold inside of a subprogram; postconditions and invariants don't hold
after a subprogram call, and so on.

All of these things are bad, and should be discouraged (or even banned).

If you think any of these cases can be "useful stuff", then you can stop reading
now, because there is nothing really to discuss. I can believe that someone
could somehow use these effects for some interesting effect, but since any such
code is unlikely to be portable (because of the permissions to evaluate
assertions in any order, to short-circuit assertions, and to ignore side-effects
if the result can be determined), such techniques are precisely what we want to
discourage. Ada is not about tricky code!

(Also remember that such tricks can be performed without involving any
assertions. It's only the content of assertions that is restricted.)

(2) How can we discourage these things? We looked at a number of options, but
any choice other than compile-time rejection makes the program less safe in the
margins (if you do something bad, the last thing you want is an exception being
raised randomly).

We also agree that there are "benign" side-effects, like memo functions, call
logging, and the like. We do not want to disallow these.

We'd liked to have crafted a real Legality Rule, but that would require real
global in/out contracts (which we don't have) and probably would have also
prevented some "benign" and useful side-effects. It's just beyond the
state-of-the-art.

Thus, we settled on an implementation-permission. This takes the form of a
narrow rule that allows a compiler to reject only "significant" side-effects.
The intent is that *only* cases like the two described above can be rejected;
other side-effects (even if they affect later calls) *cannot* be rejected.

(3) The effect of the rule should be a stern warning to anyone caring about
portable code to avoid tricky assertions. One hopes that John manages to explain
this more clearly than I can in the Rationale. (He has the handicap of having
missed the meetings where this was discussed at length.)

(4) OTOH, we expected that it would be impossible for a compiler to take
advantage of the permission in all but the most obvious of circumstances. That
is, we're not really expecting compilers to reject anything here -- just having
the threat should help programmers stay on the safe side of assertion
expressions.

If I thought that it was possible to enforce this rule in Janus/Ada, I would
surely do so. But I don't think it will be practical and most likely will fall
back to warnings (and better categorization) instead.

(5) I would not be surprised if the rule will need tweaking. If there are any
truly useful cases that it bans, we'll certainly consider modifying it to allow
them. That should be easier as an Implementation Permission than it would have
been as a Legality Rule (as compatibility is unlikely to be impacted). The point
is that this is a narrow rule, only banning clearly bad behavior, not anything
that could be useful.

I personally would have preferred to see the rule go somewhat further, such that
evaluating an assertion should not change the effects of following code. (That
way, ignoring an assertion never can cause a problem.) But that is too hard to
define while still allowing "benign" side-effects.

(6) No rule at all would mean that (some) users would expect examples like the
ones above to have well-defined meanings. That would be counter to the intent of
assertions, and also would leave us having to explain the detailed semantics of
'Old, ordering for predicates and precondition checks, and other things we
really don't want to deal with. That way leads to madness.


Anyway, 'nuff said. I'm sure you'll disagree with something irrelevant that I
mentioned in passing. :-)

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

From: Tucker Taft
Sent: Tuesday, March 27, 2012  7:21 PM

Well put, Randy.

Just for the record, this is what is left after all our discussions about side
effects in assertion expressions:

       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.

       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 expression that is checked as part
       of a call on 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.

This seems eminently reasonable, though as you both seem to agree, most
implementations won't take much if any advantage of the permission.  But I could
see it being a reasonable basis for warnings generated by a decent static
analysis tool (like CodePeer ;-).

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

From: Robert Dewar
Sent: Tuesday, March 27, 2012  11:13 PM

Of course the warnings would be appropriate even if the above language were not
present!

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