!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. :-) ***************************************************************