Version 1.1 of acs/ac-00256.txt

Unformatted version of acs/ac-00256.txt version 1.1
Other versions for file acs/ac-00256.txt

!standard 3.2.4(7/3)          14-02-09 AC95-00256/00
!standard 3.2.4(8/3)
!standard 3.2.4(11/3)
!class confirmation 14-02-09
!status received no action 14-02-09
!status received 13-11-21
!subject Inherited ignored subtype predicates
!summary
!appendix

From: Tucker Taft
Sent: Thursday, November 21, 2013  7:47 PM

AdaCore has implemented subtype predicates, but did not implement the
all-or-nothing rule for predicates as defined in the RM as it relates to
Assertion_Policy.  Here is a summary of what AdaCore ended up implementing:

     At the point in the source where a predicate is declared
     it is either checked or ignored, depending on the policy
     in place at the point of declaration.

     When a type is derived, or a new subtype is declared in terms of
     an existing one, it inherits any checked predicates
     from its parent, but not any ignored ones.

The RM suggests that for any given subtype, either all of the predicates are
checked or none of them, independent of whether the predicate was inherited from
some other subtype.

I was supposed to bring this up earlier, but it got lost somewhere.  So the AI
would be to suggest that we reconsider the rules for Assertion_Policy as it
relates to inherited predicates.

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

From: Randy Brukardt
Sent: Thursday, November 21, 2013  10:01 PM

Could you explain *why* AdaCore decided to ignore the RM in this case? I recall
that we discussed this issue for quite a while, and there were (important?)
reasons for preferring the model described in the RM to the piece-meal model
described above. That is to say, the model in the RM is not an accident, we
wrote it that way on purpose. (I'll go look up what I can find out about those
discussions, but in any case, I'd like to know some reasoning for preferring the
more complex rule described here. I don't think "we don't like the rules" is a
very good reason to ask for reconsideration!)

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

From: Tucker Taft
Sent: Thursday, November 21, 2013  10:14 PM

> Could you explain *why* AdaCore decided to ignore the RM in this case?
> I recall that we discussed this issue for quite a while, and there were
> (important?) reasons for preferring the model described in the RM to
> the piece-meal model described above. That is to say, the model in the
> RM is not an accident, we wrote it that way on purpose.

I gave that feedback at the time this first came up.  However, there are some
arguments on the other side.  The main issue is that someone might think they
have turned off a particularly expensive Dynamic_Predicate by specifying an
Assertion_Policy of Ignore, and then might be surprised to see it suddenly "come
back to life" if another subtype were defined in terms of the first with a
relatively simple Static_Predicate, say.  Adding that Static_Predicate would
have the effect of re-awakening the expensive Dynamic_Predicate.

At this point I am not convinced either way, but it seems at least worth
discussing in an ARG meeting, given some additional experience with the
predicates.  Note also that we have recently decided to change the way
predicates are evaluated, making it more linear, and so it might not be as
difficult to change the rules, and the change might make more sense. One choice
might be to treat Static_Predicates and Dynamic_Predicates separately, so that
turning on Static_Predicates would not automatically turn on Dynamic_Predicates.

> ... (I'll go look up what I can
> find out about those discussions, but in any case, I'd like to know
> some reasoning for preferring the more complex rule described here. I
> don't think "we don't like the rules" is a very good reason to ask for
> reconsideration!)

It was more than that. ;-)

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

From: Randy Brukardt
Sent: Thursday, November 21, 2013  10:09 PM

The relevant AI is AI05-0290-1. The AI itself doesn't explain the predicate
model specifically, but it does give the following overarching rule:

"In order to achieve the intended effect that library writers stay in control
over the enforcement of pre- and postconditions as well as type invariants, the
policy control needs to extend over all uses of the respective types and
subprograms. The place of usage is irrelevant. This is enforced by the rules in
the !wording."

This (oddly) doesn't mention predicates, but given that we want to be able to
switch between preconditions and predicates without semantic change, I'd expect
it to hold for predicates as well. That seems to argue for the all-or-nothing
model.

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

