CVS difference for ai05s/ai05-0146-1.txt
--- ai05s/ai05-0146-1.txt 2010/11/13 06:56:45 1.12
+++ ai05s/ai05-0146-1.txt 2011/01/31 04:22:20 1.13
@@ -89,7 +89,7 @@
private_extension_declaration.
Type_Invariant'Class
This aspect shall be specified by an expression, called an *invariant
- expression*.
+ expression*.
Type_Invariant'Class may be specified on a private_type_declaration or a
private_extension_declaration.
@@ -225,7 +225,7 @@
holes can only be created by the package itself (by passing out
access-to-subprogram values); a client cannot create them on their own. Thus
we don't require herculean efforts to catch all possible ways a value
-might be updated and then become externally accessible.
+might be updated and then become externally accessible.
Assertion Policy
@@ -1942,6 +1942,831 @@
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.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Sunday, June 13, 2010 9:11 PM
+
+> I disagree, ...
+
+I know. ;-)
+
+>...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".
+
+And I think ``far from "invariant"'' is hyperbole. Invariants (and predicates)
+are ALMOST ALWAYS true. Yes, acc-to-subp and other stuff can cause trouble, but
+that doesn't amount to "far from". If you violate an invariant, it is HIGHLY
+LIKELY that you'll get an exception pretty soon after.
+
+> 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!
+
+No, not only in erroneous programs. Example:
+
+ procedure P(X : Natural) is
+ begin
+ Put_Line(Natural'Image(X));
+ end P;
+
+The above can print "-1". All it takes is an uninit var:
+
+ Uninit : Natural;
+
+ P(Uninit);
+
+It's a programming error, but it's not erroneous.
+
+The fact that the language does not require this programming error to be
+detected is NOT a good argument against having constraints.
+
+You're trying to use an analogous (bogus, IMHO) argument against invariants.
+It's true that if you hand out (to clients) pointers to components of your
+private type, those clients can "sneakily" violate the invariant by assigning
+via such pointers. The current situation is that the invariant is expressed as
+a comment, and there's zero chance that such "sneaking" will be detected by run
+time checks. With variants, on the other hand, there's a pretty good (not 100%)
+chance that the sneaking will be caught.
+
+In other words, I'm asking you to consider these features as compared to what we
+have without them (mainly, comments), rather than comparing them to some ideal
+features that we don't know how to design in the context of Ada.
+
+> ...
+> > 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".
+
+I was specifically talking about invariants and predicates.
+Those features are placed once, one the relevant [sub]type decl.
+To do it by hand, you have to "sprinkle" on every call, return, and (for
+predicates) a lot of places like assignments and initializations. That sounds
+like hundreds or thousands of places, to me.
+
+>... 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.)
+
+No, predicates are not like null exclusions in that regard.
+
+The reason null exclusions are primarily useful on parameters and function
+results is a because of a design mistake in Ada 83: for access types, there is
+no distinction between "uninitialized" and "null". For ex., that means you
+can't declare a not-null local variable, and initialize it later. Constraints
+and predicates are different: you CAN declare a local variable with a
+constraint, and initialize it later. Similarly, null exclusions don't work very
+well for components, but constraints and predicate do.
+
+Anyway, even if we're talking only about parameters and function results, that's
+still a lot of sprinkling.
+
+Here's one data point: I just did some searching, and found over 4000 parameters
+and results of type Node_Id in the GNAT sources. My search method
+underestimates -- it could easily be twice that. And I'm sure that well over
+99% of those will not operate properly on ALL Node_Ids -- they're retricted to
+Node_Id's for statements, or for just assignment statements, or some other
+predicate.
+
+Adding local variables of type Node_Id into the mix, I'd guess we're talking
+about tens of thousands of "sprinkles". Approx. 100 subtype predicates could do
+all that sprinkling automatically.
+
+> 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.
+
+"Hardly anyone"? Bah. I'm sure I could teach average-competence Ada
+programmers to use invariants and predicates properly. (Don't try to get me to
+teach average-competence Ada programmers to use coextensions properly! Or even
+tasking, for that matter.)
+
+****************************************************************
+
+From: Robert Dewar
+Sent: Sunday, June 13, 2010 9:17 PM
+
+I entirely agree with Bob here, I was about to write my own message, and then
+read Bob's and it said everything I wanted to say.
+
+I don't understand (or sympathize) with Randy's position at all here, it seeems
+to be based on a very personal and peculiar idea of what the term invariant
+means in this context.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Tuesday, June 14, 2010 2:11 PM
+
+...
+> 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.
+
+I basically agree with this. Also just as an observation, the fact that pragma
+Asserts started showing up in Ada code (and Java and C, for that matter) was a
+big help to static analysis, even if their semantics were defined dynamically in
+the language definition. The reason pragma Assert didn't make it into Ada 95
+was largely because of claims that:
+
+ 1) Folks not using static analysis have no use
+ for them
+ 2) Folks using static analysis need something much
+ for sophisticated.
+
+(1) is demonstrably false, at least based on my experience.
+(2) is also demonstrably false in my experience,
+ but in Ada 2012 we are also addressing the issue
+ of sophistication, by at least considering the
+ addition of conditional expressions and quantified
+ expressions.
+
+...
+>> 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.
+
+Fair enough. I will drop it or try to find a better analogy.
+
+...
+> 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.
+
+Subtype predicates also work on subp's invented tomorrow.
+But as far as the "contract" for a private type, I think the "type invariant" is
+more directly relevant.
+
+If we always say "subtype predicate" and "type invariant"
+(or even "private type invariant") in our discussion, hopefully we can do a
+better job of keeping these things apart. They really *aren't* the same thing,
+though I think we could describe the semantics of "private type invariants" in
+terms of "subtype predicates." (It would clearly not be possible to describe
+the semantics of subtype predicates in terms of type invariants!)
+
+Whether we want to eliminate type invariants and make a subtype predicate, when
+applied to a partial view, have the special property of applying to *only* the
+partial view "subtype" along the lines specified for "private type invariants,"
+I could go either way. Alternatively, we could keep the "Invariant =>" (or
+"Type_Invariant =>") syntax, but describe its semantics in terms of "Predicate
+=>" (or "Subtype_Predicate =>"), and do the checks at the same points as we do
+for subtype predicates, that might be a way of reducing the amount of "bulk" in
+the manual.
+
+>> 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.
+
+I don't agree. A private type invariant depends on having a well-defined
+default-initialized state, unless of course the programmer has eliminated the
+possibility of having default-initialized objects, by declaring the partial view
+with "(<>)" unknown discriminants.
+
+> 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.
+
+This doesn't seem logically necessary, but in the interests of being able to
+define the semantics of private-type invariants in terms of subtype predicates,
+I could see the advantage. Adding them to all operations with "in" parameters
+is clearly a dramatic increase in the number of checks required. Here is a case
+where I might make it implementation defined, or perhaps some separate assertion
+policy, which controls such things. Perhaps we need at this point to add at
+least one more language-defined policy, which would be "Minimal_Checks" vs.
+"Full_Checks" or something like that.
+
+...
+>> 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.
+
+It is important for a "call" to know exactly where the exception is raised. For
+the other two I agree this is redundant. We actually go on to say more about
+the "call" so perhaps there is no need to say "at the point" in this sentence,
+if we believe it is covered later for calls.
+
+
+>> 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).
+
+How can type conversion require multiple ones?
+
+...
+>> ...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?
+
+Everyone loves equivalences! ;-) It is also dangerous when writing an AI to
+depend on the semantics of some other AI. But if we believe preconditions and
+postconditions are a slam dunk, then describing some of these as
+preconditions/postconditions would seem to save on wording "bulk."
+
+>> 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.)
+
+Can you elaborate on this contradiction?
+
+...
+>> 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.
+
+As suggested above, I am beginning to think we might need an additional checking
+policy, perhaps just to get a "some-but-not-all" policy identifier into the
+standard, even if the implementation defines some of the details of such an
+intermediate policy. Yes of course implementations can define as many policies
+as they want, but it would be nice to have a portable identifier for an
+"intermediate" level of checking, so you could move source code across Ada
+compilers without having to always change policy identifiers.
+
+...
+>> 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).
+
+Now I am contradicting myself, thinking that there is a useful intermediate
+point. The biggest difference would be eliminating the check on "in"
+parameters, given that there are *many* more calls with an "in" parameter than
+with in-out or out. Also, checks on "out"/"in-out" parameters are easier to
+eliminate when included "inside" the body. Checks on "in" parameters are
+essentially impossible to eliminate if the code is inside the body.
+
+>> !appendix
+>> ...
+>
+> Best not to include the !appendix in emails. ;-)
+
+Agreed. Sorry about that.
+
+****************************************************************
+
+From: Robert A Duff
+Sent: Monday, June 14, 2010 10:03 PM
+
+> > 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.
+>
+> Subtype predicates also work on subp's invented tomorrow.
+
+Yes. Are you saying the above "Invariants can help..."
+is intended to contrast invariants with predicates?
+I didn't get that. Still don't, really.
+
+> But as far as the "contract" for a private type, I think the "type
+> invariant" is more directly relevant.
+
+More than what?
+
+> If we always say "subtype predicate" and "type invariant"
+> (or even "private type invariant") in our discussion, hopefully we can
+> do a better job of keeping these things apart.
+> They really *aren't* the same thing, ...
+
+Well, they have something in common, and some differences, and if we try to emphasize the commonality, Randy will snap. ;-) So I"ve pretty much given up on that.
+
+>...though I think
+> we could describe the semantics of "private type invariants"
+> in terms of "subtype predicates."
+
+Probably, but I'm not sure it helps, and anyway, Randy will snap.
+
+>...(It would clearly not
+> be possible to describe the semantics of subtype predicates in terms
+>of type invariants!)
+
+Agreed.
+
+> Whether we want to eliminate type invariants and make a subtype
+> predicate, when applied to a partial view, have the special property
+> of applying to *only* the partial view "subtype" along the lines
+> specified for "private type invariants,"
+
+At this point, I think that would be unwise.
+
+> I could go either way. Alternatively, we could keep the "Invariant
+> =>" (or "Type_Invariant =>") syntax, but describe its semantics in
+> terms of "Predicate =>"
+> (or "Subtype_Predicate =>"), and do the checks at the same points as
+> we do for subtype predicates, that might be a way of reducing the
+> amount of "bulk"
+> in the manual.
+
+Hmm... Maybe.
+
+I'm inclined to keep invariants and predicates (OK, type invariants and subtype
+predicates) separate, even though they have much in common.
+
+> >> !wording
+...
+> I don't agree. A private type invariant depends on having a
+> well-defined default-initialized state, unless of course the
+> programmer has eliminated the possibility of having
+> default-initialized objects, by declaring the partial view with "(<>)"
+> unknown discriminants.
+
+Well, I can live with your view, but I'm not sure it's best.
+Currently, SOME private types (with invariants expressed as comments) allow:
+
+ X : Priv_Type;
+ ...
+ (later)
+ X := Blah (...);
+
+It's a language flaw that you can't tell from the private type decl whether it
+has a meaningful default, and I'm not sure what to do about that.
+
+> > 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.
+>
+> This doesn't seem logically necessary, but in the interests of being
+> able to define the semantics of private-type invariants in terms of
+> subtype predicates, I could see the advantage.
+
+I'm thinking purely from a practical point of view -- it's useful to catch
+"sneaky" violations of the invariant that happen outside the package. I mean,
+catch them as soon as you enter the package.
+
+>...Adding them to all operations with "in" parameters is clearly a
+>dramatic increase in the number of checks required.
+> Here is a case where I might make it implementation defined, or
+>perhaps some separate assertion policy, which controls such things.
+>Perhaps we need at this point to add at least one more
+>language-defined policy, which would be "Minimal_Checks" vs.
+>"Full_Checks"
+> or something like that.
+
+Not impl-def, please. I could live with another policy.
+I could also live with not checking 'in's -- then an impl can do it, with an
+impl-def policy. Or I could live with checking 'in's, and an impl can have the
+other impl-def policy. But if the policy in use is language defined, we
+shouldn't be too loose.
+
+...
+> >> 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.
+>
+> It is important for a "call" to know exactly where the exception is
+> raised. For the other two I agree this is redundant. We actually go
+> on to say more about the "call" so perhaps there is no need to say "at
+> the point"
+> in this sentence, if we believe it is covered later for calls.
+
+I think it's sufficiently covered by "Upon return..." above.
+
+> >> 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).
+>
+> How can type conversion require multiple ones?
+
+What I said below, "or for...".
+
+> >> 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
+
+Here. A type T has its own invariant, plus other invariants from class-wide
+things. You didn't say these all get 'anded', you said they are multiple
+invariants. So T(X) involves checking all those.
+
+This is just a minor wording issue.
+
+...
+> > This seems to contradict the prior rule about where the policy applies.
+> > (I don't care too much what the exact rule is.)
+>
+> Can you elaborate on this contradiction?
+
+I thought before you said the policy that matters is the one that applies to the
+type decl. But here you're saing it's the one that applies to some subprogram.
+
+...
+> > 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.
+>
+> As suggested above, I am beginning to think we might need an
+> additional checking policy, perhaps just to get a "some-but-not-all"
+> policy identifier into the standard, even if the implementation
+> defines some of the details of such an intermediate policy.
+> Yes of course implementations can define as many policies as they
+> want, but it would be nice to have a portable identifier for an
+> "intermediate" level of checking, so you could move source code across
+> Ada compilers without having to always change policy identifiers.
+
+OK, I suppose.
+
+We don't want TOO many policies. Seems like the important ones are the
+extremes.
+
+...
+> > 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).
+>
+> Now I am contradicting myself, thinking that there is a useful
+> intermediate point. The biggest difference would be eliminating the
+> check on "in" parameters, given that there are *many* more calls with
+> an "in" parameter than with in-out or out. Also, checks on
+> "out"/"in-out" parameters are easier to eliminate when included
+> "inside" the body. Checks on "in" parameters are essentially
+> impossible to eliminate if the code is inside the body.
+
+True.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Friday, June 25, 2010 6:01 PM
+
+We agreed to change the name of the aspects to be "Type_Invariant" and
+"Subtype_Predicate".
+We abandoned any attempt to explain the
+semantics of Type_Invariant in terms of
+Subtype_Predicate, as it didn't seem to
+help anyone (except perhaps me ;-).
+
+More specific comments below.
+
+...
+> Yes. Are you saying the above "Invariants can help..."
+> is intended to contrast invariants with predicates?
+> I didn't get that. Still don't, really.
+
+No, I meant no contrast. Both Type_Invariants and Subtype_Predicates apply to
+subprograms invented tomorrow.
+
+>> But as far as the "contract" for a private type, I think the "type
+>> invariant" is more directly relevant.
+>
+> More than what?
+
+A Type_Invariant makes sense for a private type, and helps to express the
+contract between the implementor and the client of the type. A Subtype_Predicate
+doesn't have as much to do with a contract between the implementor and the
+client of the *type*, but rather is used to create distinctions between
+different (named) subsets of values of the same type, and allow a subprogram to
+indicate which of the various named subsets it expects as a parameter.
+
+>> If we always say "subtype predicate" and "type invariant"
+>> (or even "private type invariant") in our discussion, hopefully we
+>> can do a better job of keeping these things apart.
+>> They really *aren't* the same thing, ...
+>
+> Well, they have something in common, and some differences, and if we
+> try to emphasize the commonality, Randy will snap. ;-) So I"ve pretty
+> much given up on that.
+
+So have I.
+
+>
+>> ...though I think
+>> we could describe the semantics of "private type invariants"
+>> in terms of "subtype predicates."
+>
+> Probably, but I'm not sure it helps, and anyway, Randy will snap.
+
+I have given up on that.
+
+...
+>> Whether we want to eliminate type invariants and make a subtype
+>> predicate, when applied to a partial view, have the special property
+>> of applying to *only* the partial view "subtype" along the lines
+>> specified for "private type invariants,"
+>
+> At this point, I think that would be unwise.
+
+Yes, we have proceeded treating them as distinct features, one applies to
+partial views, and one applies to any old named subtype.
+
+>> I could go either way. Alternatively, we could keep the "Invariant
+>> =>" (or "Type_Invariant =>") syntax, but describe its semantics in
+>> terms of "Predicate =>"
+>> (or "Subtype_Predicate =>"), and do the checks at the same points as
+>> we do for subtype predicates, that might be a way of reducing the
+>> amount of "bulk"
+>> in the manual.
+>
+> Hmm... Maybe.
+
+This approach didn't attract any interest.
+
+...
+> Well, I can live with your view, but I'm not sure it's best.
+> Currently, SOME private types (with invariants expressed as comments)
+> allow:
+>
+> X : Priv_Type;
+> ...
+> (later)
+> X := Blah (...);
+>
+> It's a language flaw that you can't tell from the private type decl
+> whether it has a meaningful default, and I'm not sure what to do about
+> that.
+
+That seems pretty error prone, to have a private type whose initial state is
+undefined, but doesn't have unknown discriminants and so any use of the type
+before a full-object assignment is potentially meaningless. Doesn't sounds like
+a very safe "abstraction."
+
+...
+
+I'll have to respond to other parts at a later time...
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, June 26, 2010 9:16 AM
+
+Note that my message you are replying to was sent about a week ago -- it
+apparently got stuck in arg@ada-auth.org for a while.
+
+> We agreed to change the name of the aspects to be "Type_Invariant" and
+> "Subtype_Predicate".
+
+In order to uphold Ada's reputation for useless verbosity? Sigh.
+
+I am strongly opposed to making either of these features harder to use,
+including by making the names longer. I can't think of any example where the
+extra "Type_" or "Subtype_" would enhance readability. I guess the ARG was
+talking along the lines of "people could be confused between these two
+rather-similar features" (which is true!), and came up with an ineffectual
+non-solution.
+
+I'm happy to call them "type invariants" and "subtype predicates" in the RM, but
+to require all programs to echo that all over the place seems ridiculous.
+
+I hope we keep "Pre" and "Post, rather than "Precondition"
+and "Postcondition" (or "Require" and "Ensure").
+Or should it be "Subprogram_Precondition"?
+Oops, that's not right, it has to be
+"Callable_Entity_Precondition", to allow for entries.
+
+> We abandoned any attempt to explain the semantics of Type_Invariant in
+> terms of Subtype_Predicate, as it didn't seem to help anyone (except
+> perhaps me ;-).
+
+I don't think your viewpoint is wrong -- I just don't think it's for this
+language, at this time.
+
+[...snipping various points of agreement]
+
+> > Well, I can live with your view, but I'm not sure it's best.
+> > Currently, SOME private types (with invariants expressed as
+> > comments) allow:
+> >
+> > X : Priv_Type;
+> > ...
+> > (later)
+> > X := Blah (...);
+> >
+> > It's a language flaw that you can't tell from the private type decl
+> > whether it has a meaningful default, and I'm not sure what to do
+> > about that.
+>
+> That seems pretty error prone, to have a private type whose initial
+> state is undefined, but doesn't have unknown discriminants and so any
+> use of the type before a full-object assignment is potentially
+> meaningless. Doesn't sounds like a very safe "abstraction."
+
+You're right, it's error prone and unsafe. But that has nothing to do with type
+invariants (and only a little to do with private types).
+
+You need to think about unintended consequences. If you make airplanes safer,
+and that costs some money, so ticket prices go up, that's a good thing, right?
+It saves lives! No, it's wrong -- it will cause more people to drive cars more
+often, so the number of unnecessary deaths and injuries will go up.
+
+Suppose I need/want to do the above thing (see "(later)" above), You are
+proposing that I'm not allowed to do that if I use an invariant. So I have two
+choices:
+
+ 1. Express my invariant in a comment, the old-fashioned way.
+ That's even less safe.
+
+ 2. Provide a useless init on X. Again, less safe.
+
+ 3. Provide a bogus default value for Priv_Type. (The extreme
+ of this strategy is Jave, where EVERY variable gets a
+ possibly-bogus initial value. I know you don't like that
+ rule -- so why require it for the new types-with-invariants
+ feature.)
+
+We can live with these problems, but if you think they make the language
+net-safer, you're wrong, IMHO.
+
+Note that 2 and 3 introduce inefficiency, as well as unsafety.
+2 and 3 also probably defeat useful compiler warnings, which currently
+(partially) address the problems you're worried about.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, June 26, 2010 9:16 AM
+
+> > X : Priv_Type;
+> > ...
+> > (later)
+> > X := Blah (...);
+
+Actually, thinking about this a little more, it seems even worse than what I
+said before. In particular, for private types whose full type is scalar.
+Here's some code that comes from CodePeer's arbitrary-range arithmetic package,
+somewhat simplified:
+
+ package Bignums is
+ type Big_Int is private; -- no default initial value
+ ...
+ private
+ type Big_Int is range ...;
+ end Bignums;
+
+Big_Int is an index into some sort of table (I'm oversimplifying!).
+
+You're saying (I think) that if Big_Int has an invariant, then:
+
+ X : Big_Int;
+ ...
+ X := To_Big_Int (1);
+
+It is implementation dependent whether or not this raises Assertion_Failure. X
+is initialized to some arbitrary stack junk, so the invariant will fail if that
+junk happens to represent a "bad" value.
+
+That seems like a totally unacceptable non-portability.
+
+Without an invariant, the above is completely correct and portable. Surely we
+don't want "adding an invariant" to sprinkle arbitrary and impl-dep exceptions
+all over the place!
+
+We could make it illegal for any type with an invariant to lack some sort of
+default (thus forbidding scalars), but that seems like overkill, and doesn't
+even fully solve the problem. I could live with it, though -- it's far better
+than applying invariants to arbitrary stack junk!
+
+Note that when I wrote the Big_Int code some years ago, I tried to use a default
+value, which in full-checking mode would raise an exception on use of an
+uninitialized Big_Int. This turned out to cause an intolerable amount of cruft
+inside the package. It might not seem like a big deal to wrap the thing in a
+record, with a default for the component, but it meant every operation has to
+grab the components out, and then rewrap using an aggregate. That hugely damaged
+the readability of the code, so I gave up. We're talking about thousands of
+lines of code in the package (including children).
+
+I suggest you do an experiment:
+
+ type Big_Int(<>) is private;
+ ^^^^
+and see how many errors you get in clients. (I don't know how to build
+CodePeer, and I don't want to learn how, so I'm not going to do the experiment.)
+
+Note that I advocate checking invariants on 'in' parameters (on the way in). I
+think the above discussion is another argument in favor of that view (if you are
+now convinced that checking invariants on uninit vars is a bad idea).
+
+Summary: My first choice is as I said before -- check invariants on object decls
+if the type has some default init, or the object is explicitly initialized,
+otherwise don't check. My second choice is to forbid invariants on a type that
+has no default init and no (<>) discrim. The third choice (which seems
+unaccepable) is to check on all object decls.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Monday, June 28, 2010 9:09 AM
+
+Another possibility might be to allow
+the specification of a default initial
+value for a scalar type, and disallow
+a type_invariant unless such a default
+is specified, for a private type completed by a scalar type. That would provide
+the most safety, I would think.
+
+[This idea eventually led to the proposal in AI05-0228-1. See that
+AI for more e-mail on this topic. - Editor.]
+
+****************************************************************
+
+From: Bob Duff
+Sent: Monday, July 5, 2010 2:18 PM
+
+> Another possibility might be to allow
+> the specification of a default initial value for a scalar type, and
+> disallow a type_invariant unless such a default is specified, for a
+> private type completed by a scalar type. That would provide the most
+> safety, I would think.
+
+I could live with that. I'm not entirely convinced that it adds a whole lot of
+safety, but it's certainly preferable to my "third (unacceptable) choice" below.
+
+If we do that, we should allow a default for access types, for uniformity,
+right?
+
+I suppose if you say:
+
+ subtype T is Integer range 1..10 := 11;
+
+a compiler should warn if an object uses that default (and NOT on the default
+itself, which is deliberately intended to prevent uninit objects).
****************************************************************
Questions? Ask the ACAA Technical Agent