!standard 7.3.2(6/3) 12-11-29 AI12-0042-1/01 !class binding interpretation 12-11-29 !status work item 12-11-29 !status received 12-04-09 !priority Medium !difficulty Medium !subject Type invariants cannot be inherited by non-private extensions !summary A record extension whose ancestor has a Type_Invariant'Class specified is illegal. !question If a Type_Invariant'Class is specified for a type, which operations of a descendant type must perform the invariant check when the descendant type is not a private type or private extension? !recommendation (See summary.) !wording Add after 7.3.2(6/3): If a Type_Invariant'Class expression applies to any ancestor of a type extension, the extension shall be a private extension or a record extension that is the completion of a private type or extension that has a Type_Invariant'Class that applies. In addition to the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit. !discussion Type invariants were designed assuming that they only apply to private types declared in packages. That is necessary to have any sort of safety associated with them -- if they can apply to non-private types, pretty much anything can cause the invariant to be violated. On the other hand, for private types, nothing a client can do (short of unchecked programming or erroneous execution) can invalidate the invariant. That can only happen within the package, under the control of the package designer. [Truth in advertising - the package designer can introduce holes in rare cases; but these are easily avoided.] It's too early in the life of Ada 2012 to be abandoning the model of type invariants (or any other model, for that matter) [Note: this is being written in November 2012]. Thus, it is best to make the simplest fix that preserves the model. This rule doesn't introduce a generic contract problems, as extensions from generic formal types are prohibited in generic bodies for other reasons (see 3.9.1(4)). The part about completions exists simply so that the completions of private extensions aren't illegal. (It also serves to prevent "hidden class-wide invariants", which would make enforcing the rule problematical.) [Should we define the term "class-wide invariant", it might make this wording a bit easier?] This rule is not incompatible with any existing (Ada 2005 or before) code; it only affects users of Type_Invariant'Class. !ACATS test An ACATS B-Test should be created to test this rule. !appendix From: Tucker Taft Sent: Wednesday, August 1, 2012 6:49 PM Two issues have come up recently at AdaCore relative to Type_Invariant'Class. The first is a bigger issue, and has to do with applying Type_Invariant'Class to an interface type (or some other abstract tagged type). Currently Type_Invariant'Class is not permitted on a type which is not a private type/extension. But it seems pretty useful when defining an interface to establish an invariant which should be satisfied by all types that implement the interface, particularly an invariant that establishes a relationship between multiple operations, such as: type Rectangle is interface with Type_Invariant'Class => Area(Rectangle) = Width(Rectangle) * Height(Rectangle); Quentin Ochem of AdaCore, who first bumped into this issue, will submit an AI on this issue. The second is a more subtle, but related issue. If a Type_Invariant'Class is specified for a type, which operations of a descendant type must perform the invariant check, particularly if the descendant type is *not* a private type or private extension, and perhaps is not even defined inside a package spec? It seems clear that if an invariant based on a Type_Invariant'Class aspect is checked on an operation of the ancestor type, then the corresponding operation of the descendant type should also check the invariant, even if the descendant is not declared in a package spec. Should any additional operations check the invariant? If the type is not declared immediately within the visible part of a package spec, then probably not. However, if it is, then probably the rules of 7.3.2(16-19) should be applied, even if the type is *not* a private type/extension. It would be illegal to define a new Type_Invariant'Class aspect on such a type, but if it inherits a Type_Invariant'Class, we need to define which operations of the type will perform the invariant check. **************************************************************** From: Erhard Ploedereder Sent: Friday, August 3, 2012 10:58 AM > The first is a bigger issue, and has to do with applying > Type_Invariant'Class to an interface type (or some other abstract > tagged type). .... But > it seems pretty useful when defining an > interface to establish an invariant... I wholeheartedly agree. This should be added. > The second is a more subtle, but related issue. If a > Type_Invariant'Class is specified for a type, which operations of a > descendant type must perform the invariant check, particularly if the > descendant type is *not* a private type or private extension, and > perhaps is not even defined inside a package spec? > It seems clear that if an invariant based on a Type_Invariant'Class > aspect is checked on an operation of the ancestor type, then the > corresponding operation of the descendant type should also check the > invariant, even if the descendant is not declared in a package spec. > Should any additional operations check the invariant? Yes, of course. Otherwise the situation is no different from a completely non-private type, since the operations could break the invariant easily. > If the type is not declared immediately within the visible part of a > package spec, then probably not. However, if it is, then probably the > rules of 7.3.2(16-19) should be applied, even if the type is *not* a > private type/extension. It would be illegal to define a new > Type_Invariant'Class aspect on such a type, but if it inherits a > Type_Invariant'Class, we need to define which operations of the type > will perform the invariant check. Too much of a mouthful. Could you put this in terms of examples? My gut answer would have been: all operations need to check, no buts. But you say differently. Why? **************************************************************** From: Steve Baird Sent: Friday, August 3, 2012 12:28 PM > The second is a more subtle, but related issue. If a > Type_Invariant'Class is specified for a type, which operations of a > descendant type must perform the invariant check, particularly if the > descendant type is *not* a private type or private extension, and > perhaps is not even defined inside a package spec? > > It seems clear that if an invariant based on a Type_Invariant'Class > aspect is checked on an operation of the ancestor type, then the > corresponding operation of the descendant type should also check the > invariant, even if the descendant is not declared in a package spec. > Should any additional operations check the invariant? If the type is > not declared immediately within the visible part of a package spec, > then probably not. However, if it is, then probably the rules of > 7.3.2(16-19) should be applied, even if the type is *not* a private > type/extension. It would be illegal to define a new > Type_Invariant'Class aspect on such a type, but if it inherits a > Type_Invariant'Class, we need to define which operations of the type will perform the invariant check. I agree. In the case of a no-partial-view type which is declared in a a package spec, the existing wording is actually ok, although adding a clarifying AARM note seems (very) appropriate. The case where we need a wording change is that of a type which inherits a Type_Invariant'Class and is not declared in a package spec. Certainly we want a predicate check if this type overrides an inherited primitive subprogram.. Erhard raises the question of whether it should also be checked for new (non-overiding) primitive subprograms in this case; this needs to be resolved. But while we've got the hood up on this section of the RM, there is a related issue (although much more of a corner-case) that has been discussed ("discussed" = 2 email messages) internally at AdaCore. AdaCore folks can ignore the rest of this message - you've seen it before. 7.3.2(18/3) says: is visible outside the immediate scope of type T or overrides an operation that is visible outside the immediate scope of T, and I think this may be a case of a rule that really needs to be recursive but instead we only unwind one level of the recursion. I'm thinking about the following (admittedly, somewhat improbable) example: package Type_Invariant_Pkg is type T1 is tagged private with Type_Invariant'Class => Is_Ok (T1); function Is_Ok (X1 : T1) return Boolean; procedure Op (X : in out T1); private type T1 is tagged record F1, F2 : Natural := 0; end record; function Is_Ok (X1 : T1) return Boolean is (X1.F1 <= X1.F2); end Type_Invariant_Pkg; package Type_Invariant_Pkg.Child is type T2 is new T1 with null record; private overriding procedure Op (X : in out T2); type T3 is new T2 with null record; overriding procedure Op (X : in out T3); end; and the question of whether a check is performed upon returning from a call to T3's Op procedure. We want the check to be performed since the call in question might actually (statically) be a dispatching call to Type_Invariant_Pkg.Op. Does the existing wording capture this intent? Now clearly T3's Op procedure is not "visible outside the immediate scope of" T3. So the question is whether it "overrides an operation that is visible outside the immediate scope of" T3. Strictly speaking, this wording may be more fundamentally flawed. In this example, one might think (as the author of the wording seemed to think) that T2's Op procedure overrides T1's Op procedure. Strictly speaking, T2's Op procedure overrides the derived copy of T1's Op procedure and that copy does not have the same visibility as the original. Clearly the wording was intended to refer to the visibility of the original, not of the inherited copy. Let's ignore that issue for now and get back to the original question. What operation(s) does T3's Op procedure override and what is its(their) visibility? The singular/plural uncertainty in the preceding paragraph is actually the crux of the matter. Clearly T3's Op procedure overrides (the inherited copy of) T2's explicitly-declared Op procedure. The subtle point which might make this work is if T3's Op procedure also overrides (the inherited copy of) the inherited (by T2) operator that T2's explicitly declared Op procedure overrode. This (possible) second override (ignoring the issue discussed above that we talk about the visibility of the copy when we really mean that of the original) *is* visible outside of the immediate scope of T3, so we would get the desired behavior if in fact this second overriding occurs here. But I don't think it does. Consider a simpler example: type Pkg1.Aaa declares a primitive procedure Prim. type Pkg2.Bbb is derived from Aaa and explicitly overrides Prim. type Pkg3.Ccc is derived from Bbb and explicitly declares no Prim. Clearly it is ok to call Pkg3.Prim and such a call ends up executing the body of Pkg2.Prim. But if Ccc inherited copies of both the preceding Prims, then 8.3(12.2/2) would apply: If more than one such homograph remains that is not thus overridden, then they are all hidden from all visibility. So clearly Ccc didn't inherit two copies. One could imagine defining things so that two copies are inherited and 8.3 would have a rule that if one op overrides another then an inherited copy of the first overrides an inherited copy of the second, but that doesn't seem to be how things work. Therefore in the example of interest, T3 only inherited one copy and T3's Op only overrides that one copy and we have a problem (arguably a very small one). **************************************************************** From: Steve Baird Sent: Friday, August 3, 2012 12:33 PM >. Erhard raises the question of whether it should also be checked for >new (non-overiding) primitive subprograms in this case; this needs to >be resolved. Oops. I realize now that I don't understand Erhard's point. If a type isn't declared in a package spec, it can't have any new ops. Erhard - can you give an example where your proposal differs from Tuck's? **************************************************************** From: Randy Brukardt Sent: Friday, August 3, 2012 2:12 PM ... > > If the type is not declared immediately within the visible part of a > > package spec, then probably not. However, if it is, then probably > > the rules of 7.3.2(16-19) should be applied, even if the type is > > *not* a private type/extension. It would be illegal to define a new > > Type_Invariant'Class aspect on such a type, but if it inherits a > > Type_Invariant'Class, we need to define which operations of the type > > will perform the invariant check. > > Too much of a mouthful. Could you put this in terms of examples? My > gut answer would have been: all operations need to check, no buts. But > you say differently. Why? The model of type invariants has been that only a limited set of operations get the checks (namely those visible in the package specification). So one would surely expect the set of operations to be limited for any derivations, as well. (Otherwise, implementation could be difficult, as one might need private operations that don't respect the invariants.) Another way to look at it is that we check invariants only when we cross the boundary from the "service" to the "client" -- that is, at the point of the package specification. (This, BTW, is the design we used for shared generics in Ada 83 -- the representation changed if necessary at, and only at, that interface.) It makes sense for overridden primitive operations to get such checks (no matter where they are declared). It *might* make sense for *new* primitive operations to get the checks. It certainly does *not* make sense for non-primitive operations to get the checks (and all operations not declared in package specs are not primitive). I have to admit, I don't think the model of type invariants works very well at all for interfaces, because it brings up all kinds of issues that we purposely avoided thinking about. The model is that the checks are performed only at the public interfaces (including type conversion as a sort of implicit public interface). I think we ought to stick with that model, and that means that only operations that are primitive get the checks (new or old). I think (without reading the wording) that the existing wording should handle that for interfaces: Type_Invariant'Class is inherited by any types that are derived from an interface, and any primitives of that type (inherited or otherwise) would automatically get checks. (If the wording doesn't say that, it's wrong IMHO, irrespective of whether interfaces are involved.) If we want to go beyond that, we're going to have to start over with this aspect, because nothing is defined (or designed) to work on arbitrary subprograms -- there are certainly many gaping holes in the checking in that case. **************************************************************** From: Erhard Ploedereder Sent: Sunday, August 5, 2012 12:48 PM >> . Erhard raises the question of whether it should also be checked for >> new (non-overiding) primitive subprograms in this case; this needs to >> be resolved. > > Oops. I realize now that I don't understand Erhard's point. > If a type isn't declared in a package spec, it can't have any new ops. > > Erhard - can you give an example where your proposal differs from > Tuck's? My argument was not based on an example, but on a principle that I thought was the guiding light on type invariants: "Type invariants are sensible only for private types, because for non-private types they would have to be checked with every modification of instances anywhere in the code - this in turn would not really be manageable, since one needs to allow for temporary inconsistency, but where do you put the bounds for the inconsistency if the type is not private? For private types, visible ops are the bounds and we can guarantee that every call on a primitive operation leaves the invariant intact." In that sense, for a type with type invariants to have additional primitive operations that do not check the invariant, while being able to destroy them, is just as bad as not having privacy in the first place. You could "legitimately" break invariants by using derivation. That does not sound good to me and that was my point. If anyone can convincingly argue that I cannot destroy type invariants in a new op (or else that I cannot have new ops), I am happy. But I have not seen that argument coherently. On the contrary, I believe that private operations will give me the open barn door, since they do not check invariants. (Doing the check in new ops is the conservatively correct route. Not doing the check should be an invisible optimization, figuratively speaking.) **************************************************************** From: Erhard Ploedereder Sent: Sunday, August 5, 2012 1:07 PM PS on my earlier mail.... > Oops. I realize now that I don't understand Erhard's point. > If a type isn't declared in a package spec, it can't have any new ops. I was not interested in the corner cases such as a local type decl as yet, nor in non-primitive ops - surely they are no different from any other procedure. I was interested to cover the cases of ops capable of breaking invariants legitimately. There should not be any where the type invariant is not being checked at the end. **************************************************************** From: Randy Brukardt Sent: Sunday, August 5, 2012 7:39 PM ... > I was interested to cover the cases of ops capable of breaking > invariants legitimately. There should not be any where the type > invariant is not being checked at the end. Could you give an example of the sort of thing you are concerned about? I don't understand how this could happen (since you can't override operations that you can't see, so private operations that don't check invariants can't be visibly overridden). **************************************************************** From: Erhard Ploedereder Sent: Monday, August 6, 2012 7:49 AM You asked for it .... Am 06.08.2012 02:38, schrieb Randy Brukardt: > Erhard Ploedereder writes: > ... >> I was interested to cover the cases of ops capable of breaking >> invariants legitimately. There should not be any where the type >> invariant is not being checked at the end. > > Could you give an example of the sort of thing you are concerned > about? I don't understand how this could happen (since you can't > override operations that you can't see, so private operations that > don't check invariants can't be visibly overridden). > > Randy. > package Carrier is type PT is tagged private; function Invariant(X: PT) return Boolean; procedure Do_AandB(X: out PT); private type PT is tagged record A,B: Integer; end record; procedure Do_A(X: out PT; V: Integer); procedure Do_B(X: out PT; V: Integer); end Carrier; Package body Carrier is procedure Do_AandB(X: out PT) is begin Do_A(X,42); Do_B(X,42); end Do_AandB; function Invariant(X: PT) return Boolean is begin return X.A=X.B; end Invariant; procedure Do_A(X: out PT; V: Integer) is begin X.A := V; end Do_A; procedure Do_B(X: out PT; V: Integer) is begin X.B := V; end do_B; end Carrier; with Carrier; use Carrier; Package Invariants is type T is new PT with null record; with Type_Invariant'Class => Invariant(PT(T)); -- type T introduced by my ignorance about visibility rules inside -- of type invariants; maybe could be on Carrier.PT already, or -- only on I below. The conclusion applies in all cases and -- combinations. end Invariants; package Interf is type I is Interface; -- if you want: with 'Type_Invariant'Class => Invariant(I); -- maybe with the same "carrier detour" because of visibility? function Invariant(X: I) return boolean is abstract; procedure HeHe(X: out I) is abstract; end Interf; with Invariants; with Interf; package Carrier.Next is type NT is new Invariants.T and Interf.I with null record; procedure HeHe(X: out NT); -- newly added op; definitely needs -- to check the invariant, or else.... end Carrier.Next; package body Carrier.Next is procedure HeHe(X: out NT) is begin DO_A(PT(X),666); -- BREAKS THE INVARIANT end Hehe; -- HeHe BETTER RAISE ASSERTION_ERROR end Carrier.Next; **************************************************************** From: Steve Baird Sent: Monday, August 6, 2012 1:48 PM > You asked for it .... > type T is new PT with null record; > with Type_Invariant'Class => Invariant(PT(T)); > package Carrier.Next is > type NT is new Invariants.T and Interf.I with null record; > procedure HeHe(X: out NT); -- newly added op; definitely needs > -- to check the invariant, or else.... > end Carrier.Next; > -- HeHe BETTER RAISE ASSERTION_ERROR For this particular example, I think you get what you want with Tuck's proposal Type_Invariant'Class is specified for T and therefore inherited by NT. HeHe is a primitive op for NT, so the check you want is performed. **************************************************************** From: Erhard Ploedereder Sent: Tuesday, August 7, 2012 6:22 AM I think so, too, but in all the "if"s and "but"s, I lost confidence that it would always be the case. However, can you say the same for all the three variations: - invariant in the class hierarchy (as in the written example) - invariant only on the interface type - invariant on both (Any conformance rules? Do both apply? That becomes tricky, since callers on either side cannot know about the other. But if one is not checked, it can be legitimately broken. ) **************************************************************** From: Steve Baird Sent: Tuesday, August 7, 2012 12:06 PM > However, can you say the same for all the three variations: > - invariant in the class hierarchy (as in the written example) Already discussed. > - invariant only on the interface type Assuming, of course, that the language is extended to allow this construct as has been described in this AI, I think there would be no problem. The op in question would still be a primitive op and subject to an invariant, so the invariant would be checked. So what do we want to do with this example? package Pkg is type Concrete is tagged ... ; procedure Prim (X : Concrete); -- no invariant type Ifc is Interface with Type_Invariant'CLass => ...; procedure Prim (X : Ifc) is abstract; type Ext is new Concrete and Ifc; end Pkg; One option is to disallow this (e.g., by saying that one implicitly declared subprogram cannot override another if the second has type_invariants that the first lacks; this would force an explicit declaration of a Prim procedure for Ext). If, on the other hand, this construct is allowed, then implementations would presumably have to generate a wrapper in this case. > - invariant on both (Any conformance rules? Do both apply? That > becomes tricky, since callers on either side cannot know about > the other. But if one is not checked, it can be legitimately > broken. ) > Discussion of preceding case applies in this case too. No conformance rules - both invariants apply. At the implementation level, callee (as opposed to caller) can perform the check (as you point out, callers don't have enough info). All of this, of course, needs to be confirmed. This is just my guess about how things would work. **************************************************************** From: Randy Brukardt Sent: Thursday, August 9, 2012 6:02 PM ... > package body Carrier.Next is > procedure HeHe(X: out NT) is > begin > DO_A(PT(X),666); -- BREAKS THE INVARIANT > end Hehe; -- HeHe BETTER RAISE ASSERTION_ERROR > end Carrier.Next; Thanks. This is a new operation, that's not likely to be a problem to check. I thought you had some case where an *existing* operation that didn't check the invariant could get called externally via a descendant. (I probably should have realized that that is Steve's job. ;-) **************************************************************** From: Erhard Ploedereder Sent: Friday, August 10, 2012 5:46 AM > This is a new operation, that's not likely to be a problem to check. I > thought you had some case where an *existing* operation that didn't > check the invariant could get called externally via a descendant. (I > probably should have realized that that is Steve's job. Well, wouldn't that be the case if an inherited primitive op came from a parent of the class that implements an interface with that primitive op and the newly introduced invariant? Obviously the inherited implementation would need to be wrappered if the implementation model is that the caller checks. **************************************************************** From: Randy Brukardt Sent: Friday, August 10, 2012 1:34 PM > > This is a new operation, that's not likely to be a problem to check. > > I thought you had some case where an *existing* operation that > > didn't check the invariant could get called externally via a > > descendant. (I probably should have realized that that is Steve's job. > > Well, wouldn't that be the case if an inherited primitive op came from > a parent of the class that implements an interface with that primitive > op and the newly introduced invariant? Steve already asked about that. For preconditions, we require overridding in such a case. Steve thought we might want to do the same for invariants. I'm not sure, either, but I wonder how the inherited routine could conform to such "added" invariants -- if it did so, it would be purely by accident. The implementation of the operation could not know about the invariants. The counter-argument is that the same is true for postconditions, and we don't require overriding for added postconditions. [Added point, 11/29/12: We always have to wrapper inherited routines if a new Type_Invariant or Type_Invariant'Class is added to the derived type, because these added things have to be checked (that's the point of of the AARM note 7.3.2(24.a/3). It doesn't make any sense to care about doing it in similar cases where interfaces or other inheritance is involved.] Anyway, I was wondering about cases where the invariant is not checked now (at all) because the operation is private. If one could inherit such an operation such that it can be called externally, then arguably an invariant would be needed. But that could be a serious problem, as uses in existing internal dispatching calls could be presuming that the invariant is *not* checked - doing so could break the expectations of the design of the base type. But I don't think that can happen; I thought that you had come up with a way to do that, but apparently not. > Obviously the inherited implementation would need to be wrappered if > the implementation model is that the caller checks. Or require overridding so that there never is an inherited operation. Which is better depends on the expectations of the caller and the expectations of the author of the callee. Not sure how to trade that off. **************************************************************** From: Randy Brukardt Sent: Thursday, November 29, 2012 11:34 PM I'm working on old e-mail topics, turning them into AIs for discussion at our upcoming meeting. One topic that had us tied in knots was the issue of what gets checked for a descendant of a type that has Type_Invariant'Class. Tucker originally explained it this way: > If a Type_Invariant'Class is specified for a type, which operations of > a descendant type must perform the invariant check, particularly if > the descendant type is *not* a private type or private extension, and > perhaps is not even defined inside a package spec? This led to all kinds of crazy ideas. The problem is that everything about type invariants was designed with the notion that they only apply to private types declared in packages. That is necessary to have an sort of safety associated with them -- if they can apply to non-private types, pretty much anything can cause the invariant to be violated. OTOH, for private types, nothing a client can do (short of unchecked programming or erroneous execution) can invalidate the invariant. That can only happen within the package, under the control of the package designer. Eliminating this guarantee seems to me to be a horrible idea, and trying to fix up the rules to keep it around is something that I'm not very interested in participating in (given how hard it was to figure out what those rules ought to be for private types). But in thinking about this today, I realized that we've been going about this the wrong way (especially for a fix to Ada 2012). What if we preserved our design decisions? It turns out this leads to a trivial rule that eliminates all of the problems. Add after 7.3.2(6/3): If a Type_Invariant'Class expression applies to any ancestor of a type extension, the extension shall be a private extension. --- A Bairdian grocery list about this idea: (1) This works because we don't allow hidden Type_Extension'Class aspects (they have to be on the private type, not on the full type). Therefore, it is always possible to check this with a compile-time rule. See also (2). (2) For a generic specification, this rule would have to be checked in the instance for any derivations from a generic formal type. (Pretty normal stuff.) There is no problem in a generic body, as extensions from formal types are prohibited in generic bodies in all cases (see 3.9.1(4) and the following AARM notes if you wonder why). So there cannot be a case of allowing something there. (3) This rule has no impact on whether or not we allow invariants on interface types. There can never be any concrete bodies for an interface type (that can be called, null procedures can't be called until inherited); where checks are performed depends on the extension (for which we have fine rules for private types). (4) This rule is best for a "quick fix" to the language, as it could be relaxed in the future without breaking any existing (legal) code. If we try to figure out what ought to happen here in a hurry, we're likely to get it subtly wrong, and be stuck with it forever. (5) It's way too early in the life of Ada 2012 to be abandoning the "private-type-only" (or mostly, if we decide to allow interfaces now). We ought to get several years experience in the use of these things before even considering changing the model around which we designed the Standard. Certainly, we shouldn't go running off and changing stuff simply because the first guy to try it is worried about something. (6) Non-private extensions ought to be rare, so this rule wouldn't bite many people. The only case where those happen with any regularity is the use of them to make up for the missing type-and-operations rename (the problem that integrated packages was intended to solve). That problem should be solved some other way (using derived types in this way is maddening, both for language designers and for users). I have some ideas about that, but those can wait for sometime during the meeting when large quantities of Sam Adams (or a local microbrew) are available. :-) (7) As noted above, I'm not remotely interested in trying to figure out all of the ways that one can get around invariant checking in non-private types. Moreover, I'm not interested in trying to figure out all of the ways that over-zealous checking has broken inherited code (as a "check everywhere rule" would do). This has all of the appeal of a root canal. Given all of the above, I'm going to write this up as described above. If someone else wants to write up an alternative AI with all of the rules that would be needed to support allowing some or all such derivations, they're welcome to do so. (And convince me of the need of doing this now, and not for Ada 2020. IMHO, the only pressing need is to plug the hole.) **************************************************************** From: Randy Brukardt Sent: Friday, November 30, 2012 12:22 AM A follow-on to my previous message: I never actually showed the real wording, as the rule I gave was the "simple" version, which doesn't include the generic boilerplate and also doesn't have a way for the completion of a private extension to be written. In the interest of heading off Steve Baird (fat chance :-), here's what I put into the AI for wording: !wording Add after 7.3.2(6/3): If a Type_Invariant'Class expression applies to any ancestor of a type extension, the extension shall be a private extension or a record extension that is the completion of a private type or extension that has a Type_Invariant'Class that applies. In addition to the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit. --- The only interesting thing about this is the part about the completions. I wrote the rule with the hope of preventing "hidden class-wide invariants", that is where the full type has a class-wide invariant that is not visible through the private type. (This is similar to the way this works for interfaces, except here we only care about the presence or absence of the invariant.) For instance, we would need to prevent something like: package P is type Root is tagged ... with Type_Invariant'Class => ... ... end P; with P; package Q is type Der is tagged private; private type Der is new P.Root with record ... -- Illegal by proposed rule. end Q; There is an easy workaround for a case like this: define a trivial class-wide invariant on the private type. You can construct similar cases for private extensions (where the base ancestor doesn't have an invariant, but the full type's ancestor does). And Steve, I'm aware that there is an obscure hole in these rules if one derives from a untagged formal private type in a generic body -- but I don't care about that at all, as objects of such a type are not considered tagged, and generally can't escape the generic (no dispatching can be involved). And they're pretty much useless. So I don't much care whether or not those are checked. (We could add a run-time check on the declaration of such an extension if someone truly cares, but I don't think it's worth the complication.) **************************************************************** From: Tucker Taft Sent: Friday, November 30, 2012 8:13 AM > ... Add after 7.3.2(6/3): > > If a Type_Invariant'Class expression applies to any ancestor of a type > extension, the extension shall be a private extension. Intriguing idea. I would also allow "null" extensions, as that would address the idiom of using a null extension as a rename. **************************************************************** From: Randy Brukardt Sent: Friday, November 30, 2012 8:51 PM Humm. That would require a bit more wording (to deal with invariants of inherited primitive routines when derived outside of a package spec), but also would eliminate the minor hole associated with the untagged derivation possible in a package body (as it would be treated like a null extension outside of a package specification). It probably also would help with the technical justification for the rule. During the e-mail, Erhard described the model as the following: "Type invariants are sensible only for private types, because for non-private types they would have to be checked with every modification of instances anywhere in the code - this in turn would not really be manageable, since one needs to allow for temporary inconsistency, but where do you put the bounds for the inconsistency if the type is not private? For private types, visible ops are the bounds and we can guarantee that every call on a {visible} primitive operation leaves the invariant intact." [Note: I added "visible" into the above as there certainly can be private primitive operations and they aren't included in the above.] Even though you can't add invariants to a non-private derived type, you still can *change* the behavior of an inherited invariant. That's because class-wide invariants dispatch to the included operations, and an overridden operation can use visible extension components. Moreover, it makes perfect sense for this to happen, and it may be out of the hands of the programmer if the operation is a publicly visible and useful outside of the invariant. [See the example below.] In such a case, there can be no guarantees about the invariant, and that violates the principles given above. OTOH, if there aren't any visible extension components, trouble can happen only if the programmer goes out of their way to allow (by adding some invariant-breaking non-primitive operation in a child unit, for instance). So it makes sense to allow that, and only that. --- Why would an invariant get (implicitly) changed to depend on extension components? Consider the following scenario. We have a widget component in some sort of third-party GUI library, and it includes an invariant that uses the size of the widget. For instance: package Widget is type Root is abstract tagged private with Type_Invariant'Class => ... Size (Root) ...; function Size (W : in Root) return Size_Type is abstract; ... private ... end Widget; Now, our programmer creates their own widget extension, using a record extension: with Widget; package Mine is type My_Widget is new Widget.Root with record My_Size : Size_Type := ...; ... end record; function Size (W : in My_Widget) return Size_Type is (W.My_Size); end Mine; My_Widget will inherit the invariant from Root, that invariant will make a dispatching call to Mine.Size, and Mine.Size returns some visible extension components. Anyone can change those components, and if they do, potentially change the result of the invariant. Moreover, the extender of Widget can't change package Widget (it's a third-party library, remember), they can't avoid overriding Size (it's abstract, and even if it wasn't, it's a useful public function that is useful outside of the invariant -- not changing it is not an option). The only thing they can avoid doing is declaring a non-private type -- and we should *make* them do that in cases like this, as the result otherwise is a swiss cheese form of protection. (Besides, we already have Dynamic_Predicates for cases where near bullet-proof protection is not required.) **************************************************************** From: Tucker Taft Sent: Saturday, December 1, 2012 10:38 AM > ... I would also allow "null" extensions, as >> that would address the idiom of using a null extension as a rename. > > Humm. That would require a bit more wording (to deal with invariants > of inherited primitive routines when derived outside of a package > spec), but also would eliminate the minor hole associated with the > untagged derivation possible in a package body (as it would be treated > like a null extension outside of a package specification). > > It probably also would help with the technical justification for the rule. > During the e-mail, Erhard described the model as the following: ... Allowing null extensions seems quite important, given that we made a big effort to allow them as a stand-in for renaming. **************************************************************** From: Erhard Ploedereder Sent: Saturday, December 1, 2012 4:00 PM > Even though you can't add invariants to a non-private derived type, > you still can *change* the behavior of an inherited invariant. That's > because class-wide invariants dispatch to the included operations, and > an overridden operation can use visible extension components. > Moreover, it makes perfect sense for this to happen, and it may be out > of the hands of the programmer if the operation is a publicly visible and > useful outside of the invariant. > [See the example below.] In such a case, there can be no guarantees > about the invariant, and that violates the principles given above. The principle can also be violated without resorting to extensions. Methods could return a component value of access type. If the type invariant refers to this hidden component, the "exported" reference to its designated object would nevertheless make the invariant susceptable to violations from the outside. I believe the right way to think about it is that - the writer of the invariant must not refer to values that are susceptable to change from the outside by whatever means. Privacy helps tremendously, but is not the entire story. - the deriver from a type must not redefine methods called in the type invariant to make the invariant susceptable to changes from the outside. Now, IF I do not touch indirectly accessible stuff in the invariant AND I am not performing dispatching calls, I am safe behind the curtains of privacy. If I go beyond, I require cooperation from the (re-)definers of the classes involved, in order to stay safe. Unfortunately, to cast this into static rules, is difficult at best and may turn out to be draconic for real OOP. Your example would not be legal, yet I realize that it should be on practical grounds. **************************************************************** From: Randy Brukardt Sent: Saturday, December 1, 2012 4:42 PM > > Even though you can't add invariants to a non-private derived type, > > you still can *change* the behavior of an inherited invariant. > > That's because class-wide invariants dispatch to the included > > operations, and an overridden operation can use visible extension components. > > Moreover, it makes perfect sense for this to happen, and it may be > > out of the hands of the programmer if the operation is a publicly > > visible and useful outside of the invariant. > > [See the example below.] In such a case, there can be no guarantees > > about the invariant, and that violates the principles given above. > > The principle can also be violated without resorting to extensions. > Methods could return a component value of access type. If the type > invariant refers to this hidden component, the "exported" reference to > its designated object would nevertheless make the invariant > susceptable to violations from the outside. Sure, the designer of an abstraction can write one that contains holes. No one has ever doubted that. The thing that bothers me is the case when the extender *introduces* a hole, *by accident*. (And returning an access value is *never* an accident.) > I believe the right way to think about it is that > - the writer of the invariant must not refer to values that are > susceptable to change from the outside by whatever means. Privacy > helps tremendously, but is not the entire story. > - the deriver from a type must not redefine methods called in the > type invariant to make the invariant susceptable to changes from > the outside. But this latter is impossible to follow, because they cannot change the invariant, and they probably cannot change the operations that they need to implement, either. > Now, IF I do not touch indirectly accessible stuff in the invariant > AND I am not performing dispatching calls, I am safe behind the > curtains of privacy. If I go beyond, I require cooperation from the > (re-)definers of the classes involved, in order to stay safe. > Unfortunately, to cast this into static rules, is difficult at best > and may turn out to be draconic for real OOP. Your example would not > be legal, yet I realize that it should be on practical grounds. I don't understand this paragraph. The only proposal is to make non-private non-null extensions of types with invariants illegal. The reason is in part to reduce the chance of inadvertent holes. It certainly won't eliminate all possibilities of holes, but these are major and unavoidable. (You talk about avoiding dispatching in your invariant, but that is impossible with Type_Invariant'Class, in which calls are defined to be dispatching and which is required to be public, so you can *only* make public calls to query properties of your type.) Methodologically, all composite types should be private types in an Ada program. (Pretty much the only exception that I've seen in practice is for tuples of elementary types, like coordinates, sizes of rectangles, and complex numbers. And that's a close call.) Arguably, Ada should never have allowed record extensions that aren't completions of private extensions. Obviously too late for that, but since it clearly causes trouble with this new feature, banning the combination seems OK. The work-around to a type illegal on these grounds is easy: make the type a private extension (and, if necessary wrap it in a package). If that somehow breaks your abstraction, you don't *have* an abstraction! So I don't see why it is necessary to allow such a record extension "on practical grounds". I'd prefer to not allow any such extensions, but Tucker points out the use of null extensions as a stand-in for renames. I absolutely detest this use of derivation (it's wrong on many levels), but given that we haven't created a viable alternative (and we certainly have tried) we probably do have to allow that. But there is very little compelling about the non-null case. Again, in almost all of the above, I'm only talking about extensions from types that have Type_Invariant'Class specified non-trivially. (I don't keep mentioning that repeatedly because otherwise the actual points get lost.) ****************************************************************