From: Tucker Taft
Sent: Thursday, November 21, 2013  10:20 PM

I don't think this actually applies to the issue.  The argument is not about
whether the predicate of a given named subtype needs to be enforced everywhere
or nowhere; there is general agreement on that.  It is about what happens when
you define a new subtype, and what happens by default if the Assertion_Policy at
the point of the definition of the new subtype is different, and you give an
explicit predicate such as "Static_Predicate => True" or perhaps something only
slightly more restrictive.  Any previously ignored Dynamic_Predicate present on
the underlying subtype might suddenly come back to life.

I think this is the kind of thing best investigated in a room with a
white-board, using various example scenarios.

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

From: Robert Dewar
Sent: Thursday, November 21, 2013  10:38 PM

> Could you explain*why*  AdaCore decided to ignore the RM in this case?
> I recall that we discussed this issue for quite a while, and there were
> (important?) reasons for preferring the model described in the RM to
> the piece-meal model described above. That is to say, the model in the
> RM is not an accident, we wrote it that way on purpose. (I'll go look
> up what I can find out about those discussions, but in any case, I'd
> like to know some reasoning for preferring the more complex rule
> described here. I don't think "we don't like the rules" is a very good
> reason to ask for reconsideration!)

And "I am sure we had a good reason, but we can't remember what it is"
is also not a very good reason for keeping things the way they are. See what you
can dig up. To me the model we implemented in GNAT is far more straightforward
to understand, describe, and implement than the (to me) very peculiar rule in
the RM.

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

From: Randy Brukardt
Sent: Thursday, November 21, 2013  10:40 PM

> At this point I am not convinced either way, but it seems at least
> worth discussing in an ARG meeting, given some additional experience
> with the predicates.  Note also that we have recently decided to
> change the way predicates are evaluated, making it more linear, and so
> it might not be as difficult to change the rules, and the change might
> make more sense.
> One choice might be to treat Static_Predicates and Dynamic_Predicates
> separately, so that turning on Static_Predicates would not
> automatically turn on Dynamic_Predicates.

I think they *are* treated separately, at least as far as when you specify the
policy on a particular kind of assertions (rather than all).

> > ... (I'll go look up what I can
> > find out about those discussions, but in any case, I'd like to know
> > some reasoning for preferring the more complex rule described here.
> > I don't think "we don't like the rules" is a very good reason to ask
> > for reconsideration!)
>
> It was more than that. ;-)

FYI, there isn't anything obvious in the minutes. The mail in the AI is
dominated by last minutes votes and changes (as this was the very last thing
that we finished for Ada 2012), and thus I didn't find any of the reasoning. (I
only skimmed about 25% of mail.)

If we assume that letting "library writers stay in control over the enforcement"
was the main goal, then it seems that the all-or-nothing rule is preferred. That
is, if a library writer requires the predicate of a particular subtype to be
checked, then its best that all parts of it can be assumed to be checked. If
that's not true, then the wrong exception (or no exception) could be raised by a
call, and it could be hard to see why that happened (the source code would
appear to have the correct effect).

By having the "last subtype" control whether the checking is on or off, the
library writer can get checking simply by adding a "subtype A is B;" to their
package.

[Editor's note: This is subtly wrong: you'd have to have a predicate on the
subtype to have this effect. "subtype A is B with Static_Predicate => True;"
would be enough.]

Of course, if the library writer keeps the entire set of subtypes in his/her
package, then there isn't a problem. So this is a pretty marginal case either
way.

Probably the best argument for the alternative is that preconditions and
postconditions work the other way: whether they're on or off depends on the
point of the original declaration. (But perhaps that's another argument for
avoiding class-wide pre/post.)

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

From: Randy Brukardt
Sent: Thursday, November 21, 2013  10:48 AM

