CVS difference for ai05s/ai05-0290-1.txt

Differences between 1.9 and version 1.10
Log of other versions for file ai05s/ai05-0290-1.txt

--- ai05s/ai05-0290-1.txt	2012/04/03 22:21:06	1.9
+++ ai05s/ai05-0290-1.txt	2012/04/28 05:10:22	1.10
@@ -186,7 +186,7 @@
 
 Replace 6.1.1(19/3) with:
 
-If performing checks is required by the Pre, Pre'Class, Post, or Post'Class 
+If performing checks is required by the Pre, Pre'Class, Post, or Post'Class
 assertion policies (see 11.4.2) in effect at the point of a corresponding aspect
 specification applicable to a given subprogram or entry, then the respective
 precondition or postcondition expressions are considered @i(enabled).
@@ -627,7 +627,7 @@
 
 @drepl
 The @i<policy_>@fa<identifier> of a @fa<pragma> Assertion_Policy shall be either Check,
-Ignore, or an implementation-defined identifier. 
+Ignore, or an implementation-defined identifier.
 @dby
 The @i<assertion_>@fa<aspect_mark> of a @fa<pragma> Assertion_Policy shall be one of
 Assert, Static_Predicate, Dynamic_Predicate, Pre, Pre'Class, Post,
@@ -641,7 +641,7 @@
 A @fa<pragma> Assertion_Policy is a configuration pragma that specifies the assertion policy
 in effect for the compilation units to which it applies. Different policies may apply to
 different compilation units within the same partition. The default assertion policy
-is implementation-defined. 
+is implementation-defined.
 @dby
 A @fa<pragma> Assertion_Policy determines for each assertion aspect named in
 the @fa<pragma_argument_association>s whether assertions of the given aspect are to
@@ -691,7 +691,7 @@
 !corrignedum 11.4.2(17/2)
 
 @ddel
-The assertion policy that applies to a generic unit also applies to all its instances. 
+The assertion policy that applies to a generic unit also applies to all its instances.
 
 !corrignedum 11.4.2(18/2)
 
@@ -5511,6 +5511,62 @@
 
 ****************************************************************
 
+From: Bob Duff
+Sent: Friday, March 2, 2012  5:26 PM
+
+> >      X: Nonzero'Base := 0; -- no exception
+> >
+> >      type Color is (Red, Yellow, Green, None)
+> >          with Static_Predicate =>  Color /= None;
+
+I'm not actually sure that's legal.  Is "None" visible here?
+Never mind, it's not important to the issues being discussed.
+
+> >      subtype Optional_Color is Color'Base; -- allows None
+> >
+> > For composites, there's no 'Base, so it applies to all objects of
+> > the type (modulo some loopholes):
+>
+> Sure, but 'Base for integer types is an odd beast anyway, I virtually
+> never saw it in user code.
+
+I don't see why it's an "odd beast".  I agree it's not particularly common, but
+I sometimes use it.  Like this, for example:
+
+    type Index is range 1..Whatever;
+    type My_Array is array(Index range <>) ...;
+
+    subtype Length is Index'Base range 0..Index'Last;
+
+And then use variables of subtype Length to point to the last-used component of
+variables of type My_Array.
+
+In Ada 83, you had to declare Length first, and then declare Index in terms of
+Length, and that still works, but the above seems better -- the main thing is
+the array index, then I add a subtype that "by the way" includes the extra zero
+value, in case of empty arrays.
+
+> And this is really no different from
+>
+>    type R is range 1 .. 10;
+>
+>    R'Base
+>    range disappeared
+
+Not sure what you're trying to say here.  I agree, it's "no different".
+The 'Base attribute takes away the predicate, and also takes away the
+constraint.  I have no objection to that, and it's occassionally useful. I just
+wish 'Base worked for composite types.
+
+My main point was to agree with Tucker that predicates don't apply to all values
+of a type, but only to a subset (at least for scalars).
+
+By the way, the more I think about this stuff, the more I agree with those who
+have said predicate violations should raise Constraint_Error rather that
+Assert_Failure!
+
+****************************************************************
+
 From: Tucker Taft
 Sent: Friday, March 2, 2012  4:52 PM
 
@@ -5617,5 +5673,1372 @@
 
 The implementation model is that an implementation should be able to compile a
 limited wither after only parsing the limited withee.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, March 2, 2012  5:30 PM
