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

--- ai05s/ai05-0146-1.txt	2010/06/11 03:29:51	1.6
+++ ai05s/ai05-0146-1.txt	2010/06/14 01:07:52	1.7
@@ -1050,7 +1050,7 @@
 ****************************************************************
 
 From: Randy Brukardt
-Sent: Monday, June 7, 2010  10:13 PM
+Sent: Thursday, June 10, 2010  10:13 PM
 
 Well, maybe, but it has been all muddled up. The whole idea of an invariant that
 allows change is idiotic, and you've been trying to claim that these things are
@@ -1078,7 +1078,7 @@
 ****************************************************************
 
 From: Randy Brukardt
-Sent: Monday, June 7, 2010  10:27 PM
+Sent: Thursday, June 10, 2010  10:27 PM
 
 ...
 > Having both of these capabilities might be useful, but I don't think
@@ -1105,6 +1105,739 @@
 think there is a problem adding one more to the list. I know we talked about
 killing this one at the meeting in Tucker's office, but didn't have the guts. I
 hope we have them in Spain...
+
+****************************************************************
+
+From: Yannick Moy
+Sent: Friday, June 11, 2010  12:26 AM
+
+>>> Having both of these capabilities might be useful, but I don't think
+>>> the terms "invariant" and "predicate"
+>>> necessarily conjure up the actual distinction, ...
+
+I quickly got used to the terminology, so it does not seem such a problem to me.
+
+The term "invariant" clearly corresponds to properties of the private types that
+should reasonably be expected by a client code of the package ("reasonably",
+because we're not talking proof of programs here, and only proof can ensure
+these invariants are never broken by the package which defines them, through
+pointers, etc.).
+
+The term "predicate" as well corresponds clearly to some property that a
+(sub)type must respect at defined points in the program.
+
+> Well, maybe, but it has been all muddled up. The whole idea of an
+> invariant that allows change is idiotic
+
+No! This is the well accepted definition of an invariant in the program-proof
+research community. So if we are to use their legacy, we should forget about the
+natural language implication that an "invariant" never changes. In proof of
+programs, an invariant breaks or holds at specific points in the program. This
+is perfectly fine.
+
+There are even very interesting "history invariants" that allow capturing some
+of these changes.
+(http://research.microsoft.com/en-us/um/people/leino/papers/krml166.pdf)
+
+> and you've been trying to claim that these things are the same. I
+> suppose that's true, they're both garbage in that both allow the
+> underlying item to violate the "whateverwecallit" some of the time.
+> That's a junk model and is not really any better than sprinkling
+> assertions around.
+
+If you go this way, contracts are also just a way to sprinkle assertions around.
+I think it is a very good model, very easy to understand, and very rich for both
+dynamic and static verification, which already know very well how to use
+assertions.
+
+> The subtype one was supposed to model an Ada constraint, but that
+> falls apart for composite types. I'm not sure what the type one is
+> supposed be, but it sure as heck isn't an invariant.
+
+Again, seeing an invariant as something that always holds is not the right way
+to look at them.
+
+> If we can't describe simply what these things are, we shouldn't have them.
+> Giving them names which don't reflect their real effects is clearly harmful.
+
+"type invariant" and "predicate subtype" don't hold for me the promise that the
+invariant or predicate described will always hold. The AI clearly states when
+these are checked, and that's perfectly fine with me.
+
+> I wanted true user-defined constraints, but Steve has convinced me
+> that those are impossible. That being the case, I'd rather opt for a
+> few additional new constraints (or nothing at all in the worst case),
+> rather than having these ill-defined assertions. These guys aren't
+> very good contracts if they are violated half the time.
+
+If you can state very precisely when they are expected to hold and when not,
+then these guys are very good at expressing contracts. A contract is no more
+than a very precise description of what you promise to do.
+
+> So I propose we reconsider the
+> well-defined constraints of AI-153-2, and dump these guys to the
+> bottom of the sea. After all, the model of constraints in Ada is
+> well-understood, and having new kinds isn't going to wreck any models
+> or provide any false promises. (And it would give Robert what he
+> wants: enumeration set constraints, without much other baggage.)
+
+I think dropping type invariants and predicate subtypes because they do not
+always hold would be a mistake: it would show more our lack of understanding of
+invariants and predicates than a clearly motivated decision.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, June 11, 2010  2:04 AM
+
+...
+> > Well, maybe, but it has been all muddled up. The whole idea of an
+> > invariant that allows change is idiotic
+>
+> No! This is the well accepted definition of an invariant in the
+> program-proof research community. So if we are to use their legacy, we
+> should forget about the natural language implication that an
+> "invariant" never changes. In proof of programs, an invariant breaks
+> or holds at specific points in the program. This is perfectly fine.
+
+I doubt many Ada programmers are members of "the program-proof research
+community". They will find the term misleading, even if it is technically used
+correctly. (And I doubt that, for reasons noted below.)
+
+...
+> > I wanted true user-defined constraints, but Steve has convinced me
+> > that those are impossible. That being the case, I'd rather opt for a
+> > few additional new constraints (or nothing at all in the worst
+> > case), rather than having these ill-defined assertions. These guys
+> > aren't very good contracts if they are violated half the time.
+>
+> If you can state very precisely when they are expected to hold and
+> when not, then these guys are very good at expressing contracts. A
+> contract is no more than a very precise description of what you
+> promise to do.
+
+The problem here is that they can *never* be *expected* to hold. The only time
+they are true is in the instant after they are checked, and that isn't
+particularly useful.
+
+Moreover, I think you may have missed the part of the AI that says that we
+aren't even going to try to check invariants for calls through
+access-to-subprogram values. That means that even in the places where they are
+defined to be checked, they might not be if the program contains any access
+calls -- something that is out of control of the package. That means that a
+package author cannot even have an expectation that the invariants hold at the
+boundary of the package, because all that the client has to do to defeat the
+checking (usually unintentionally) is use an access-to-subprogram. And there is
+no way for the package author to prevent that. Yuck.
+
+> > So I propose we reconsider the
+> > well-defined constraints of AI-153-2, and dump these guys to the
+> > bottom of the sea. After all, the model of constraints in Ada is
+> > well-understood, and having new kinds isn't going to wreck any
+> > models or provide any false promises. (And it would give Robert what
+> > he
+> > wants: enumeration set constraints, without much other baggage.)
+>
+> I think dropping type invariants and predicate subtypes because they
+> do not always hold would be a mistake: it would show more our lack of
+> understanding of invariants and predicates than a clearly motivated
+> decision.
+
+I don't like the idea of adding additional checking models on subtypes if they
+aren't clearly better than the one that is familiar to Ada programmers -
+constraints. So far as I can tell, both invariants and predicates as proposed
+are both more likely to cause trouble, especially with Ada programmers that are
+used to being able to *believe* their constraints. They will never be able to
+trust either of these as written (because there are a lot of holes, that is ways
+to change a value so that it would fail the check, without triggering the
+check), but I would expect that most programmers *would* trust these in the same
+way that they trust constraints. Which will lead to a boatload of frustration,
+and I suspect in many cases to abandoning the feature altogether or greatly
+restricting its use (rather like many organizations do with use clauses).
+
+There is also the problem of having two similar features with different sets of
+insecurities - programmers would have trouble determining when to use one or the
+other, remembering which they are using, and the like.
+
+Finally, the real question is whether Ada needs these features at all. Ada
+already has a powerful constraint system, and some targetted extensions to it
+might provide the majority of the needed functionality (and the rest can be done
+with preconditions and asserts). This is very different than for preconditions,
+where there is little ability in Ada as it stands to do any checking on a call
+(especially for interactions between parameters).
+
+Anyway, food for thought.
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, June 11, 2010  7:10 AM
+
+>> Well, maybe, but it has been all muddled up. The whole idea of an
+>> invariant that allows change is idiotic
+>
+> No! This is the well accepted definition of an invariant in the
+> program-proof research community. So if we are to use their legacy, we
+> should forget about the natural language implication that an
+> "invariant" never changes. In proof of programs, an invariant breaks
+> or holds at specific points in the program. This is perfectly fine.
+
+I strongly agree with Yannick on this point, basically I agree with Yannick's
+entire message.
+
+> I think dropping type invariants and predicate subtypes because they
+> do not always hold would be a mistake: it would show more our lack of
+> understanding of invariants and predicates than a clearly motivated decision.
+
+yes!
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, June 11, 2010  7:08 PM
+
+> I wanted true user-defined constraints, but Steve has convinced me
+> that those are impossible. That being the case, I'd rather opt for a
+> few additional new constraints (or nothing at all in the worst case),
+> rather than having these ill-defined assertions. These guys aren't
+> very good contracts if they are violated half the time. So I propose
+> we reconsider the well-defined constraints of AI-153-2, and dump these
+> guys to the bottom of the sea. After all, the model of constraints in
+> Ada is well-understood, and having new kinds isn't going to wreck any
+> models or provide any false promises. (And it would give Robert what
+> he wants: enumeration set constraints, without much other baggage.)
+
+Right, that's what I really want, I don't see too much use in anything else,
+although I don't mind the generalization. I do mind if the attempt at
+generaliation fails and we lose the important feature :-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Friday, June 11, 2010  7:11 AM
+
+> I doubt many Ada programmers are members of "the program-proof
+> research community". They will find the term misleading, even if it is
+> technically used correctly. (And I doubt that, for reasons noted
+> below.)
+
+You would be surprised, remember that a major motivation of such features is
+precisely to support formal techniques, and lots of Ada programmers are
+interested in such approaches!
+
+****************************************************************
+
+From: Jean-Pierre Rosen
+Sent: Friday, June 11, 2010  7:21 AM
+
+Moreover, DBC is a cornerstone of OO support in OOTiA/DO178C (and if you want to
+learn more about this, you are welcome to register for my tutorial on Monday ;-)
+)
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, June 11, 2010  8:00 AM
+
+> ...
+>>> Well, maybe, but it has been all muddled up. The whole idea of an
+>>> invariant that allows change is idiotic
+>> No! This is the well accepted definition of an invariant in the
+>> program-proof research community. So if we are to use their legacy,
+>> we should forget about the natural language implication that an
+>> "invariant" never changes. In proof of programs, an invariant breaks
+>> or holds at specific points in the program. This is perfectly fine.
+>
+> I doubt many Ada programmers are members of "the program-proof
+> research community". They will find the term misleading, even if it is
+> technically used correctly. (And I doubt that, for reasons noted below.)...
+
+I think you are off base here.  Static analysis is definitely the direction the
+world is heading as the complexity of doing full dynamic analysis grows
+exponentially.  Static analysis is based on program-proof technology.
+Preconditions and postconditions are related to program-proof technology. "Loop
+invariants" are expressions that are true at a particularly point in the loop.
+They are "invariant" because they are true each time the program passes through
+the point where the invariant holds.
+
+So what "invariant" means is something that is *always* true at particular
+*points* in the execution. There are many interesting invariants that involve
+relationships between multiple objects, or multiple components of the same
+object.  These clearly can't be true at every point in the program, since you
+generally can't simultaneously change multiple objects.  For example, you might
+have an invariant that X.A = X.B + X.C.  Well clearly, you couldn't change any
+of these and keep the invariant true.  But if the invariant is only specified to
+hold at certain places, then so long as compensating changes to X.A, X.B, and
+X.C are made between such places, the invariant is useful.
+
+Subtype predicates/constraints work in part because there is an underlying type
+without any predicate/ constraint.  That's why in Ada you can have a restricted
+subtype like 0..10, but you can still do arithmetic where the intermediate
+values are negative values, or greater than 10.  Similarly you can have an array
+subtype of String(1..10) but still do slicing and concatenation that temporarily
+violates the constraint.
+
+My observation that a private type invariant, where the invariant only holds
+outside the package, is similar to having two different subtype predicates, one
+for outside the package, and one for inside.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, June 12, 2010  7:16 PM
+
+...
+> I think you are off base here. ...
+
+Fair enough. No point in arguing it, but at least you hopefully understand where
+I'm coming from.
+
+...
+> Subtype predicates/constraints work in part because there is an
+> underlying type without any predicate/ constraint.  That's why in Ada
+> you can have a restricted subtype like 0..10, but you can still do
+> arithmetic where the intermediate values are negative values, or
+> greater than 10.  Similarly you can have an array subtype of
+> String(1..10) but still do slicing and concatenation that temporarily
+> violates the constraint.
+
+Right.
+
+> My observation that a private type invariant, where the invariant only
+> holds outside the package, is similar to having two different subtype
+> predicates, one for outside the package, and one for inside.
+
+I suppose the model works, but I still think that is way too confusing. Ada
+constraints work because you always know exactly what constraint holds at a
+given point -- it is the one that belongs to the subtype of the entity, no
+matter what. It doesn't depend on visibility or location or anything else. If
+you start bringing visibility and location into it, even for this limited case,
+it will mean that it will be very hard (and confusing) to determine what applies
+
+I can live with the idea of type invariants, but please don't confuse the
+existing constraint model to cram them into it -- they're something different. I
+can live with the model of checks as outlined in the current AI, but those have
+nothing whatsoever to do with constraint model of Ada.
+
+Still, I think these aren't worth the confusion with predicates. Especially as
+it is possible to use a combination of other features (including predicates) to
+get the effect of these "invariants". So I still want to simplify here: choose
+one or the other, and predicates are more generally useful. So...
+
+Vote NO on 146!  :-)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Saturday, June 12, 2010  7:30 PM
+
+> I suppose the model works, but I still think that is way too
+> confusing. Ada constraints work because you always know exactly what
+> constraint holds at a given point -- it is the one that belongs to the
+> subtype of the entity, no matter what. It doesn't depend on visibility or location or anything else.
+> If you start bringing visibility and location into it, even for this
+> limited case, it will mean that it will be very hard (and confusing)
+> to determine what applies
+
+As you know, I am no friend of complex stuff, but I don't understand the
+possible confusion here, this model seems perfectly clear to me.
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Saturday, June 12, 2010  8:15 PM
+
+By itself, it might be OK. But combined with constraints that hold everywhere
+and predicates that logically hold everywhere, it seems beyond nasty to do
+something different if the aspect happens to occur on a private type. That's
+especially true as the model of aspects in Ada has previously been that the
+aspects are the same for all views of a type -- changing that model seems
+especially dangerous. We don't have any mechanism for changing an aspect
+depending on a view.
+
+As a separate aspect with separate semantics, I can live with (but do not like)
+the semantics of type invariants. I am totally opposed to any attempt to "unify"
+these with predicates, because of the damage that would do to the aspect model
+and to understanding.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Sunday, June 13, 2010  4:26 PM
+
+> Here is an update to AI-146 on Type invariants.
+
+Looks good.  See comments, below.
+
+One general comment, and this AI, and related ones.
+I think it might be a good idea to say something in the AARM about our intent
+with respect to static analysis.
+
+Many "static analysis / proof of (so-called) correctness" folks sneer at the
+idea of run-time checks having anything to do with proofs.  And all these AI's
+do is add some run-time checks.
+
+Points to be made:
+
+    - We expect these run-time checks to feed into tools (could be
+      part of the compiler, could be separate tools) that do
+      static analysis.
+
+    - It's beyond the scope of the Ada language to define such
+      stuff, so we don't say much about it.
+
+    - We freely admit that these features have loopholes.
+
+    - Some tools may want to close the loopholes (e.g.
+      make sure you don't refer to globals in an invariant).
+
+    - Some tools may want to produce conditional proofs (e.g.
+      we don't know X, but we know that IF there are no
+      access types and so on that use the loopholes, then X).
+
+I strongly believe that "static" vs. "dynamic" is not a property of some sort of
+assertion facility, but is a property of the tool doing the analysis.
+
+> !problem
+
+> Note that type invariants are not the same thing as constraints, as
+> invariants apply to all values of a type, while constraints are
+> generally used to identify a subset of the values of a type.
+> Invariants are only meaningful on private types, where there is a
+> clear boundary (the enclosing package) that separates where the
+> invariant applies
+> (outside) and where it need not be satisfied (inside). In some ways,
+> an invariant is more like the range of values specified when declaring
+> a new integer type, ...
+
+I think this is a poor analogy.  I suggest you delete it from the AI.
+The intermediate results being out of bounds doesn't match the crossing of the
+public/private boundary that these invariants talk about.
+
+>...as opposed to the constraint specified when defining  an integer
+>subtype. The specified range of an integer type can be  violated (to
+>some degree) in the middle of an arithmetic computation,  but must be
+>satisfied by the time the value is stored back into an  object of the
+>type.
+>
+> Invariants can help to more accurately define the "contract" between
+> the user and implementor of a package, and thereby to catch errors in
+> usage or implementation earlier in the development cycle. They also
+> can provide valuable documentation of the intended semantics of an
+> abstraction.
+
+Seems to me that the key point is that invariants apply to ALL subp's, including
+the ones invented tomorrow, including the ones in derived (tagged) types, etc.
+That's something that just can't be expressed using pragma Assert, or
+pre/postconditions, or even comments.
+
+> !wording
+
+>   If one or more invariant expressions apply to a type T, and the Assertion_Policy
+>   at the point of the partial view declaration for T is Check, then an
+>   invariant check is performed at the following places, on the specified object(s):
+
+>   * After default initialization of an object of type T, on the new
+> object;
+
+This essentially forces every type with invariants to have a sensible default
+value (or have unknown discrims).  I'm not sure that's wise. Note that we
+decided differently for predicates.  Maybe you should copy that rule.
+
+Also, given the existence of loopholes that Randy likes to pound his shoe on the
+table about, I think 'in' and 'in out' params ought to be checked on the way in.
+
+>   * After conversion to type T, on the result of the conversion;
+>
+>   * Upon return from a call on any subprogram or entry that:
+>       - has a result of type T, or one or more IN OUT or OUT
+>         parameters of type T,
+>       - is explicitly declared within the immediate scope of type T
+>         (or is a part of an instance of a generic unit declared within
+>         the immediate scope of type T), and
+>       - is visible outside the immediate scope of type T or overrides
+>         an operation that is visible outside the immediate scope of T,
+>     on the result object of type T, and on each IN OUT or OUT
+>     actual parameter of type T.
+>
+>   The invariant check consists of the evaluation of each invariant
+>   expression that applies to T, on each of the objects specified above.
+>   If any of these evaluate to False, Ada.Assertions.Assertion_Error is
+>   raised at the point of the object initialization, conversion, or call.
+
+I think "at the point ..." could be removed, without losing any info.
+
+>   If a given call requires more than one evaluation of an invariant
+
+"call" --> "evaluation", or something less specific (because type conv can do
+multiple ones; so can default init).
+
+>   expression, either for multiple objects of a single type or for
+>   multiple types with invariants, ...
+
+or for multiple invariants that apply to a single object of a single type
+
+>...the order of the evaluations is not
+>   specified, and if one of them evaluates to False, it is not specified
+>   whether the others are evaluated. Any invariant check is performed
+>   prior to copying back any by-copy IN OUT or OUT parameters.  It is not
+>   specified whether any constraint checks associated with by-copy IN OUT
+>   or OUT parameters are performed before or after any invariant checks.
+>   It is not specified whether any postcondition checks are performed
+>   before or after any invariant checks.
+
+I wonder if the above could be simplified by saying that an invariant defines a
+bunch of postconditions?
+
+>   The invariant checks performed on a call are determined by the subprogram
+>   or entry actually invoked, whether directly, as part of a dispatching call, or
+>   as part of a call through an access-to-subprogram value.
+>
+>   [Redundant: If the Assertion_Policy in effect at the point of a
+>   subprogram or entry declaration is Ignore, then no invariant check is
+>   performed on a call on that subprogram or entry.]
+
+This seems to contradict the prior rule about where the policy applies.
+(I don't care too much what the exact rule is.)
+
+> !discussion
+
+> Invariant checks apply to all calls on (relevant) subprograms declared
+> in the visible part of the package, even for calls from within the package.
+> This allows the checks to be performed inside the procedures rather
+> than at the call point, and makes the invariants equivalent to a
+> series of postconditions. We considered making invariant checks apply
+> only to calls from outside the package, but this appeared to
+> complicate the implementation and description with little additional
+> benefit.
+
+I agree with this rule, but it might be worth noting that it is different from
+(and simpler than) the Eiffel rule.
+
+My rationale is:
+
+    - implementation of the Eiffel rule is way over complicated
+
+    - the need for it is rare (a semi-educated guess)
+
+    - the workaround is easy (declare another subprogram in the
+      body to skip the inv check, and call that from the exported one).
+
+I don't know if you want to say all that here, but if the ARG agrees with my
+rationale...
+
+> The invariant checks are performed as postcondition checks to ensure
+> that violations are caught as soon as possible. Presumably the
+> invariants could also be enforced as preconditions, but those checks
+> would in general be redundant, and the failures would be harder to
+> track down since the call that actually created the problem would be
+> harder to identify.
+
+I don't buy it.  If an invariant fails on the way 'in', that's a strong clue
+that some client is driving one of their trucks through a loophole. That makes
+it EASIER to track down, whereas if we only check on the way out, we will be
+fooled into thinking it's THIS package's fault.
+
+Eiffel checks on the way 'in', after admitting that there are loopholes.
+Note that the loopholes in Eiffel are worse, because (almost) everything's a
+pointer, so it's easy for a class to accidentally hand out pointers to parts of
+itself.  That loophole exists in Ada, but should be rarer.
+
+Anyway, if I lose this part of the argument, it's no big deal.  I will advocate
+that GNAT turn on such checks via '-gnata'.
+
+> We have adopted a rule that the invariant checks performed are
+> determined by the subprogram invoked, whether directly or indirectly,
+> to match the rule for pre- and postconditions.
+
+Note to Randy: I think you missed this part, given one of your other messages.
+
+> Note that we do not worry about subprograms that have their Access
+> attribute evaluated, even though they might be called from outside the package.
+> We recognize there are holes in the protection provided by type
+> invariants, so we don't require herculean efforts to catch all
+> possible ways a value might be updated and then become externally accessible.
+>
+> Assertion Policy
+>
+> We have used the Assertion_Policy pragma defined in Ada 2005, with the
+> same options and interpretation. It might make sense to define a
+> separate pragma, such as Invariant_Policy, but with the same set of
+> identifiers. This would give the programmer more control. On the other
+> hand, typically either the programmer wants full debugging, or full
+> speed. Intermediate points seem relatively rare, and it seems even
+> more unlikely that the intermediate point would correspond to the
+> distinction between assertions and invariants.
+
+Right.  The useful "intermediate point" is that part of your program is more
+trusted (via testing, or whatever), and some other part is less trusted. We DO
+support that distinction (I think).
+
+> !appendix
+> ...
+
+Best not to include the !appendix in emails.  ;-)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Sunday, June 13, 2010  3:09 PM
+
+I think the following message constitutes unhelpful hyperbole.
+(I say that admitting that I am sometimes guilty of hyperbole myself!  ;-))
+
+Both type invariants and subtype predicates have some loopholes.  That doesn't
+mean they are "idiotic", "garbage", "junk model", "clearly harmful", "violated
+half the time".  That's all just nonsense.  These things are clearly useful.
+
+Note that constraints have loopholes, too.  That's unfortunate, but they're
+still better than nothing.
+
+> Well, maybe, but it has been all muddled up. The whole idea of an
+> invariant that allows change is idiotic, and you've been trying to
+> claim that these things are the same. I suppose that's true, they're
+> both garbage in that both allow the underlying item to violate the
+> "whateverwecallit" some of the time. That's a junk model and is not
+> really any better than sprinkling assertions around.
+>
+> The subtype one was supposed to model an Ada constraint, but that
+> falls apart for composite types. I'm not sure what the type one is
+> supposed be, but it sure as heck isn't an invariant.
+>
+> If we can't describe simply what these things are, we shouldn't have them.
+> Giving them names which don't reflect their real effects is clearly harmful.
+>
+> I wanted true user-defined constraints, but Steve has convinced me
+> that those are impossible. That being the case, I'd rather opt for a
+> few additional new constraints (or nothing at all in the worst case),
+> rather than having these ill-defined assertions. These guys aren't
+> very good contracts if they are violated half the time. So I propose
+> we reconsider the well-defined constraints of AI-153-2, and dump these
+> guys to the bottom of the sea. After all, the model of constraints in
+> Ada is well-understood, and having new kinds isn't going to wreck any
+> models or provide any false promises. (And it would give Robert what
+> he wants: enumeration set constraints, without much other baggage.)
+
+The ides that "sprinkling assertions around" (by hand) is just as good is
+nonsense.  Both predicates and subtype invariants apply in ALL of certain
+well-defined places.  To do that by hand is error prone.  (Think about the
+inheritance of Invariant'Class, for example.  Or just think about adding a
+procedure to a package -- "invariant" applies to all the procedures, including
+the ones invented tomorrow.)
+
+****************************************************************
+
+From: Bob Duff
+Sent: Sunday, June 13, 2010  3:09 PM
+
+> So I still want to
+> simplify here: choose one or the other, and predicates are more
+> generally useful. So...
+
+Well, at least you and I agree that predicates are more generally useful than
+invariants, so if we can't have both...
+
+> Vote NO on 146!  :-)
+
+But I wouldn't go that far (unless these things are too hard to implement.
+That's really my main concern about Ada 2012 -- that it be feasible to
+implement).
+
+> As a separate aspect with separate semantics, I can live with (but do
+> not
+> like) the semantics of type invariants. I am totally opposed to any
+> attempt to "unify" these with predicates, because of the damage that
+> would do to the aspect model and to understanding.
+
+OK, I give up on trying to unify predicates and invariants.  I still think
+they're pretty similar, conceptually, with some minor details that are
+different.  But I won't push that view on the Ada lanugage by trying to unify
+them!
+
+****************************************************************
+
+From: Bob Duff
+Sent: Sunday, June 13, 2010  3:11 PM
+
+> > ...enumeration set
+> > constraints, without much other baggage.)
+>
+> Right, that's what I really want, I don't see too much use in anything
+> else, although I don't mind the generalization. I do mind if the
+> attempt at generaliation fails and we lose the important feature :-)
+
+Robert,
+
+Don't you see the use of having:
+
+    subtype Access_Type_Entity_Id is Entity_Id
+        with Predicate => Ekind (Access_Type_Entity_Id in ...);
+
+    function Get_Designated_Type (E : Access_Type_Entity_Id) return ...;
+
+    ... -- 100 other subprograms that operate on
+        -- Access_Type_Entity_Ids, or return them,
+        -- and 1000 local variables of this subtype.
+
+?
+
+The point is, you're often not dealing DIRECTLY with enumeration values, but
+with records discriminated by those, or (in the case of Entity_Id), a table that
+contains enums somewhere therein, or ....
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, June 13, 2010  6:58 PM
+
+> I think the following message constitutes unhelpful hyperbole.
+> (I say that admitting that I am sometimes guilty of hyperbole myself!
+> ;-))
+>
+> Both type invariants and subtype predicates have some loopholes.  That
+> doesn't mean they are "idiotic", "garbage", "junk model", "clearly
+> harmful", "violated half the time".
+> That's all just nonsense.  These things are clearly useful.
+
+I disagree, especially in the case of "type invariants". The terminology (IMHO,
+not shared by most) promises much more than they actually deliver. In that case,
+I think that they will be far more confusing than helpful. In a vacuum (without
+the existing Ada concepts, and especially without subtype predicates), I
+wouldn't argue that they could be useful. But Ada is not a vacuum!
+
+My biggest concern is really with the terminology, which according to the rest
+of the group has been hijacked to mean something far from "invariant". I'm not
+going to argue about how others are using (or misusing) the terminology, but I
+cannot abide by it myself. If that is "hyperbole", so be it.
+
+> Note that constraints have loopholes, too.  That's unfortunate, but
+> they're still better than nothing.
+
+Only in erroneous programs, for which no reasoning is possible. If there are any
+others, we need to fix them!
+
+...
+> The ides that "sprinkling assertions around" (by hand) is just as good
+> is nonsense.  Both predicates and subtype invariants apply in ALL of
+> certain well-defined places.  To do that by hand is error prone.
+> (Think about the inheritance of Invariant'Class, for example.  Or just
+> think about adding a procedure to a package -- "invariant" applies to
+> all the procedures, including the ones invented tomorrow.)
+
+I really do not understand why you and others keep calling this "sprinkling".
+Generally, there is only a very small number of places where these checks go,
+and they are ones where most Ada programmers are going to explicitly write
+checks no matter what "contracts" exist. For preconditions, there is only *one*
+place where the checks go; that's usually true for postconditions as well
+(although you have to take care when there are multiple exit points). For
+subtype predicates, we are just talking about additional checks on parameters --
+which is the first thing that you would normally write in an subprogram. (I
+don't think subtype predicates will be very useful in other contexts, in this
+sense they are like null exclusions.)
+
+So only type invariants have any sort of "sprinkling" effect. And given that
+hardly anyone will understand them well enough to use them correctly, I'm not
+sure that is really harmful.
 
 ****************************************************************