...
> > This (oddly) doesn't mention predicates, but given that we want to
> > be able to switch between preconditions and predicates without
> > semantic change, I'd expect it to hold for predicates as well. That
> > seems to argue for the all-or-nothing model.
>
> I don't think this actually applies to the issue.  The argument is not
> about whether the predicate of a given named subtype needs to be
> enforced everywhere or nowhere; there is general agreement on that.
> It is about what happens when you define a new subtype, and what
> happens by default if the Assertion_Policy at the point of the
> definition of the new subtype is different, and you give an explicit
> predicate such as "Static_Predicate => True" or perhaps something only
> slightly more restrictive.  Any previously ignored Dynamic_Predicate
> present on the underlying subtype might suddenly come back to life.

I think that was the intent. I recall someone suggesting that this is feature,
in that
    pragma Assertion_Policy(Check);
    subtype A is B;
could be used to make the predicate checks be performed regardless of the state
of B.

[Editor's note: As noted in the previous message, this should be:
    pragma Assertion_Policy(Check);
    subtype A is B with Static_Predicate => True;
]

Another argument in favor of the all-or-nothing model is that predicates can be
built on top of each other. If the original ones aren't checked, the later ones
may not get the correct results. (This is similar to the reasons that we have to
specify the ordering of predicates; evaluating them out of order gets the wrong
answers.)

> I think this is the kind of thing best investigated in a room with a
> white-board, using various example scenarios.

Perhaps. It sounds like a nasty time for the note-taker, though. :-)

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

From: Robert Dewar
Sent: Thursday, November 21, 2013  10:49 PM

> Probably the best argument for the alternative is that preconditions
> and postconditions work the other way: whether they're on or off
> depends on the point of the original declaration.

which seems a simple rule to state, understand, and implement. Anythying else
seems very odd to me!

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

From: Randy Brukardt
Sent: Thursday, November 21, 2013  11:00 PM

...
> And "I am sure we had a good reason, but we can't remember what it is"
> is also not a very good reason for keeping things the way they are.

I *think* I remember what it was, but I'd like to see more confirmation of that
(particularly examples). But I don't really want to spend 4 hours reading a 500K
AI to find anything - I would have thought that someone asking for
reconsideration would need to do that.

> See what you can dig up. To me the model we implemented in GNAT is far
> more straightforward to understand, describe, and implement than the
> (to me) very peculiar rule in the RM.

It's hard to imagine anything "far more straightforward" than either check or
don't check. :-) Perhaps it is more consistent with other assertions; but I'd
expect them to be about the same in difficulty to understand and describe. But I
don't see any justification for saying that it is easier to implement -- you
have to keep all of the predicates around in any case (they *always* reappear in
memberships and 'Valid; "Ignore" has no effect there), so it would seem that
ignoring some of them rather than all would be harder (needing separate bits for
each predicate, rather than just one per subtype) -- but I doubt that there
would be much difference in effort in any case.

IMHO, these models are about the same in "understand, describe, and implement",
so the main issue is which makes more sense for usage. (And that's not wildly
different either.)

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

From: Robert Dewar
Sent: Friday, November 22, 2013  9:59 AM

> IMHO, these models are about the same in "understand, describe, and
> implement", so the main issue is which makes more sense for usage.
> (And that's not wildly different either.)

In practice I suspect no one will ever notice the difference, so if GNAT
continues to have a bug here, it is unlikely to show up in real customer code,
and hence unlikely to be fixed any time soon :-)

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

From: Robert Dewar
Sent: Friday, November 22, 2013  10:05 AM

Note that this is of course an argument for leaving things as is, unless someone
comes up with a very clear usage argument for changing things.

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

From: Randy Brukardt
Sent: Friday, November 22, 2013  12:44 PM

Right; that was why I originally asked for a justification for the change.
After all, the Standard is published (and soon to be printed) with the current
rules, so we need a reason to make a change. Generally, that means that the
current rules are broken in some way, but that doesn't seem to be the case here.

Moreover, ignoring of assertions is somewhat of a corner case: in many uses, all
assertions will be ignored, in which case the question of whether or not a
particular assertion is ignored isn't interesting. (And of course, if no
assertions are ignored, the rule has nothing interesting to say, either).

So we're mainly talking about cases where some packages have assertions ignored
and others do not AND a subtype is defined in terms of a subtype from another
package AND both subtypes have predicates. Not a very common occurrence, I would
think.

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

From: Robert Dewar
Sent: Friday, November 22, 2013  2:03 PM

Indeed, probably will only EVER show up in corner case tests :-)

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

From: Randy Brukardt
Sent: Friday, November 22, 2013  2:17 PM

Right, and since ACATS C-Tests are supposed to be usage-oriented, such a test
isn't a very high priority. (As such, I doubt that it would ever get written.)
Indeed, the only test involving Ignore that I put on the high priority list is
to check that predicates are still evaluated in a membership even if they are
ignored. (That seems like something that a compiler could easily get wrong, and
a programmer could sensibly write code that depends upon that behavior.)

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

From: Steve Baird
Sent: Friday, November 22, 2013  5:08 PM

> Note also that we have recently decided to change the way predicates
> are evaluated, making it more linear, and so it might not be as
> difficult to change the rules, and the change might make more sense.

FWIW, AI12-0071 is all about ensuring (at least if assertion_policy interactions
are ignored) that given

      subtype S1 is ... ;
      subtype S2 is S1 with Dynamic_Predicate => ... ;

the predicate of S2 will never be evaluated without first confirming that the
value being tested belongs to S1. If, for example, S1's predicate implies that
some access-valued component's value is non-null, then it should be safe for
S2's predicate to dereference that component.

If we disable runtime checking of S1's predicate but enable runtime checking of
S2's predicate, it seems like this could lead to unpleasant surprises. On the
other hand, the situation for S2's predicate expression is neither better nor
worse than the situation for any other client of S1 who relies on a predicate
which turns out to be disabled.

I'm not claiming that this provides a conclusive answer to the question being
discussed, but it seemed worth mentioning.

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

From: Robert Dewar
Sent: Friday, November 22, 2013  5:15 PM

> If we disable runtime checking of S1's predicate but enable runtime
> checking of S2's predicate, it seems like this could lead to
> unpleasant surprises.

I don't see why, you should only suppress predicate checking if you are sure
that the checks will succeed. To me it's just like suppressing overflow
checking. If you have a predicate then it should be met or your program is
wrong. Predicate checks are suppressed at your own risk, and to me, you are
saying, ignore this check, because I know everything is fine.

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

From: Steve Baird
Sent: Friday, November 22, 2013  5:30 PM

In support of your position, the most likely unpleasant surprise is that some
exception other than Assertion_Error will come flying out of a predicate check
that would have raised Assertion_Error if all predicates were enabled.

One can construct examples where the consequences are worse, but you have to
work at it.

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

From: Randy Brukardt
Sent: Friday, November 22, 2013  5:26 PM

> FWIW, AI12-0071 is all about ensuring (at least if assertion_policy
> interactions are ignored) that given
>
>       subtype S1 is ... ;
>       subtype S2 is S1 with Dynamic_Predicate => ... ;
>
> the predicate of S2 will never be evaluated without first confirming
> that the value being tested belongs to S1.
> If, for example, S1's predicate implies that some access-valued
> component's value is non-null, then it should be safe for S2's
> predicate to dereference that component.
>
> If we disable runtime checking of S1's predicate but enable runtime
> checking of S2's predicate, it seems like this could lead to
> unpleasant surprises. On the other hand, the situation for S2's
> predicate expression is neither better nor worse than the situation
> for any other client of S1 who relies on a predicate which turns out
> to be disabled.
>
> I'm not claiming that this provides a conclusive answer to the
> question being discussed, but it seemed worth mentioning.

Thanks. I mentioned this yesterday, but without the nice example. I'm not sure
that there is any very conclusive answer to this question. :-)

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

Questions? Ask the ACAA Technical Agent