+
+> At this point it looks simpler to disallow the conversion if different
+> assertion policies apply to the two designated subtypes, even if we
+> don't know for sure whether there is a predicate.
+
+Now we are back to undesirable choice B:
+   Conservatively disallow otherwise-legal constructs
+   because of assertion policy incompatibilities even
+   though there are no assertions of any kind in the
+   entire program.
+
+This is a point I would like to get consensus on before working on RM wording.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, March 2, 2012  5:31 PM
+
+> There would be bigtime implementation problems if we ever introduced a
+> language rule that required resolution of a name which occurs in a
+> limited view of a package.
+
+Tuck - I didn't mean to suggest that you were advocating such a language rule;
+in your message, you had already pointed out that this approach doesn't work in
+the general case.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, March 2, 2012  5:40 PM
+
+>> At this point it looks simpler to disallow the conversion if
+>> different assertion policies apply to the two designated subtypes,
+>> even if we don't know for sure whether there is a predicate.
+>
+> Now we are back to undesirable choice B:
+> Conservatively disallow otherwise-legal constructs because of
+> assertion policy incompatibilities even though there are no assertions
+> of any kind in the entire program.
+>
+> This is a point I would like to get consensus on before working on RM
+> wording.
+
+Using the term "incompatibility" is a bit misleading... ;-) I would say
+"conflicts" so you don't scare anyone.
+
+Anyone who is using conflicting assertion policies but has no assertions of any
+kind in the program is asking for trouble, in my mind...
+
+Are we really just worried about conversions between access-to-incomplete types,
+or is there a bigger problem here?
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, March 2, 2012  5:47 PM
+
+> At this point it looks simpler to disallow the conversion if different
+> assertion policies apply to the two designated subtypes, even if we
+> don't know for sure whether there is a predicate.
+
+So I write a program and debug/test with all-checks-on, as is common practice.
+Then I turn some checks off, and it turns illegal?  I don't know what the right
+answer is here, but I'm pretty sure this isn't the right answer.
+
+If one turns checks off, and one violates the checks, one should expect bad
+things to happen.
+
+> > package Pkg1 is
+> > type Even is new Integer with
+> > Dynamic_Predicate => Even mod 2 = 0; end Pkg1;
+&c
+
+Tuck, your mailer is deleting indentation.  Mailers that molest mail content are
+a menace, and should be banished (grumble). But maybe you could just turn that
+malfeature off?
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, March 2, 2012  5:58 PM
+
+> Using the term "incompatibility" is a bit misleading... ;-) I would
+> say "conflicts" so you don't scare anyone.
+>
+
+Good point.
+
+> Anyone who is using conflicting assertion policies but has no
+> assertions of any kind in the program is asking for trouble, in my
+> mind...
+
+Yeah, but I was just demonstrating the point with an extreme example. Either
+there is a need for varying assertion policies within a partition or there isn't
+- if there is, then this problem can arise.
+
+> Are we really just worried about conversions between
+> access-to-incomplete types, or is there a bigger problem here?
+>
+
+There are variations; P.all'Access is effectively a
+type conversion.
+
+I think that what it really comes down to is the
+definition of "statically matching" for subtypes;
+to see where the problems are, look where that is
+used. As your question suggests, I think we can
+dismiss RM uses of "statically matching" that cannot
+involve an incomplete type.
+
+There was also the issue that determining whether a
+private type has a specified predicate breaks privacy,
+but we know how to implement that (and, if you think
+of predicates as being similar to constraints, then
+it seems reasonable to treat a predicate spec as being
+just another kind of rep spec).
+
+****************************************************************
+
+From: Bob Duff
+Sent: Friday, March 2, 2012  5:59 PM
+
+> Using the term "incompatibility" is a bit misleading... ;-) I would
+> say "conflicts" so you don't scare anyone.
+
+Right.  But are you sure there no real incompatibilities
+(2005-2012) here?  Say a program contains pragmas Assert, no other assertions,
+and contains pragmas Assertion_Policy. It seems like you're wanting to add an
+assume-the-worst rule just-in-case there are predicates, which there aren't.
+Isn't that incompatible?
+
+I hope I have the sense to butt out of this conversation soon!
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, March 2, 2012  6:09 PM
+
+I agree with both of you, but mostly Tuck.
+
+Tuck was referring to my use of the word "incompatibility" in talking about
+about a single partition where the entire partition did not share the same
+assertion policy.
+
+Bob is raising the point that there is an incompatibility here in the usual
+sense (we reject a program that used to compile), but Tuck was correct that I
+was not talking about that kind of incompatibility when I used the term.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Friday, March 2, 2012  6:38 PM
+
+> Now we are back to undesirable choice B:
+>   Conservatively disallow otherwise-legal constructs
+>   because of assertion policy incompatibilities even
+>   though there are no assertions of any kind in the
+>   entire program.
+>
+> This is a point I would like to get consensus on before working on RM
+> wording.
+
+I suppose that if I'm going to talk about choice B and request a consensus, then
+I ought to also present a choice A.
+
+We could simply ignore assertion policy in deciding whether two names denoting
+the same subtype denote statically matching subtypes and then say that in cases
+where a stricter conformance check along the lines of the stuff we have been
+discussing today would have flagged a problem, users instead get
+implementation-dependent assertion enforcement. Or perhaps we could even define
+some portable rules for resolving these assertion-policy conflicts.
+
+This would be a simpler model, but it would make predicates easier to violate
+(and might introduce portability issues).
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Saturday, March 3, 2012  12:44 PM
+
+> Now we are back to undesirable choice B:
+>   Conservatively disallow otherwise-legal constructs
+>   because of assertion policy incompatibilities even
+>   though there are no assertions of any kind in the
+>   entire program.
+
+I find this not just undesirable; it is close to unacceptable.
+
+Why is there no further discussion on treating subtype predicates in the
+constraints/checks/suppressable category rather than the assertion/ignorable
+category?
+
+If the main point of resistance is that predicate checks unlike constraint
+checks are not to be assumed to be "true" when suppressed, than this rule can be
+easily stated as such. It would certainly be a rule far preferable to the rules
+that are being discussed currently.
+
+It also would automatically allow for Steve's proposal phrased as "...users
+instead get implementation-dependent assertion enforcement"
+
+If "erroneousness by suppressing" is the issue, well (apart from my opinion that
+it is indeed erroneous to ignore a failed subtype predicate), then one could
+probably also describe it as a bounded error to create an invalid value by
+ignoring/suppressing the failed check or limit the suppressing in Steve's sense.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, March 3, 2012  1:05 PM
+
+> ... If the main point of resistance is that predicate checks unlike
+> constraint checks are not to be assumed to be "true" when suppressed,
+> than this rule can be easily stated as such. It would certainly be a
+> rule far preferable to the rules that are being discussed currently.
+
+This would mean that the compiler could never trust a predicate on a subprogram
+parameter, on a global variable, on a dereferenced object, etc.  That would seem
+to imply a lot of overhead.
+
+If the only issue is conversion between access-to-incomplete types, I am
+reluctant to give up everything else just for those.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, March 3, 2012  1:50 PM
+
+> Why is there no further discussion on treating subtype predicates in
+> the constraints/checks/suppressable category rather than the
+> assertion/ignorable category?
+
+I am in favor of this, I think trying to ignore predicates makes no sense.
+
+> If the main point of resistance is that predicate checks unlike
+> constraint checks are not to be assumed to be "true" when suppressed,
+> than this rule can be easily stated as such. It would certainly be a
+> rule far preferable to the rules that are being discussed currently.
+>
+> It also would automatically allow for Steve's proposal phrased as
+> "...users instead get implementation-dependent assertion enforcement"
+>
+> If "erroneousness by suppressing" is the issue, well (apart from my
+> opinion that it is indeed erroneous to ignore a failed subtype
+> predicate), then one could probably also describe it as a bounded
+> error to create an invalid value by ignoring/suppressing the failed
+> check or limit the suppressing in Steve's sense.
+
+I really don't mind failed predicates being just as bad as failed constraints
+(any differentiation between the two seems hard to explain and plain odd).
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, March 3, 2012  1:51 PM
+
+> This would mean that the compiler could never trust a predicate on a
+> subprogram parameter, on a global variable, on a dereferenced object,
+> etc.  That would seem to imply a lot of overhead.
+
+I think the compiler should be allowed to trust predicates exactly to the same
+extent it is allowed to trust constraints, no more, and no less.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Saturday, March 3, 2012  2:16 PM
+
+>> Why is there no further discussion on treating subtype predicates in
+>> the constraints/checks/suppressable category rather than the
+>> assertion/ignorable category?
+>
+> I am in favor of this, I think trying to ignore predicates makes no
+> sense.
+  ...
+
+If we go this route, then I would be in favor of the suggestion that predicate
+checks raise Constraint_Error on failure, and we treat them as similarly to
+constraints in every way.  That is, assign them their own "_Check" identifier
+and have them controlled by pragma Suppress/Unsuppress.
+
+I agree that the more we talk about them, the more they resemble subtype
+constraints, and trying to give them the same "pampering" we give the other
+assertion-like things doesn't seem to be working.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, March 3, 2012  2:33 PM
+
+> I think the compiler should be allowed to trust predicates exactly to
+> the same extent it is allowed to trust constraints, no more, and no
+> less.
+
+I agree.  And they should raise Constraint_Error on failure, as for constraints
+and "not null".
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, March 3, 2012  2:33 PM
+
+>> I am in favor of this, I think trying to ignore predicates makes no
+>> sense.
+>    ...
+>
+> If we go this route, then I would be in favor of the suggestion that
+> predicate checks raise Constraint_Error on failure, and we treat them
+> as similarly to constraints in every way.  That is, assign them their
+> own "_Check" identifier and have them controlled by pragma
+> Suppress/Unsuppress.
+
+I agree 100% with this proposal
+
+> I agree that the more we talk about them, the more they resemble
+> subtype constraints, and trying to give them the same "pampering" we
+> give the other assertion-like things doesn't seem to be working.
+
+I think it is just confusing to try to distinguish them from subtype
+constraints.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, March 3, 2012  2:34 PM
+
+> I agree that the more we talk about them, the more they resemble
+> subtype constraints, and trying to give them the same "pampering" we
+> give the other assertion-like things doesn't seem to be working.
+
+Maybe they should be called Constraint instead of Predicate (half kidding :-))
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Saturday, March 3, 2012  4:39 PM
+
+> If we go this route, then I would be in favor of the suggestion that
+> predicate checks raise Constraint_Error on failure, and we treat them
+> as similarly to constraints in every way.  That is, assign them their
+> own "_Check" identifier and have them controlled by pragma
+> Suppress/Unsuppress.
+
+That is exactly the notion that I would like to see explored more.
+Intuitively, it seems "right". But I am waiting for Steve's "have you considered
+... ?".
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, March 4, 2012  6:53 PM
+
+> That is exactly the notion that I would like to see explored more.
+> Intuitively, it seems "right". But I am waiting for Steve's "have you
+> considered ... ?".
+
+I'm not Steve, but have you considered ;-) that Suppress eliminates checks based
+on their location, while assertions (contract if you prefer) eliminate checks
+based on the declaration?
+
+This works for constraints only because any check that would fail (but is not
+detected by a suppressed check) makes the program erroneous. In that case, the
+fact that the body of the subprogram is "wrong" (assumes that the check is made)
+is OK (the program makes no sense anyway). (Arguably, this is not the way
+Suppress was really intended to work, as evidenced by the "On" parameter to the
+Suppress pragma, but it never was properly defined.)
+
+But there never has been any support for making predicates (or any other
+assertions) cause erroneous execution in this way. (The idea being that adding a
+predicate should never make a program less safe, in any language-defined mode.)
+
+That means that if you have location-based Suppress, then you cannot use
+predicates to move correctness checks into the contract rather than in the body.
+When the check state is ignore at some call site, you neither get a check nor
+erroneous execution if that check fails. Thus you have to repeat the check in
+the body (and moreover, the compiler can almost never optimize the duplicate
+check away). OTOH, preconditions work "right", so the net effect is that you
+always have to use a precondition rather than a predicate (which is usually
+going to be more complicated and less readable). That would strip away a large
+part of their value.
+
+Erhard, you have been as concerned about this as I have, so I don't understand
+why you're willing to abandon it now.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, March 4, 2012  7:07 PM
+
+...
+> But there never has been any support for making predicates (or any other
+> assertions) cause erroneous execution in this way. (The idea being
+> that adding a predicate should never make a program less safe, in any
+> language-defined mode.)
+
+I understand the idea, but the fact of the matter is it just doesn't work to
+somehow thing of predicates as something that makes the program safer. They
+really fundamentally change the meaning of the program, just as constraints do.
+Any attempt at distinguishing them from constraints is IMO doomed to end up in a
+mess.
+
+> Erhard, you have been as concerned about this as I have, so I don't
+> understand why you're willing to abandon it now.
+
+I do!
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, March 4, 2012  7:09 PM
+
+...
+> We could simply ignore assertion policy in deciding whether two names
+> denoting the same subtype denote statically matching subtypes and then
+> say that in cases where a stricter conformance check along the lines
+> of the stuff we have been discussing today would have flagged a
+> problem, users instead get implementation-dependent assertion
+> enforcement. Or perhaps we could even define some portable rules for
+> resolving these assertion-policy conflicts.
+
+It's pretty clear that the "default" should be "Check"; that is, if there is any
+"conflict", "Check" always wins. Everybody has to see "Ignore" before we ignore
+anything.
+
+But I have to admit, this doesn't seem to be working.
+
+What I don't understand (or perhaps remember) is what was so bad about the
+"simple" model that the policy that applies to the predicate is what applies to
+the check? The way Tucker wrote that model up during the meeting didn't work,
+but that was a terminology problem rather than any real definitional problem.
+That model avoids problems with static matching (because the subtypes that match
+are identical to the policies applied), it doesn't assign a meaning to
+"renaming" subtypes (which bothered people about some other models).
+
+It works properly for contracts (so long as you are careful), it doesn't cause
+these definitional problems, and it doesn't introduce erroneousness. So what
+have I missed??
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, March 4, 2012  7:47 PM
+
+> I understand the idea, but the fact of the matter is it just doesn't
+> work to somehow thing of predicates as something that makes the
+> program safer. They really fundamentally change the meaning of the
+> program, just as constraints do. Any attempt at distinguishing them
+> from constraints is IMO doomed to end up in a mess.
+
+I tried to make a point like this last fall, and was essentially told I was
+crazy. Apparently, it is only crazy if I try to explain it...sigh.
+
+Anyway, I don't disagree with your point, but it is important to realize that
+anything that is true about predicates is also true about preconditions. That
+is, some specifications have to be given in precondition form (because they
+involve multiple parameters), but other specifications can be given in either
+predicate or precondition (or constraint for that matter) forms. It is
+uncomfortable for those to be handled differently.
+
+And I don't want something a client does to introduce errors (or
+erroneousness) into my code - no matter how I describe the contract.
+
+(I can show examples of all of these cases using the Ada.Containers as a basis,
+if you need examples of what I'm talking about.)
+
+One of the appealing things about predicates is that they (appear) to offer a
+way to avoid the bugs caused by client suppression of constraint checks. Using
+an assertion model, I'd definitely consider eliminating almost all of the
+constraints from my program. If we use a Suppression model for predicates but
+not preconditions, then that will force everything into preconditions.
+
+Let me make it clear that virtually any model would be preferable to the one
+Tucker and Steve seem to be describing. So I could imagine following a purely
+suppression model for predicates if we can't work out something better. But I'm
+very dubious that there was any problem with the "policy at the point of
+predicate declaration" model.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, March 4, 2012  7:59 PM
+
+> Anyway, I don't disagree with your point, but it is important to
+> realize that anything that is true about predicates is also true about
+> preconditions. That is, some specifications have to be given in
+> precondition form (because they involve multiple parameters), but
+> other specifications can be given in either predicate or precondition
+> (or constraint for that
+> matter) forms. It is uncomfortable for those to be handled differently.
+
+I do not think of predicates this way at all, I think of them just as
+constraints, trying to convolute them with preconditions is to me confusing
+obfuscation.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, March 4, 2012  8:21 PM
+
+That makes sense for static predicates and some other predicates. But keep in
+mind that constraints themselves are a replacement for preconditions (for
+instance, if you use a Positive parameter, you don't usually include that the
+parameter is positive as part of the precondition - but it surely is).
+
+And certainly some dynamic predicates would exist only for the purpose of
+simplifying preconditions in this way. For instance, if you had:
+
+     subtype Valid_Root_Window_Type is Root_Window_Type
+         with Dynamic_Predicate => Is_Valid (Valid_Root_Window_Type);
+
+in Claw, you could use it on most of the operations to eliminate having to
+mention this in (almost) every precondition. It would be preferable because the
+name of the subtype would serve as a reminder of the requirement (it wouldn't be
+necessary to read the precondition).
+
+If predicates work differently than preconditions, then 3rd-party developers
+(and the Standard itself) can really only use preconditions for this sort of
+thing (or at least have a strong incentive to do so), and that will clutter and
+lengthen the preconditions a lot. Bob has said that he uses predicates almost
+exclusively for this sort of thing, so it is not just me thinking this way. (Not
+to put thoughts into Bob's mouth though - I don't know if he cares about how
+assertion policy works at all.)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Sunday, March 4, 2012  8:40 PM
+
+>...Bob has said that he uses predicates  almost exclusively for this
+>sort of thing, so it is not just me thinking  this way.
+
+Yes.  In many cases, at first I think I need a precondition, and then I see that
+the same precondition applies to many procedures, and it's a property of a
+single parameter, so I switch to a predicate.  And then I can use it for local
+variables, components, etc.  Good.
+
+The only time I really need a precondition is when it refers to two or more
+parameters.  Other times, predicates usually seem better.  For DRY if nothing
+else.
+
+>...(Not to put thoughts into Bob's mouth though - I don't know if he
+>cares about how assertion policy works at all.)
+
+I care, but I've come to the conclusion that it doesn't much matter what the
+Standard says.  Implementations will do what their customers want.  I think we
+can safely let the market decide, in this case.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, March 4, 2012  8:46 PM
+
+> Yes.  In many cases, at first I think I need a precondition, and then
+> I see that the same precondition applies to many procedures, and it's
+> a property of a single parameter, so I switch to a predicate.  And
+> then I can use it for local variables, components, etc.  Good.
+>
+> The only time I really need a precondition is when it refers to two or
+> more parameters.  Other times, predicates usually seem better.  For
+> DRY if nothing else.
+
+Well the above are incompatible observations to me.
+
+You say in the first para that a predicate is appropriate if it applies to many
+procedures. But if you have a precondition that applies to a single parameter
+for a single procedure, it ends up being heavier to use a predicate, since it
+requires you to declare a special subtype just for that procedure call.
+
+****************************************************************
+
+From: Jeff Cousins
+Sent: Monday, March 5, 2012  5:30 AM
+
+Speaking as a poor old user I agree with Robert, predicates are a lot easy to
+understand if they work like constraints and are suppressed like constraints.
+Predicates have been "sold" as being a cleverer form of constraints, and it's
+confusing if they sit in a fuzzy area half way between constraints and
+assertions.
+
+There is Randy's problem that you cannot use predicates to move correctness
+checks into the contract rather than in the body, but as this problem already
+exists for constraints I think it should be solved in a common way, say a pragma
+or aspect "suppress_determined_at_call_site_not_body" in the spec.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, March 5, 2012  5:48 AM
+
+I think people are worrying too much about the detailed issue of what happens
+when suppressed checks fail.
+
+For preconditions and postconditions, I think it is just fine for these to be
+totally ignored if suppressed, like assertions (sorry can't help using this term
+in its obvious sense, i.e. stuff done with pragma assert).
+
+But predicates really do read like constraints (and BTW I think
+*should* raise constraint error if they fail).
+
+"poor old users" have the following pretty simple view of constraints.
+
+You leave checks on unless you are absolutely sure that the checks won't fail,
+and you really need the extra performance. Then, if and only if these two
+factors are true, you suppress checks.
+
+The issue of exactly what happens if checks fail when they are suppressed is
+something that only language lawyers know for constraints, and that will
+continue to be true for predicates no matter what we decide, users simply won't
+know the rules (and won't think that they have to, because they will only
+suppress checks when they are sure they won't fail).
+
+****************************************************************
+
+From: Jeff Cousins
+Sent: Monday, March 5, 2012  5:56 AM
+
+Yes to all that.
+
+****************************************************************
+
+From: Erhard Ploedereder
+Sent: Monday, March 5, 2012  7:22 AM
+
+> That means that if you have location-based Suppress, then you cannot
+> use predicates to move correctness checks into the contract rather
+> than in the body. When the check state is ignore at some call site,
+> you neither get a check nor erroneous execution if that check fails.
+> Thus you have to repeat the check in the body (and moreover, the
+> compiler can almost never optimize the duplicate check away). OTOH,
+> preconditions work "right", so the net effect is that you always have
+> to use a precondition rather than a predicate (which is usually going to be more complicated and less readable).
+> Erhard, you have been as concerned about this as I have, so I don't
+> understand why you're willing to abandon it now.
+
+Correct, but arguably this is not such a bad move. To use subtype predicates for
+that purpose, one needs to introduce a subtype, which either clutters up the
+interface (if it is part of the interface) or the predicate is not visible as
+part of a contract (if it is part of the body of the interface). I don't see why
+PRE does not cover the necessary grounds for this.
+
+> I'm not Steve, but have you considered  that Suppress eliminates
+> checks based on their location, while assertions (contract if you
+> prefer) eliminate checks based on the declaration?> This works for
+> constraints only because any check that would fail (but is not
+> detected by a suppressed check) makes the program erroneous.
+
+The erroneousness I am willing to accept. The Suppress semantics for subtype
+predicates could be made different than for constraints, as far as I am
+concerned to maintain value-safeness, i.e. wahtever applied to the aspect
+specficiation appplies to all checks of the aspect.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March 5, 2012  9:43 AM
+
+> It works properly for contracts (so long as you are careful), it
+> doesn't cause these definitional problems, and it doesn't introduce erroneousness.
+> So what have I missed??
+
+You have to have two different predicates, one which is used for checking, and
+one which is used for membership. Or I suppose you could say is what matters is
+the Assertion_Policy at the point of the "last" explicit aspect specification
+for a predicate.  That means if you want to change whether a given predicate
+check is enabled, you have to write
+
+   ... with Static_Predicate => True;
+
+at a point where you have specified a different Assertion_Policy.
+
+That could probably work, as you would be unlikely to do that by mistake.
+
+****************************************************************
+
+From: Geert Bosch
+Sent: Monday, March 5, 2012  1:16 PM
+
+> If we go this route, then I would be in favor of the suggestion that
+> predicate checks raise Constraint_Error on failure, and we treat them
+> as similarly to constraints in every way.  That is, assign them their
+> own "_Check" identifier and have them controlled by pragma
+> Suppress/Unsuppress.
+>
+> I agree that the more we talk about them, the more they resemble
+> subtype constraints, and trying to give them the same "pampering" we
+> give the other assertion-like things doesn't seem to be working.
+
+Right, I agree with this. Anything else is just too complicated for users to
+grasp and for us to properly define.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 5, 2012  6:25 PM
+
+> > It works properly for contracts (so long as you are careful), it
+> > doesn't cause these definitional problems, and it doesn't introduce
+> > erroneousness. So what have I missed??
+>
+> You have to have two different predicates, one which is used for
+> checking, and one which is used for membership.
+
+Yes, but that seems necessary in any model (including Suppression). Since
+predicates are always used in memberships, validity checks, and case/loop
+statements (irrespective of the Assertion_Policy), and all subtypes have
+predicates, there are always going to be two predicates associated with every
+subtype (the "full" predicate and the one that depends on the assertion policy).
+The only reason you can get away with a single constraint is that only the last
+constraint is used (it's always a proper subset or fails a check); that model
+does not work for predicates.
+
+> Or I suppose you could say is what matters is the Assertion_Policy at
+> the point of the "last" explicit aspect specification for a predicate.
+> That means if you want to change whether a given predicate check is
+> enabled, you have to write
+>
+>    ... with Static_Predicate => True;
+>
+> at a point where you have specified a different Assertion_Policy.
+>
+> That could probably work, as you would be unlikely to do that by
+> mistake.
+
+I'm not sure this helps much; you've still got two predicates for every subtype.
+And it makes subtype predicates subtly different than preconditions (which would
+be the point of using this model - to make them work the same). Preconditions
+inherit the checking state from parent operations.
+
+Anyway, we have to find a proper model here, and soon, as this is the last
+remaining Ada 2012 issue and we've promised an almost-final standard for review
+ASAP.
+
+Also note that changing predicates to a suppression model would also imply no
+longer classifying them as "assertions". (I cannot imagine how we could still
+call them "assertions" but yet treat them differently in every important
+[user-visible] way - not affected by assertion_policy, erroneous rather than
+ignore, etc.) This would totally destroy our carefully-crafted wording, which
+would have to be completely done over from scratch. Indeed, that also includes
+the bounded error rules for protected actions among other things.
+
+Predicates are more like assertions for most purposes (since arbitrary
+expressions evaluated at arbitrary points have far more "issues" than the much
+more restricted possibilities of constraints). We need (almost) all of the rules
+that apply to assertions (including preconditions, etc.) to apply to them as
+well.
+
+Since assertions (general name) are the most important thing about Ada 2012, it
+appears that we have two unappealing choices:
+(1) Go forward with rules we *know* are wrong, assuming implementers will clean
+    up the mess (with the complete loss of portability that entails); or
+(2) Abandon Ada 2012 altogether, restarting it whenever we figure this stuff out
+    to true agreement (essentially making it Ada 2014).
+
+Blah.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, March 5, 2012  6:50 PM
+
+> Also note that changing predicates to a suppression model would also
+> imply no longer classifying them as "assertions". (I cannot imagine
+> how we could still call them "assertions" but yet treat them
+> differently in every important [user-visible] way - not affected by
+> assertion_policy, erroneous rather than ignore, etc.) This would
+> totally destroy our carefully-crafted wording, which would have to be
+> completely done over from scratch. Indeed, that also includes the
+> bounded error rules for protected actions among other things.
+
+Right, indeed I think we should NOT call predicates assertions, it's confusing.
+
+> Predicates are more like assertions for most purposes (since arbitrary
+> expressions evaluated at arbitrary points have far more "issues" than
+> the much more restricted possibilities of constraints). We need
+> (almost) all of the rules that apply to assertions (including
+> preconditions, etc.) to apply to them as well.
+
+Well they may be more like assertions from a detailed legalistic semantic point
+of view, but the fact remains that they are like constraints from the
+programmers point of view
+
+> Since assertions (general name) are the most important thing about Ada
+> 2012, it appears that we have two unappealing choices:
+
+> (1) Go forward with rules we *know* are wrong, assuming implementers
+> will clean up the mess (with the complete loss of portability that
+> entails)
+
+No I don't see the problem as nearly so intractable, and in fact I think the
+details that we are discussing now are pretty unimportant details. It is a
+common phenomenon that language lawyers regard problems of no great importance
+as significant :-)
+
+> (2) Abandon Ada 2012 altogether, restarting it whenever we figure this
+> stuff out to true agreement (essentially making it Ada 2014).
+
+To me this is a strawman of no significance at this stage. If ISO delays the
+standard it would not have much effect on the implementation scene, which is
+what matters to users *other* than language lawyers. But the effect which it
+*would* have would be wholly negative, and it would be unfortunate to delay over
+essentially unimportant minor points.
+
+Just to be clear, to me as a user, looking at all the suggestions that have been
+made for predicates, I see no big significant difference between them, these are
+VERY minor semantic points if you ask me.
+
+Yes, I know they seem big, language design discussions always have that effect!
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March 5, 2012  6:53 PM
+
+I think a rule that associates the assertion policy with the location of the
+"final" explicit predicate expression that is applicable to the subtype could
+work.  The only other alternative that seems to be simple enough to be
+understandable at this point is the suppress model, where it is erroneous if you
+suppress it and it would have evaluated to False.
+
+I would recommend a straw vote at this point to see which way most folks are
+leaning:
+
+1) Assertion_Policy applies to subtype predicates, based on the last explicit
+   predicate aspect clause, and the effect is that the predicates are not
+   checked on conversion, etc., but are still relevant for membership tests,
+   full case-statement coverage, etc.
+
+   or
+
+2) Suppress(Predicate_Check) applies to predicates, and it is erroneous if the
+   check would have returned False at the point of a suppressed check.
+
+Personally, I am on the fence between these two.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, March 5, 2012  7:15 PM
+
+I strongly favor 2). I have given my reasons. I think that whatever you say in
+the RM, ordinary programmers will think of predicates as being like constraints.
+It won't matter very much if you choose 1) and their thinking is not quite
+accurate, since as I said earlier, in the case where the predicate is not
+violated, the two rules are equivalent, and I think most programmers will figure
+if they suppress predicate checking they had better make sure the predicates are
+not violated.
+
+But all in all, given that programmers will inevitably think of predicates as
+being like constraints, they may as well behave as much like constraints as
+possible.
+
+****************************************************************
+
+From: Steve Baird
+Sent: Monday, March 5, 2012  7:49 PM
+
+> ...
+> it is erroneous if the check would have returned False at the point of
+> a suppressed check.
+
+With suppressed checks, Ada05 gives us an unambiguous definition of when a
+program crosses the line into erroneousness.
+
+The line doesn't seem so clearly defined when we allow arbitrary boolean
+expressions.
+
+Consider, for example, a predicate which has side effects.
+
+I know that such predicates are considered to be poorly behaved, but I still
+want the language to be well-defined if someone does choose to write such a
+thing.
+
+What is the state of a program which depends on the value of a global variable
+that a predicate function "would have" updated?
+
+Is an implementation allowed (but of course not required) to perform a
+suppressed assertion check?
+
+Maybe there are no serious problems here - I haven't had a chance to think
+things through - but I feel nervous about this.
+
+Can we go with 90% of the suppression model, but keep the rule that a suppressed
+predicate check is simply not performed (or perhaps it is
+implementation-dependent as to whether the check is performed, but there are
+only two options: it is, or it isn't).  I generally like the suppression model,
+but I'd feel better if we could avoid using "would have in some alternative
+universe" stuff to define erroneous execution.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, March 5, 2012  7:51 PM
+
+> Well they may be more like assertions from a detailed legalistic
+> semantic point of view, but the fact remains that they are like
+> constraints from the programmers point of view
+
+Well, I agree, but in fact all of the following are pretty-much alike from the
+programmer's point of view:
+
+    constraints (range, index, discrim)
+    null exclusions ("not null")
+    predicates
+    invariants
+    preconditions
+    postconditions
+    pragma Assert
+    if ... then raise Blah
+    when others => raise Program_Error;
+
+Only the details are different.
+
+Did I forget any?  I'd mention digits_constraint and delta_constraint, except
+most programmers have probably never heard of those.
+
+> No I don't see the problem as nearly so intractable, and in fact I
+> think the details that we are discussing now are pretty unimportant
+> details.
+
+Exactly.
+
+>...It is a common phenomenon that language lawyers regard problems  of
+>no great importance as significant :-)
+
+Right, sometimes it's hard for language lawyers to take off the "lawyer" hat and
+put on the "plain old programmer" hat.  ;-)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, March 5, 2012  8:00 PM
+
+> Since assertions (general name) are the most important thing about Ada
+> 2012, it appears that we have two unappealing choices:
+> (1) Go forward with rules we *know* are wrong, assuming implementers
+> will clean up the mess
+
+That would be just fine.  I find it only mildly "unappealing".
+
+>... (with the complete loss of portability that entails); or
+
+There's no loss of portability when checks are turned ON.
+
+And in the big scheme of things, it really doesn't matter that much if there's a
+loss of portability when checks are turned OFF.
+
+> (2) Abandon Ada 2012 altogether, restarting it whenever we figure this
+> stuff out to true agreement (essentially making it Ada 2014).
+
+I never understood the hurry for 2012, but now that it's almost done, it would
+be pretty silly to delay just because the rules for turning off checks are
+somewhat bogus.
+
+Look at the big picture!
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, March 5, 2012  8:04 PM
+
+> Can we go with 90% of the suppression model, but keep the rule that a
+> suppressed predicate check is simply not performed (or perhaps it is
+> implementation-dependent as to whether the check is performed, but
+> there are only two options: it is, or it isn't). I generally like the
+> suppression model, but I'd feel better if we could avoid using "would
+> have in some alternative universe" stuff to define erroneous
+> execution.
+
+I don't think that really works, unless you go for something based on the
+location of a use in some declaration, and I think we agreed that was getting
+pretty complicated.
+
+On the other hand, we could perhaps distinguish static and dynamic predicates,
+and say that the compiler can never assume a dynamic predicate evaluates to
+true, since we know dynamic predicates are not always well behaved.  On the
+other hand, a static predicate is pretty well defined, definitely doesn't have
+any side effects, and is about as equivalent to a range constraint as you can
+get, so it is well defined to say what it means to assume it is true even
+without checking it.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, March 5, 2012  8:04 PM
+
+> I know that such predicates are considered to be poorly behaved, but I
+> still want the language to be well-defined if someone does choose to
+> write such a thing.
+
+I don't care, why not say it is a bounded error to have side effects, and the
+possible effects of a suppressed check is that it might or might not update the
+global or may set it to some unexpected value.
+
+> What is the state of a program which depends on the value of a global
+> variable that a predicate function "would have"
+> updated?
+>
+> Is an implementation allowed (but of course not required) to perform a
+> suppressed assertion check?
+
+I don't care one way or another
+
+> Can we go with 90% of the suppression model, but keep the rule that a
+> suppressed predicate check is simply not performed (or perhaps it is
+> implementation-dependent as to whether the check is performed, but
+> there are only two options: it is, or it isn't).  I generally like the
+> suppression model, but I'd feel better if we could avoid using "would
+> have in some alternative universe" stuff to define erroneous
+> execution.
+
+I think it is fine to insist on the predicate check not being performed if it is
+suppressed. After all the only reason we don't insist on the check being
+suppressed in the constraint case is that it may be infeasible or too expensive
+to suppress the check (e.g. if it is free in hardware), and that reasoning does
+not apply to predicates.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Monday, March 5, 2012  8:09 PM
+
+> On the other hand, we could perhaps distinguish static and dynamic
+> predicates, and say that the compiler can never assume a dynamic
+> predicate evaluates to true, since we know dynamic predicates are not
+> always well behaved.  On the other hand, a static predicate is pretty
+> well defined, definitely doesn't have any side effects, and is about
+> as equivalent to a range constraint as you can get, so it is well
+> defined to say what it means to assume it is true even without
+> checking it.
+
+I could live with that certainly
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 5, 2012  9:47 PM
+
+...
+> Can we go with 90% of the suppression model, but keep the rule that a
+> suppressed predicate check is simply not performed (or perhaps it is
+> implementation-dependent as to whether the check is performed, but
+> there are only two
+> options: it is, or it isn't).  I generally like the suppression model,
+> but I'd feel better if we could avoid using "would have in some
+> alternative universe" stuff to define erroneous execution.
+
+I don't think that works, because it would mean that both (1) you have no
+control over whether clients make a check or not and (2) the program is not
+erroneous if the check fails. Which means that any predicates could not affect
+correctness in a body.
+
+To take a concrete example:
+
+The vector container has the following routine:
+
+function Element (Position  : Cursor) return Element_Type;
+   -- If Position equals No_Element, then Constraint_Error is propagated.
+   -- Otherwise, Element returns the element designated by Position.
+
+Ignoring for the moment the exact exception being raised, this could (and
+probably should) be written as:
+
+     subtype Element_Cursor is Cursor
+         with Dynamic_Predicate => Has_Element (Element_Cursor);
+
+I'm using a predicate here because there are quite a few routines with such a
+requirement, and repeating it over and over in preconditions is not appealing.
+[I'm not thrilled by the subtype name here; Ada.Containers does not have a
+concept of a "null" cursor by that name, and "valid" means something else. I
+don't want to spend too long on this example, so I used the first name that
+works.]
+
+    function Element (Position : Element_Cursor) return Element_Type;
+        -- Element returns the element designated by Position.
+
+A precondition would work, of course:
+
+    function Element (Position : Cursor) return Element_Type
+        with Pre => Has_Element (Position);
+        -- Element returns the element designated by Position.
+
+In both cases, this is assuming that Assertion_Policy is Check, and this is
+specified inside the package Ada.Containers.Vectors.
+
+Now, the problem is that if the client Suppresses predicate checks, then the
+predicate check is not made at the call site. If the resulting body is *not*
+erroneous, then the only possibility for a correct implementation of the
+original specification is to repeat the check within the body of Element.
+
+OTOH, an Assertion_Policy of Ignore at the client site would have no effect on
+whether the Precondition is checked, so it in fact could be used in this way.
+
+The net effect is that Dynamic_Predicates could not be used to define checking
+for parameters [without repeating the checks in the body]. And that is 90% of
+the uses I envison for them (these are very similar to null exclusions in that
+way, 90% of uses being associated with parameters).
+
+At least if the effect is erroneousness, we don't have to care whether the body
+works or not. And as Robert says, most users will understand that. (I'd prefer
+to avoid erroneousness; indeed, I tend to recheck parameters that may be called
+from client code where we don't control the checking specifically to avoid
+erroneous execution, but I realize I'm unusual here.)
+
+Note that if we *don't* use the predicate, and just check the rules in the body,
+we don't have any possible erroneousness nor incorrectness. Nor do tools get a
+chance to do verification or remove the extra error path from the code.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 5, 2012  9:52 PM
+
+...
+> I would recommend a straw vote at this point to see which way most
+> folks are leaning:
+>
+> 1) Assertion_Policy applies to subtype predicates, based on the last
+> explicit predicate aspect clause, and the effect is that the
+> predicates are not checked on conversion, etc., but are still relevant
+> for membership tests, full case-statement coverage, etc.
+>
+>    or
+>
+> 2) Suppress(Predicate_Check) applies to predicates, and it is
+> erroneous if the check would have returned False at the point of a
+> suppressed check.
+>
+> Personally, I am on the fence between these two.
+
+I prefer (1), for the reasons outlined in my previous messages: (1) I'd rather
+not add more erroneous execution to the language, and without it, predicates
+can't be used to check "semantics"; and (2) I don't want to rewrite all of the
+11.4.1 stuff to exclude predicates from "assertions" but then apply all of the
+side-effect and protected operation rules to them. [Note that static predicates
+really don't have issue (2), but it would be even messier to separate static and
+dynamic predicates here.]
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Monday, March 5, 2012  10:06 PM
+
+...
+> > Since assertions (general name) are the most important thing about
+> > Ada 2012, it appears that we have two unappealing choices:
+>
+> > (1) Go forward with rules we *know* are wrong, assuming implementers
+> > will clean up the mess (with the complete loss of portability that
+> > entails)
+>
+> No I don't see the problem as nearly so intractable, and in fact I
+> think the details that we are discussing now are pretty unimportant
+> details. It is a common phenomenon that language lawyers regard
+> problems of no great importance as significant :-)
+
+You might be right in terms of the language design. But these are very important
+details - get them wrong, and I (and many other programmers) will not be able to
+use Dynamic_Predicates for a substantial fraction of their intended purpose.
+That's very bad.
+
+Moreover, even if we agree we want Suppression rules, I don't know how to
+(re)word the rules in 11.4.1 that assume that predicates are "assertions". We
+had so much trouble getting them right as it is (and that's assuming that
+they're right now, probably a dubious assumption), redoing them is a very scary
+task.
+
+And the Standard is promised for delivery ASAP after March 1st (which has
+already passed). Most likely, that will be sometime next week. This wording all
+has to be done and letter balloted by then. That has me *very* scared.
+
+****************************************************************
+
+From: John Barnes
+Sent: Tuesday, March 6, 2012  2:07 AM
+
+I fear that I have not been following this properly (very busy on lectures on
+the fourth dimension), but
+
+...
+>> I agree that the more we talk about them, the more
+>> they resemble subtype constraints, and trying to give
+>> them the same "pampering" we give the other assertion-like
+>> things doesn't seem to be working.
+>
+
+Yes, yes, I felt that when writing that bit of the rat (which will now need
+revising heavily). And do I get Value'First amd Value'Last as well?
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, March 6, 2012  5:14 AM
+
+> I fear that I have not been following this properly (very busy on
+> lectures on the fourth dimension), but
+
+!!
+
+> Yes, yes, I felt that when writing that bit of the rat (which will now
+> need revising heavily). And do I get Value'First amd Value'Last as well?
+
+If there's no predicate, you get 'First.  If Value is static, you get
+Value'First_Valid.  Otherwise (there's a dynamic predicates), you get neither.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, March 6, 2012  7:21 AM
+
+> If there's no predicate, you get 'First.  If Value is static, you get
+> Value'First_Valid.  Otherwise (there's a dynamic predicates), you get
+> neither.
+
+Note that Value'First_Valid can also be used if there is no predicate, providing
+there is at least one value (not a null subtype!)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Tuesday, March 6, 2012  6:00 AM
+
+> You might be right in terms of the language design. But these are very
+> important details - get them wrong, and I (and many other programmers)
+> will not be able to use Dynamic_Predicates for a substantial fraction
+> of their intended purpose. That's very bad.
+
+Randy, this is is just over-the-top pessimistic!
+
+I'm quite sure we WILL get these rules wrong.  So what?
+We'll work it out over the next couple of years.
+Implementers will do what their customers need, and ARG will adjust the rules
+accordingly.
+
+> Moreover, even if we agree we want Suppression rules, I don't know how
+> to (re)word the rules in 11.4.1 that assume that predicates are "assertions".
+> We had so much trouble getting them right as it is (and that's
+> assuming that they're right now, probably a dubious assumption),
+> redoing them is a very scary task.
+
+Don't panic.  Steve is going to produce some wording.
+If he gets it wrong, the sky will not fall.
+
+Compiler writers are going to understand one way or another, whether predicates
+go by "erroneous" rules or "ignore" rules. It really doesn't matter whether or
+not the wording says they are "assertions".
+
+> And the Standard is promised for delivery ASAP after March 1st (which
+> has already passed). Most likely, that will be sometime next week.
+> This wording all has to be done and letter balloted by then. That has me
+> *very* scared.
+
+Take some advice from Alfred E. Newman.  ;-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, March 6, 2012  7:24 AM
+
+> I don't think that works, because it would mean that both (1) you have
+> no control over whether clients make a check or not
+
+I really think it is a waste of time to worry about this. If people turn off
+checks, they get what they get, I think that worrying too much about the status
+of programs with checks that are turned off and fail is pointless.
+
+I copy Yannick on this, because he is in charge of a major project
+(Hi-Lite) that is concerned with mixing tests and proofs, and I think his
+perspective may be useful. Yannick, can you review this thread?
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, March 6, 2012  7:30 AM
+
+> You might be right in terms of the language design. But these are very
+> important details - get them wrong, and I (and many other programmers)
+> will not be able to use Dynamic_Predicates for a substantial fraction
+> of their intended purpose. That's very bad.
+
+You keep saying this, but frankly I don't see "many other programmers"
+here, and I don't sympathize with your concerns, since I think they are
+misplaced. You are trying to push the language into a "Randy Brukardt" mold here
+when it just doesn't fit, and doesn't fit with normal Ada usage.
+
+> Moreover, even if we agree we want Suppression rules, I don't know how
+> to (re)word the rules in 11.4.1 that assume that predicates are "assertions".
+> We had so much trouble getting them right as it is (and that's
+> assuming that they're right now, probably a dubious assumption),
+> redoing them is a very scary task.
+
+It's such a minor point to me, that I dont really care if the RM gets it 100%
+right.
+
+> And the Standard is promised for delivery ASAP after March 1st (which
+> has already passed). Most likely, that will be sometime next week.
+> This wording all has to be done and letter balloted by then. That has me *very* scared.
+
+We can fix this with a binding interpretation if necessary. The Ada 2012 RM is
+full of errors, I am sure of that, no reason to think we have succeeded in
+producing an error free document where we never succeeded in doing this before.
+
+Just as there is nothing special about a day when you don't know any of the
+remaining bugs in a piece of software, and in practice you release software with
+known bugs, there is nothing special about a problem we know about in the RM
+when we release the RM compared to the myriad problems in the RM that we don't
+know about.
+
+So stop being scared, it is based on this faulty perception that there is some
+merit in passing the Ada 2012 RM on to the next stage on a day when we are not
+aware of any errors!
+
+****************************************************************
+
+From: Brad Moore
+Sent: Tuesday, March 6, 2012  8:16 AM
+
+1) They are like contraints
+or
+2) They are like invariants,
+       (or like preconditions/postconditions that are implicitly applied
+        on all calls involving the subtype)
+
+The initial problem was that our Ada 2005 assertion policy was too course. We
+decided we needed more fine-grained control, which led to our current (almost)
+proposal. We are still saying that we would ideally like to have the ability to
+ensure that checks are enforced in certain situations. That tells me that our
+current proposal isn't fine-grained enough.
+
+I haven't completely thought this through, but...
+
+What if we added another assertion policy identifier, in addition to Check and
+Ignore, call it Force, say.
+
+The idea here is that such an assertion policy cannot be overridden, and it
+requires the checks to be performed (like Check).
+
+You could think of this as setting a Checks_Forced aspect on all subtypes
+covered by the scope of the assertion policy pragma.
+
+Hopefully that would satisfy Randy, and others who share his concerns,
+(including myself), although like Tucker, I'm still on the fence with regard to
+the straw poll. If I had to say which way I am leaning, I will say, option 1.
+
+****************************************************************
+
+From: Jeff Cousins
+Sent: Tuesday, March 6, 2012  8:34 AM
+
+Could this Force assertion policy also be used to force the checking of
+constraints on subtypes, or, if we're keeping the model of different but
+parallel systems of control for constraints and assertions, invent an
+Unsuppressable aspect to force the checking of constraints on subtypes?
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Tuesday, March 6, 2012  8:38 AM
+
+> What if we added another assertion policy identifier, in addition to
+> Check and Ignore, call it Force, say.
+
+I would not rush to add this to the RM. If such an assertion policy identifier
+is useful, then implementations can add it.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent