!standard 7.3.2(6/3) 14-09-29 AI12-0042-1/11 !standard 7.3.2(17/3) !standard 7.3.2(18/3) !standard 7.3.2(19/3) !standard 7.3.2(20/3) !class binding interpretation 12-11-29 !status Corrigendum 2015 13-12-11 !status WG9 Approved 14-10-20 !status ARG Approved 4-0-5 14-06-28 !status work item 12-12-17 !status ARG Approved 6-0-2 13-11-17 !status work item 12-11-29 !status received 12-04-09 !priority Medium !difficulty Medium !subject Type invariant checking rules !summary If a class-wide invariant applies to an ancestor, then any private operation of the ancestor type that is visible at the point of the extension shall be overridden. In addition, if a type invariant is inherited by a record extension, the type invariant is checked after any operation that corresponds to a visible operation of an ancestor to which this invariant applies. !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 extension occurs at a point where a private operation of some ancestor is visible and inherited, and a Type_Invariant'Class expression applies to that ancestor, then the inherited operation shall be abstract or shall be overridden. Modify 7.3.2(16/3-19/3) as follows: (Note: This includes the changes of AI12-0044-1 as well as this AI) * An invariant is checked upon successful return from a call on any subprogram or entry that: * is declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is 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, and] {* and either:} {*} has a result with a part of type T, or {* has} one or more {OUT or IN OUT} parameters with a part of type T, or {* has} an access{-to-object}[ to variable] parameter whose designated type has a part of type T[.]{, or} {* is a procedure or entry that has an IN parameter with a part of type T,} {* and either: * T is a private type or a private extension, and the subprogram or entry is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T, or * T is a record extension, and the subprogram or entry is a primitive operation visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T.} Add after 7.3.2 (20/3) * For a view conversion to a class-wide type occurring within the immediate scope of T, from a specific type that is a descendant of T (including T itself), a check is performed on the part of the object that is of type T. [AARM Reason: Class-wide objects are treated as though they exist outside the scope of every type, and may be passed across package "boundaries" freely without further invariant checks.] !discussion This AI addresses three issues: 1) If a type extension inherits from some ancestor both a Type_Invariant'Class and a private operation, then we've added a rule that the operation must be either overridden or abstract. The point is that the class-wide Type_Invariant of the ancestor didn't apply to the original operation (because it was a private operation) but it applies to the inherited operation. (An example of such a case is given below.) In such a case, the private operation would not be expected to maintain the invariant (as it is inside the checking boundary). However, the inherited routine would be required to maintain the invariant (as it is now on the checking boundary). We require overriding (or abstractness) in the case of inherited subprograms that have different contracts than the "original" ancestor subprogram when that significantly changes the meaning of the routine (this includes preconditions as well as type invariants). This is just to avoid surprising behavior, not because of any real definitional problem. It also spares implementations from having to generate wrapper routines in this case. 2) In 7.3.2(18/3), the existing wording: is visible outside the immediate scope of type T or overrides an operation that is visible outside the immediate scope of T was wrong in two ways and needed to be fixed up. First, this wording didn't correctly address the case of a record extension. Second, the existing wording talked about overriding operations of a parent type. But a derived type never overrides operations of its parent type - instead, it may override implicitly-declared operations that were inherited from the parent type. 3) Class-wide objects, which could represent a hole in the checking mechanism. We considered the more general issue of invariants that apply to record extensions. This can happen two ways. One is a Type_Invariant'Class inherited into a record extension. Similarly, invariants can be added to private extensions of record types that have visible components. The checking for type invariants was designed to catch virtually all cases where the objects cross the package boundaries. When there are visible components, this model breaks down as the visible components can be modified independently of the package boundaries, which could make the invariant False without detection. Both cases could be prevented with Legality Rules (as we do not allow class-wide invariants to be hidden). We decided it's not worth preventing such things, even with the possibility of misuse. Similarly, there are other holes in the checking represented by type invariants (some of these are explained in AARM 7.3.2(20.a/3)). We do not believe the effort to plug all possible holes is practical. As such, we only plug holes that are likely to occur in practice (like the use of class-wide objects). !example An example of item (1) from the discussion: 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); -- [1] private type T1 is tagged record F1, F2 : Natural := 0; end record; function Is_Ok (X1 : T1) return Boolean is (X1.F1 <= X1.F2); procedure Priv_Op (X : in out T1); -- [2] end Type_Invariant_Pkg; private package Type_Invariant_Pkg.Child is type T2 is new T1 with null record; -- Illegal by this AI. -- Inherits procedure Op (X : in out T2); -- [3] -- Inherits procedure Priv_Op (X : in out T2); -- [4] end; Note that a call on Op [1] will cause the invariant to be checked on return, while a call on Priv_Op [2] would not make such an invariant check. However, a call on either Op [3] or Priv_Op [4] will cause the invariant to be checked on return. It's this change of the check that applies to Priv_Op that makes this illegal. Note that this case is rather unlikely. If the keyword private is erased from Type_Invariant_Pkg.Child, then the error goes away (as Priv_Op [4] would be declared in the private part of Type_Invariant_Pkg.Child and no invariant check would be required). !corrigendum 7.3.2(6/3) @dinsa The Type_Invariant'Class aspect shall not be specified for an untagged type. The Type_Invariant aspect shall not be specified for an abstract type. @dinst If a type extension occurs at a point where a private operation of some ancestor is visible and inherited, and a Type_Invariant'Class expression applies to that ancestor, then the inherited operation shall be abstract or shall be overridden. !corrigendum 7.3.2(17/3) @drepl @xinbull (or by an instance of a generic unit, and the generic is declared within the immediate scope of type @i), and> @dby @xinbull (or by an instance of a generic unit, and the generic is declared within the immediate scope of type @i),> !corrigendum 7.3.2(18/3) @ddel @xinbull or overrides an operation that is visible outside the immediate scope of @i, and> !corrigendum 7.3.2(19/3) @drepl @xinbull, or one or more parameters with a part of type @i, or an access to variable parameter whose designated type has a part of type @i.> @dby @xinbull, or one or more parameters with a part of type @i, or an access to variable parameter whose designated type has a part of type @i;> @xinbull @xi2bull<@i is a private type or a private extension and the subprogram or entry is visible outside the immediate scope of type @i or overrides an inherited operation that is visible outside the immediate scope of @i, or> @xi2bull<@i is a record extension, and the subprogram or entry is a primitive operation visible outside the immediate scope of type @i or overrides an inherited operation that is visible outside the immediate scope of @i.> !corrigendum 7.3.2(20/3) @dinsa @xindent.> @dinst @xbullet, from a specific type that is a descendant of @i (including @i itself), a check is performed on the part of the object that is of type @i.> !ACATS test ACATS B-Tests and C-Tests should be created to test these rules. !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.) **************************************************************** From: Randy Brukardt Sent: Thursday, January 24, 2013 12:20 AM During the ARG meeting discussion about inherited class-wide invariants, I recorded the following: We look in detail at extensions in subprograms. The inherited routines are checked, because the original routines are called in that case (that is the point of the note 7.3.2(24/3). Overridden routines aren't checked by the rules given here. But that should be OK, because an overridden routine cannot violate the original invariant - it has to call something that will check the invariant. Randy is skeptical of this assertion because of dispatching, especially inside an invariant expression. Others would like him to come up with an example off-line, and the discussion moves on. I was wrong that the "hole" is dispatching, but I was right that there is a hole. It's caused by the fact that these extensions can be in bodies (of the base package or its children) -- and then dispatching could make the hole visible outside of the subprogram. I don't think this is a critical problem at all, but since I was asked to provide an example, here goes: (Note: We're assuming that overriding routines don't have their invariants checked, as described above.) package Root is type Safe is tagged private with Type_Invariant'Class => Is_Funny (Safe); function Is_Funny (Obj : in Safe) return Boolean; procedure Public_Proc (Obj : in out Safe); -- Invariant checked here. private type Safe is tagged record Funny : Boolean := True; ... end record; procedure Private_Proc (Obj : in out Safe); -- Invariant not checked for this routine. function Is_Funny (Obj : in Safe) return Boolean is (Obj.Funny); end Root; package body Root is procedure Public_Proc (Obj : in out Safe) is begin Private_Proc (Obj); Obj.Funny := not Obj.Funny; end Public_Proc; procedure Private_Proc (Obj : in out Safe) is begin Obj.Funny := not Obj.Funny; ... end Private_Proc; end Root; package Root.Child is procedure Do_Stuff; end Root.Child; package body Root.Child is procedure Do_Stuff is type Unsafe is new Safe with null record; overriding procedure Public_Proc (Obj : in out Unsafe); overriding procedure Private_Proc (Obj : in out Unsafe); procedure Private_Proc (Obj : in out Unsafe) is begin Private_Proc (Safe(Obj)); end Private_Proc; procedure Public_Proc (Obj : in out Unsafe) is begin ... Private_Proc (Obj); end Public_Proc; begin ... end Do_Stuff; end Root_Child; In this case, calls on the overriding Public_Proc (including dispatching calls), will never check the invariant on the Obj argument. To show how that could cause problems, I could have added another routine in Root that dispatches on Public_Proc, but that would clutter the example. This problem is mitigated somewhat by the obvious fact that you can't put objects of this type into long-lived structures (like a container) as the tag would fail the accessibility check for Safe'Class. So while it is possible for such objects to "leak out" to clients of Root, they can only do it while procedure Do_Stuff is active, so it is not a very significant problem. Note that there is rather weird effect here: if Private_Proc is inherited, the invariant will get checked on it (which it shouldn't, IMHO), but if we override it and do manually exactly the same thing that inheritance would do, we don't get a check. That seems inconsistent irrespective of this whole. Moreover, the entire issue of adding checks to inherited private routines (previously discussed in the context of private children) reappears here. (As previously noted, that could cause (re)dispatching calls in the body of Root to fail, if they are presuming that the invariants don't matter because the routines are private. Claw uses a pattern much like this to hide the workings of the message loop from programmers -- it's not just a thought experiment.) In addition, the same problem would occur if we do a derivation in the private part of a child package, or in the body of the root package or the body of any child. Anyway, more to think about for the stuckee for this AI (that would be Tucker). **************************************************************** From: Tucker Taft Sent: Thursday, January 24, 2013 8:55 AM > We look in detail at extensions in subprograms. The inherited routines > are checked, because the original routines are called in that case > (that is the point of the note 7.3.2(24/3). Overridden routines aren't > checked by the rules given here. But that should be OK, because an > overridden routine cannot violate the original invariant - it has to > call something that will check the invariant. Randy is skeptical of > this assertion because of dispatching, especially inside an invariant > expression. Others would like him to come up with an example off-line, and the discussion moves on. ... The NOTE at 7.3.2(24/3) is talking about *specific* type invariants, not class-wide type invariants. So does that mean the rest of this note is confused? **************************************************************** From: Randy Brukardt Sent: Thursday, January 24, 2013 10:14 AM I'm not 100% sure, but I think this is correct. Inheritance works the same either way (it obviously doesn't depend on invariants); the note was pointing out a particular ramification of the rules for specific type invariants. The same conclusion would be true for class-wide invariants, but it's less interesting because the same class-wide invariant would normally be checked for both the inherited routine and the original routine that it calls. So we probably didn't mention that case. However, in this case, the "new" routine isn't checked, but the original routine is. So that argues that the original premise was correct. OTOH, I could have misunderstood the rules such that I confused the note (and/or the minutes). I wasn't able to convince myself that anything that we "decided" during the meeting was correct (for these derivations, or for visible record types for that matter), so I just took them as a given and constructed an example accordingly. Obviously, any assumptions that I got wrong would mess up the example. (In particular, I can't figure out what impact, if any, the requirement that a subprogram "be visible outside of its scope" would have. No subprogram declared in a subprogram or other body is ever visible outside of its scope, which would imply that nothing is checked anywhere other than in package specifications. I'm pretty certain that would not work, because of dispatching and the like, and in any case, it's not the assumption that we seem to be making.) My example only depends on the idea that only the original routine is checked (not the inherited one) plus the fact that routines declared in private parts are never checked. That's what we decided at the meeting, and the claim (which I say is incorrect) is that it isn't possible to get an object that is not checked to "leak" out (the check must happen somewhere else). If you think there is something specifically wrong with my example, please explain it. And if you now believe that one or more for the assertions made at the meeting are incorrect, please explain *that* so we can discuss it further. **************************************************************** From: Tucker Taft Sent: Sunday, June 9, 2013 3:50 PM I added a new rule that requires a private operation of an ancestor with a class-wide type invariant to be overridden if it is inherited at the point of a private extension. This is because the class-wide invariant starts to apply to such an operation, when it didn't before, and the only way that avoids breaking privacy is if the operation is overridden. [This is version /02 of the AI - Editor.] **************************************************************** From: Steve Baird Sent: Saturday, June 15, 2013 6:24 AM My wording quibbles are orthogonal to the rest of the AI. I think we decided to kill the first paragraph of the wording changes we looked at today and keep the second, but in any case, here are *my* wording changes for this one. In 7.3.2(18/3) replace is visible outside the immediate scope of type T or overrides an operation that is visible outside the immediate scope of T with is dynamically callable (i.e. either directly or via a dispatching call) from outside the immediate scope of T. [In other words, that is visible outside of the immediate scope of T or that overrides an operation inherited from one that is dynamically callable from outside of the immediate scope of T.] Cheating here a little, recursively defining a new term without explicitly saying that that is what I am doing. It seemed the best way. The above addresses two separate issues: 1) Transitivity - we want to deal with overrides of overrides, etc. 2) Given type T2 extends T1, T2's ops never override T1's ops, although they might override ops inherited from T1's ops. [This is part of version /03 of this AI - Editor.] **************************************************************** From: Steve Baird Sent: Sunday, June 16, 2013 4:25 AM > Cheating here a little, recursively defining a new term without > explicitly saying that that is what I am doing. It seemed the best > way. Folks didn't like the cheating (understandably). So here is a more explicit version: In 7.3.2(18/3) replace is visible outside the immediate scope of type T or overrides an operation that is visible outside the immediate scope of T with is *dynamically callable from outside the immediate scope of T*. A subprogram is dynamically callable from outside the immediate scope of T if it is is visible outside of the immediate scope of T or if it overrides an operation inherited from one that is dynamically callable from outside of the immediate scope of T. **************************************************************** From: Tucker Taft Sent: Saturday, November 16, 2013 10:40 PM Here is a rewrite of AI12-0042. [Editor's note: This is version /06 of the AI.] I reorganized a bit, and then handled the case of a private/private-extension type differently from a record extension. **************************************************************** From: Randy Brukardt Sent: Wednesday, December 11, 2013 7:08 PM In working on the minutes for AI12-0042-1, I'm not sure that an issue that I raised was adequately addressed. So let me raise it again here. From the minutes: Randy worries that this definition means that new primitive operations of a record extension are not checked against an inherited class-wide type invariant. If the programmer later derives a private extension from that type, the operation would suddenly get checking. That's similar to the private case where we require overriding. Tucker claims that there is no issue, since there is no privacy breaking going on in this case. The sort of case I had in mind is the following (using an example from the meeting as a starting point): package Pack1 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 Pack1; with Pack1; package Pack2 is type T2 is new Pack1.T1 with null record; -- Record extension. -- Op is inherited here, with checks of Is_OK. procedure Op2 (X : in out T2); -- Does not enforce the invariant. end Pack2; with Pack2; package Pack3 is type T3 is new Pack2.T2 with private; -- Private extension. -- Op is inherited here, with checks of Is_OK. -- Op2 is inherited here, now checking Is_OK to enforce the invariant. private type T3 is new Pack2.T2 with null record; end Pack3; The inheritance of Op2 adds checks not known to the body of the original Op2. Tucker's response of "this is OK because there is no privacy breaking" seems irrelevant, given the discussion in AI12-0042-1. If a private extension inherits from some ancestor both a Type_Invariant'Class and a private operation, then we've added a rule that the operation must be either overridden or abstract. The point is that the class-wide Type_Invariant of the ancestor didn't apply to the original operation (because it was a private operation) but it applies to the inherited operation. As a general rule, we require overriding (or abstractness) in the case of inherited subprograms that have different contracts (this includes pre/post-conditions as well as type_invariants) than the "original" ancestor subprogram. We don't want an implicitly-declared inherited subprogram that performs checks that were not performed by the original subprogram. This is just to avoid surprising behavior, not because of any real definitional problem. It also spares implementations from having to generate wrapper routines. This "general rule" surely would apply to the example I gave, as it has nothing to do with privacy. So either the case I outlined above ought to be covered, or the discussion explaining why we added the rule for private operations is wrong, and we need a different explanation (and maybe a different rule). I'm not sure why privacy should matter (as the original problem can only happen in private child packages, which by definition are part of the private part, and as such they cannot break any privacy). I admit that the discussion is wrong, at least in the sense that we *don't* make such a requirement for class-wide postconditions. We require wrappers in the case that further postconditions are added on inheritance. I'd argue, however, that the general rule is right, and in fact the rules for class-wide postconditions are wrong as well. The reason is that we ought not want to be able to silently add requirements to existing subprograms. For instance, I don't think it is a good idea that a derivation that adds an interface can add requirements (class-wide postconditions in this case) to an existing subprogram. If that existing subprogram was proved to meet its postconditions, adding requirements could require the inherited version to be proved again (and potentially would require modifications to meet those additional requirements). That's especially bad for reusable code (where modifying a body could affect many programs). With rules allowing the adding of requirements, the only way to be certain that a subprogram meets all of its postconditions and invariants is to check the entire program - proof of a part doesn't guarantee anything. (Obviously, this can be made to work, but it effectively weakens contracts.) I'd state the general rule as "Inheritance cannot add requirements (postconditions and invariants) to an existing subprogram; subprograms have to be overridden to add requirements." (I'd suggest that this be a language-design principle, in fact.) I know my view is colored by my opinion that for proof to be generally used, it has to be effective on a per-unit basis. (Which requires strong contracts.) Otherwise, it will be impractical to prove large systems simply because of the combinatorial explosion that results without those strong boundaries. Perhaps there will be some magic that will allow proving million line systems without strong boundaries, but I wouldn't want to wait for that to be found. Anyway, if we don't want the general rule, then we certainly shouldn't explain the overriding rule in terms of it. And honestly, I can't see any good reason to ban this particular case and allow others. They're all bad, or all tolerable. Arguably, this would be a methodological restriction that could be a suppressible error (given that the semantics are well-defined, if surprising, in its absence). Not sure if that makes any sense. Thoughts?? **************************************************************** From: Randy Brukardt Sent: Wednesday, December 11, 2013 7:40 PM ... > So either the case I outlined above ought to be covered, or the > discussion explaining why we added the rule for private operations is > wrong, and we need a different explanation (and maybe a different > rule). I neglected to mention that the easiest fix to preserve the "general rule" in this case is simply to have any inherited type invariants apply to any new visible primitive operations of a record extension as well as any inherited ones. That's what I would have expected in any case (assuming we're allowing record extensions of types that have class-wide invariants). I think the important thing is that any class-wide invariant apply to all visible primitive operations of any extension, regardless of where the primitive operations originate. I find it weird otherwise. (I realize that if the extension is not in a package specification, then any new operations won't be primitive, and the invariant would not apply. But that oddity is well-understood - to the extent that anything about derivation is understood - and the new operations cannot be dispatching operations in that case, so there's no weird mixture of operations.) **************************************************************** From: Tucker Taft Sent: Saturday, December 14, 2013 4:50 PM Your argument is convincing. I would agree that when a class-wide invariant becomes newly relevant to an inherited operation, it should be overridden. An alternative in this case is to make inherited class-wide type invariants apply to *all* visible primitive operations of the descendant type, independent of whether the descendant type is itself a private extension, presuming the type is declared in the visible part of a package. I think that might actually make more sense in this case. We would still only allow you to define a new type invariant on a private type or private extension, but it seems a bit odd to have these "holes" in the record extensions of private types, where the inherited type invariant applies to some but not all of the visible operations. I also think your general language-design principle makes sense, though I'm not quite convinced that we want to force overriding when inheriting an operation from the parent and inheriting a class-wide postcondition from a progenitor. It seems like we are interfering with what might be legitimate implementation inheritance. On the other hand, you can always override the inherited operation with a wrapper that calls the parent's operation, so perhaps this should not be a big concern. This would have the net effect of making the user aware of the wrapper that it is likely the compiler would have to create anyway, to insert the class-wide postcondition check. **************************************************************** From: Randy Brukardt Sent: Wednesday, December 11, 2013 8:00 PM A secondary issue with AI12-0042-1: when Tucker created wording for this, he didn't use the draft future standard. If he looked there, he would have see that we'd already modified 7.3.2(19/3) [for the function call problem]. Unfortunately, I don't see how to merge those successfully (at least without a lot of change). AI12-0042-1 gives the following wording change: Modify 7.3.2(16/3-19/3) as follows: * An invariant is checked upon successful return from a call on any subprogram or entry that: * is declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is 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, and] * has a result with a part of type T, or one or more parameters with a part of type T, or an access to variable parameter whose designated type has a part of type T[.]{,} {* and either: * T is a private type or a private extension and the subprogram or entry is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T, or * T is a record extension and the subprogram or entry is a primitive operation that corresponds to a visible operation of a private or private extension ancestor to which the same (class-wide) invariant applies.} And AI12-0044-1 has the following wording change: * has a result with a part of type T, or one or more {OUT or IN OUT} parameters with a part of type T, or an access{-to-object}[ to variable] parameter whose designated type has a part of type T[.]{; * is a procedure or entry and has an IN parameter with a part of type T.} The obvious combination gives: * An invariant is checked upon successful return from a call on any subprogram or entry that: * is declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is 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, and] * has a result with a part of type T, or one or more {OUT or IN OUT} parameters with a part of type T, or an access{-to-object}[ to variable] parameter whose designated type has a part of type T[.]{;} {* is a procedure or entry and has an IN parameter with a part of type T,} {* and either: * T is a private type or a private extension and the subprogram or entry is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T, or * T is a record extension and the subprogram or entry is a primitive operation that corresponds to a visible operation of a private or private extension ancestor to which the same (class-wide) invariant applies.} But the semicolon ending the revised 7.3.2(19/3) seems out of place -- all of the other bullets are combined with "and"; the two from AI12-0044-1 are really combined with "or". I suppose we could try something similar to what Tucker already did to pull the "or"s out: * An invariant is checked upon successful return from a call on any subprogram or entry that: * is declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is 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, and] {* and either:} * has a result with a part of type T, or one or more {OUT or IN OUT} parameters with a part of type T, or an access{-to-object}[ to variable] parameter whose designated type has a part of type T[.]{, or} {* is a procedure or entry and has an IN parameter with a part of type T,} {* and either: * T is a private type or a private extension and the subprogram or entry is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T, or * T is a record extension and the subprogram or entry is a primitive operation that corresponds to a visible operation of a private or private extension ancestor to which the same (class-wide) invariant applies.} or maybe even split up the bullets of the middle part (so all of the "or"s are at the same level): * An invariant is checked upon successful return from a call on any subprogram or entry that: * is declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is 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, and] {* and either:} {*} has a result with a part of type T, or {*} one or more {OUT or IN OUT} parameters with a part of type T, or {*} an access{-to-object}[ to variable] parameter whose designated type has a part of type T[.]{, or} {* is a procedure or entry and has an IN parameter with a part of type T,} {* and either: * T is a private type or a private extension and the subprogram or entry is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T, or * T is a record extension and the subprogram or entry is a primitive operation that corresponds to a visible operation of a private or private extension ancestor to which the same (class-wide) invariant applies.} It appears that the main problem is with the AI12-0044-1 wording, not so much with the AI12-0042-1 wording. Anyway, I don't like the double "and either". Any better ideas??? **************************************************************** From: Tucker Taft Sent: Saturday, December 14, 2013 4:51 PM > A secondary issue with AI12-0042-1: when Tucker created wording for > this, he didn't use the draft future standard. If he looked there, he > would have see that we'd already modified 7.3.2(19/3) [for the function call problem]. > Unfortunately, I don't see how to merge those successfully (at least > without a lot of change). > ... > > * An invariant is checked upon successful return from a call on any > subprogram or entry that: > > * is declared within the immediate scope of type T (or by an > instance of a generic unit, and the generic is 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, > and] > > {* and either:} > > {*} has a result with a part of type T, or > {*} one or more {OUT or IN OUT} parameters with a part of type T, or > {*} an access{-to-object}[ to variable] > parameter whose designated type has a part of type T[.]{, or} > {* is a procedure or entry and has an IN parameter with a > part of type T,} > > {* and either: > > * T is a private type or a private extension and the subprogram > or entry is visible outside the immediate scope of type T or > overrides an inherited operation that is visible outside the > immediate scope of T, or > > * T is a record extension and the subprogram or entry is a primitive > operation that corresponds to a visible operation of a private > or private extension ancestor to which the same (class-wide) > invariant applies.} This version seems better, but with my recent answer to your prior note, I would suggest we can simplify this a bit and treat record extensions and private extensions the same as it relates to applicability of class-wide invariants. This means it might be possible to merge the last two paragraphs, and eliminate the second "and either." **************************************************************** From: Jeff Cousins Sent: Tuesday, December 17, 2013 10:03 AM As a minimum we should change to the "pull the "or"s out version". The "split up the bullets" version would be better still, but the "has" should be repeated for the "OUT or IN OUT" and "access" cases. "that has an IN parameter" would seem clearer to me than "and has an IN parameter" and cut the mounting count of "and"s and "or"s. I think a comma is needed after "T is a private type or a private extension". Giving: * An invariant is checked upon successful return from a call on any subprogram or entry that: * is declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is 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, and] {* and either:} {*} has a result with a part of type T, or {* has} one or more {OUT or IN OUT} parameters with a part of type T, or {* has} an access{-to-object}[ to variable] parameter whose designated type has a part of type T[.]{, or} {* is a procedure or entry that has an IN parameter with a part of type T,} {* and either: * T is a private type or a private extension, and the subprogram or entry is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T, or * T is a record extension and the subprogram or entry is a primitive operation that corresponds to a visible operation of a private or private extension ancestor to which the same (class-wide) invariant applies.} I think merging the last two paragraphs as Tucker suggests would just get rid with of the "either" rather than the "and either", but what exactly would be the result? {* and: * T is a private type, a private extension, or a record extension, and the subprogram or entry is ?WHAT?} It's getting a bit beyond me now. **************************************************************** From: Tucker Taft Sent: Tuesday, December 17, 2013 10:54 AM > I think merging the last two paragraphs as Tucker suggests would just get rid > with of the "either" rather than the "and either", but what exactly would be > the result? > > {* and: > > * T is a private type, a private extension, or a record extension, > and the subprogram or entry is ?WHAT?} I would also move this in front of the prior "and-either" construct. Once we group record and private extensions together, we can simplify this to (roughly): * T is a private type, or a type extension declared immediately within the visible part of a package, and the subprogram or entry is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T **************************************************************** From: Jeff Cousins Sent: Tuesday, December 17, 2013 11:23 AM Thanks Tuck. Hopefully we're near a conclusion, it seemed worth a final push. 7.3.2 16/3 - 19/3: * An invariant is checked upon successful return from a call on any subprogram or entry that: * is declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is 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, and] {* T is a private type, or a type extension declared immediately within the visible part of a package, and the subprogram or entry is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T,} {* and either:} {*} has a result with a part of type T, or {* has} one or more {OUT or IN OUT} parameters with a part of type T, or {* has} an access{-to-object}[ to variable] parameter whose designated type has a part of type T[.]{, or} {* is a procedure or entry that has an IN parameter with a part of type T.} **************************************************************** From: Tucker Taft Sent: Tuesday, December 17, 2013 11:34 AM > Thanks Tuck. Hopefully we're near a conclusion, it seemed worth a final push. This looks OK, but it doesn't seem to have parallel construction when written out this way, and is perhaps redundant in various ways. I think this needs to be assigned to someone to work out. E-mail exchanges can only go so far. ;-) **************************************************************** From: Randy Brukardt Sent: Tuesday, December 17, 2013 4:17 PM I agree. (Of course, you're getting dangerously close to being the one so assigned. :-) In any case, there is no rush. Since we've seriously changed the conclusion that we voted on in Pittsburgh, the AI will have to be reopened. (It's not clear to me whether only primitive operations or all visible operations should be involved for record extensions, so I think we need a bit more consideration. See my next message.) Since that's the case, there is no particular rush to work out the wording (we've got until June). I needed something to put into the draft Standard, and I've got that. [Note that since I've already added AI12-0042-1 to the draft Standard, I won't take it out, since I presume we'll do something similar and it makes no sense to redo the work twice more (first to take it out, then to put it back). But it doesn't have to be perfect today.] **************************************************************** From: Randy Brukardt Sent: Tuesday, December 17, 2013 4:34 PM ... > {* and either:} > > {*} has a result with a part of type T, or > {* has} one or more {OUT or IN OUT} parameters with a part of type T, or > {* has} an access{-to-object}[ to variable] > parameter whose designated type has a part of type T[.]{, or} > {* is a procedure or entry that has an IN parameter with a part of type T.} This reminds me of a question: does T'Class have a part of type T? Does Root'Class (if T is visibly derived from Root)? Does NT'Class (if NT is visibly derived from T)? The definition of "part" doesn't make a clear answer, at least in my mind: "Similarly, a *part* of an object or value is used to mean the whole object or value, or any set of its subcomponents." So what is a part of type T, anyway? I've always thought it was an object or subcomponent of an object of type T. T'Class does NOT have one of those. OTOH, T'Class does have a set of subcomponents that happen to be the same set of subcomponents as type T has. (But these are different types, so there's nothing formally said about the relationship.) Perhaps one could claim that T'Class has a parent part of type T, although that's not literally true. But then NT'Class would seem to not be involved. A couple of the AARM notes for 7.3.2 seem to imply that these rules do in fact apply to class-wide types. If that's the case, I think we need to be much more explicit about that. (And which ones.) At least with an AARM note, and perhaps better with a user note. The reason this matters is the point I mentioned in my previous message. If an inherited class-wide invariant does not apply to class-wide types, then the only operations that matter are primitives of the type, which is the group that can be inherited and have problems with future changes in whether or not the invariant applies. Non-primitives (like class-wide operations) do not have these problems and as such there is a much weaker case for including them. Especially as the concerns about allowing holes in the model do not apply in any event to record extensions (they are by definition a large hole in the model, the exact size of that hole is not relevant). OTOH, if class-wide operations are intended to be covered by invariants of private types, then there would be a consistency issue. (And that does seem desirable in order to prevent holes in the model for private types. But unless Root'Class is covered [and I can't see any way for that to be the case], there is still a pretty large hole in the model, so I don't know if it matters again how large that hole is.) Which I why I'm confused by Tucker's leap to all routines (not just primitives). But maybe it's right. Anyone have any enlightenment? **************************************************************** From: Tucker Taft Sent: Tuesday, December 17, 2013 5:00 PM > ... Which I why I'm confused by Tucker's leap to all routines (not > just primitives). But maybe it's right. I didn't actually mean to make *that* leap, and that was one reason I am uncomfortable doing this wording by e-mail exchanges. I was really trying to eliminate the "hole" that a visible record extension could create when you have a sequence of extensions, some private and some record. It seems that all of these should be treated the same, since *most* of the components may still be private. Since we aren't changing the inherited invariant, but only adding primitive operations to which it should apply, it seems fine (and useful) if it applies to objects manipulated by primitive operations that were added as part of doing a record extension. > Anyone have any enlightenment? Well, back to your question about whether T'Class has a part of type T. I think the answer is that it should. Similar questions apply to all class-wide types rooted at descendants of T. I think yes for those as well. Then finally there is T0'Class, where T is a descendant of T0, and the actual object of type T0'Class happens to have a tag that identifies T (or some descendant of T). For those, I think "no" for legality rules and static semantics. I suppose there are some dynamic semantics rules where it might make sense to consider an object of nominal type T0'Class to have a part of type T, but that would be exceptional. I agree we should try to sort all of this class-wide stuff out, at least in cases where it might really matter. Certainly we need to decide to what objects and/or parts of objects we apply an invariant check. It seems like type invariants are in danger of turning into the rat-hole that streams were for Ada 95... **************************************************************** From: Randy Brukardt Sent: Tuesday, December 17, 2013 6:13 PM > > ... Which I why I'm confused by Tucker's leap to all routines (not > > just primitives). But maybe it's right. > > I didn't actually mean to make *that* leap, and that was one reason I > am uncomfortable doing this wording by e-mail exchanges. I was really > trying to eliminate the "hole" that a visible record extension could > create when you have a sequence of extensions, some private and some > record. It seems that all of these should be treated the same, since > *most* of the components may still be private. Right. Of course, when I tried to raise this point in Pittsburgh (because it was immediately obvious to me), you said it wasn't a problem and we moved on. So I guess meetings aren't the best place to do this wording, either. :-) > Since we aren't changing the inherited invariant, but only adding > primitive operations to which it should apply, it seems fine (and > useful) if it applies to objects manipulated by primitive operations > that were added as part of doing a record extension. That makes sense. Including class-wide operations also would make some sense, but that isn't as important because they can't change later. > > Anyone have any enlightenment? > > Well, back to your question about whether T'Class has a part of type > T. I think the answer is that it should. Similar questions apply to > all class-wide types rooted at descendants of T. I think yes for > those as well. I concluded the same as well. But my question was really "does T'Class already have a part of T, or do we need wording to make it true"? > Then finally there is T0'Class, where T is a descendant of T0, and the > actual object of type T0'Class happens to have a tag that identifies T > (or some descendant of T). For those, I think "no" for legality rules > and static semantics. I suppose there are some dynamic semantics > rules where it might make sense to consider an object of nominal type > T0'Class to have a part of type T, but that would be exceptional. > > I agree we should try to sort all of this class-wide stuff out, at > least in cases where it might really matter. > Certainly we need to decide to what objects and/or parts of objects we > apply an invariant check. > > It seems like type invariants are in danger of turning into the > rat-hole that streams were for Ada 95... Really, that's all of the assertions. (Think 'Old, and predicate ordering, and Predicate_Failure, and raise expressions...) And it's not that surprising, given we started from a blank sheet of paper. Hard to imagine that we'd get all of the details right on the first try. Anyway, to give us a concrete example to think about class-wide checks: package P is type Root is abstract tagged ... function Calc_It (Obj : in Root) return Natural is abstract; function Is_OK (Obj : in Root) return Boolean is abstract; end P; with P; package Q is type T is new P.Root with private with Type_Invariant => Is_OK (T); function Calc_It (Obj : in T) return Natural; -- No invariant check (function). function Is_OK (Obj : in T) return Boolean; -- No invariant check (function). function Create return Root'Class; -- No invariant check (? - no part of T). function Create_T return T'Class; -- Invariant check on result. end Q; with P, Q; procedure Main is Obj : P.Root'Class := Q.Create; -- Obj potentially is not Is_OK (invariant not checked). begin if P.Calc_It (Obj) > 10 then -- Dispatching call into Q with an object that was never checked and -- might not meet the invariant for type T. ... end Main; Note that Create_T would have an invariant check (assuming we follow Tucker's advice), but not Create. Thus Create could return a value of type T that doesn't meet the invariant. (It also could return a value that isn't of type T at all, but let's focus on the case where the value is in fact of type T.) Note that I was very careful to avoid any conversion to type T that might in fact trigger one of the other invariant checks. (I say "might" because figuring out when those rules apply make my head hurt, so I didn't try to figure them out again by avoiding any conversions at all.) This would seem to provide an easy way around the checking of an invariant. The basic idea is that "leaking" a value outside of the package without getting a check should be difficult. (There are ways involving access-to-subprogram types and call-backs within the package body, but to trigger one of those you really have to want to break the guarantees - it wouldn't happen by accident - so one imagines that even quick code review would catch the problem. This is not like that.) So I would think that we would want to plug this opening somehow. (Of course, the Root'Class could also be a parameter of some sort, passed a value of T that is then corrupted so it doesn't meet the invariant.) **************************************************************** From: Tucker Taft Sent: Thursday, December 19, 2013 2:36 PM > with P, Q; > procedure Main is > Obj : P.Root'Class := Q.Create; -- Obj potentially is not > Is_OK (invariant not checked). > begin > if P.Calc_It (Obj) > 10 then -- Dispatching call into Q with > an object that was never checked and > -- might not meet the invariant > for type T. I think this dispatching call involves an implicit conversion to type T, and so should involve an invariant check. > ... > end Main; > > Note that Create_T would have an invariant check (assuming we follow > Tucker's advice), but not Create. Thus Create could return a value of > type T that doesn't meet the invariant. (It also could return a value > that isn't of type T at all, but let's focus on the case where the > value is in fact of type T.) Note that I was very careful to avoid any > conversion to type T that might in fact trigger one of the other invariant checks. (I say "might" > because figuring out when those rules apply make my head hurt, so I > didn't try to figure them out again by avoiding any conversions at all.) ... I think we tried to design the conversion rules to catch some of these holes. It is easy to believe we missed some. **************************************************************** From: Randy Brukardt Sent: Thursday, December 19, 2013 4:38 PM ... > > if P.Calc_It (Obj) > 10 then -- Dispatching call into Q with > > an object that was never checked and > > -- might not meet the invariant > > for type T. > > I think this dispatching call involves an implicit conversion to type > T, and so should involve an invariant check. Maybe, I can never remember the rules for that. I was thinking that a dispatching call just called the right routine, without necessarily converting (formally) the operands, just as happens with a statically bound call. But perhaps there is a conversion in there somewhere. ... > > Note that Create_T would have an invariant check (assuming we follow > > Tucker's advice), but not Create. Thus Create could return a value > > of type T that doesn't meet the invariant. (It also could return a > > value that isn't of type T at all, but let's focus on the case where > > the value is in fact of type T.) Note that I was very careful to > > avoid any conversion to type T that might in fact trigger one of the > > other invariant > > checks. (I say "might" because figuring out when those rules apply > > make my head hurt, so I didn't try to figure them out again by > > avoiding any conversions at all.) ... > > I think we tried to design the conversion rules to catch some of these > holes. It is easy to believe we missed some. BTW, this AI got assigned back to you as you were the author of record on it. Since a significant part of the redo involves wording, it is right in your wheelhouse. If you would prefer that someone else take it on, please tell me so that we can find a different victim, er, author. **************************************************************** From: Tucker Taft Sent: Thursday, December 19, 2013 5:03 PM > Maybe, I can never remember the rules for that. I was thinking that a > dispatching call just called the right routine, without necessarily > converting (formally) the operands, just as happens with a statically > bound call. But perhaps there is a conversion in there somewhere. This one is actually pretty simple. On any call, every actual parameter is converted to the subtype of the formal parameter if it is a by-copy IN or IN OUT parameter, or is a by-reference parameter of any mode (this latter conversion is a view conversion). ... > BTW, this AI got assigned back to you as you were the author of record > on it. Since a significant part of the redo involves wording, it is > right in your wheelhouse. If you would prefer that someone else take > it on, please tell me so that we can find a different victim, er, author. Not a problem. **************************************************************** From: Bob Duff Sent: Thursday, December 19, 2013 5:18 PM > This one is actually pretty simple. Nothing is simple. ;-) >...On any call, every actual parameter is converted to the subtype of >the formal parameter if it is a by-copy IN or IN OUT parameter, or is >a by-reference parameter of any mode (this latter conversion is a view >conversion). What makes this one not quite as simple as you might think is that by-copy vs. by-ref is implementation dependent. There is a special rule for predicates, which is necessary because we didn't want the places where predicates are checked to inherit this implementation dependence. So we can't "simply" say that every subtype conversion involves a predicate check. **************************************************************** From: Randy Brukardt Sent: Thursday, December 19, 2013 5:47 PM > > Maybe, I can never remember the rules for that. I was thinking that > > a dispatching call just called the right routine, without > > necessarily converting (formally) the operands, just as happens with > > a statically bound call. But perhaps there is a conversion in there somewhere. > > This one is actually pretty simple. On any call, every actual > parameter is converted to the subtype of the formal parameter if it is > a by-copy IN or IN OUT parameter, or is a by-reference parameter of > any mode (this latter conversion is a view conversion). To which Bob replied: > Nothing is simple. ;-) I think Bob's right. The rule for view conversions only applies outside of the scope of T. 7.3.2(12/3). You are saying that it applies to a dispatching call (which makes sense). But now think a bit about the implementation of this. At the point of the call, we don't know statically the type of T. That means that we have to dispatch (somehow) to make the needed invariant check; moreover, we have to do this for any dispatching call, whether or not any invariants are involved (absent full program compilation), because some future descendant (not necessarily written yet) might add an invariant. And we have to pass some sort of indication as to where this call occurred, because we don't know what T is, so we certainly can't determine if we are outside of the scope of T at the point of the call. (After all, we might be in the scope of some descendant of T.) On top of this, the rule is supposed to be applied recursively, for every ancestor of T that you have to pass through. AARM note 14.c/3 mentions this, but neglects to mention that being "outside of the scope of T" doesn't necessarily mean that you're outside of the scope of T's parent. You could somehow fold this information into extra parameters for the target of the call to avoid extra dispatching, but this would not only be distributed overhead, but also would make the profiles differ for 'Access and the like. Presumably, this would all have to be stuck into a wrapper for every dispatching routine that exists, since someone could add a new package deriving from the type and add an invariant. (If Ada had "final", it could be mitigated somewhat, but it still sounds awful.) This sounds to me like we had drunk too much scotch in Edinburgh when we came up with this one. :-) I hope I have missed something obvious about the interaction of these rules and dispatching, but the existence of 7.3.2(14.c/3) suggests that we thought this complication was just peachy. Please enlighten me! **************************************************************** From: Robert Dewar Sent: Thursday, December 19, 2013 9:48 PM > This is at best distributed overhead. I would have written This is at best unacceptable distributed overhead. We don't want new features in the language to EVER add distributed overhead to programs that don't use these features! If we have to do this, we have to add a restriction to get back to where we were, and it is unpleasant to have to do this on an all-or-nothing full program basis. I really think this needs fixing! **************************************************************** From: Randy Brukardt Sent: Thursday, December 19, 2013 10:28 PM I was assuming that I misunderstood something, and Tucker or Erhard would straighten me out. And I did have one thing wrong, in that the effect doesn't happen on inbound parameters, but rather on the return from the routines. Same problems though. I'll try to create a full example tomorrow to show the effect at its nastiest. **************************************************************** From: Tucker Taft Sent: Friday, December 20, 2013 2:19 PM >>> ... >>>>> if P.Calc_It (Obj) > 10 then -- Dispatching call into Q >>>>> with an object that was never checked and >>>>> -- might not meet the >>>>> invariant for type T. >>>> >>>> I think this dispatching call involves an implicit conversion to >>>> type T, and so should involve an invariant check. I am not so sure about this anymore. We don't want to interpret 7.3.2(11/3) to imply that we recheck the invariant on *every* call even when the actual is already of type T. I think 11/3 needs to be modified to say: * After successful conversion to type T {where the operand is not of type T}, the check is performed on the result of the conversion; and perhaps modified further to say: * After successful conversion to type T {where the operand is not of type T nor, if tagged, has a tag that identifies T}, the check is performed on the result of the conversion; If we make this further modification, then we need to make sure that on conversion *to* a class-wide type from inside the immediate scope of T, that the operand satisfies the invariant, unless it is T'Class itself and we check the invariant on those on the way out of the immediate scope. My temptation would now be to avoid any special handling of class-wide types at the interface, and do it all on the conversion *to* a class-wide type from T when *inside* the immediate scope. Essentially we would treat viewing an object as a class-wide type as effectively stepping "outside" the area where invariant violations are permitted, sort of like returning the value from a visible function. >>> >>> Maybe, I can never remember the rules for that. I was thinking that >>> a dispatching call just called the right routine, without >>> necessarily converting (formally) the operands, just as happens with >>> a statically bound call. But perhaps there is a conversion in there somewhere. >> >> This one is actually pretty simple. On any call, every actual >> parameter is converted to the subtype of the formal parameter if it >> is a by-copy IN or IN OUT parameter, or is a by-reference parameter >> of any mode (this latter conversion is a view conversion). > > To which Bob replied: > >> Nothing is simple. ;-) > > I think Bob's right. The rule for view conversions only applies > outside of the scope of T. 7.3.2(12/3). You are saying that it applies > to a dispatching call (which makes sense). There are two rules about conversions, one applies in all cases where we are converting *to* T, whether a value or a view conversion, and whether we are inside or outside the scope of T (7.3.2(11/3)). The other one only applies to view conversions, which go *from* T (or a descendant thereof), to a "proper" ancestor of T, and only when the view conversion is the LHS of an assignment (13/3), or upon subprogram return when the view conversion is an OUT or IN OUT actual parameter (14/3). In both of these cases (13/3 and 14/3), the underlying object has a part that is of type T, but the value being assigned does *not* have a part that is of type T, so we need to check that updating this ancestor part of T doesn't foul up the invariant on T. > But now think a bit about the implementation of this. At the point of > the call, we don't know statically the type of T. I think you mean we don't know statically whether the object's tag identifies T. In any case, this is the case where the actual is of type Root'Class. In that case, we might be triggering 11/3 (depending on how we end up modifying it), but we are definitely not triggering 12/3. > I hope I have missed something obvious about the interaction of these > rules and dispatching, but the existence of 7.3.2(14.c/3) suggests > that we thought this complication was just peachy. Please enlighten me! 12/3-14/3 only apply when converting *from* T, not *to* T, and only upon assignment or returning from a subprogram with an OUT or IN OUT parameter of some proper ancestor of T. So I don't think these apply to the Root'Class case. **************************************************************** From: Randy Brukardt Sent: Friday, December 20, 2013 5:56 PM ... > >>>> I think this dispatching call involves an implicit conversion to > >>>> type T, and so should involve an invariant check. > > I am not so sure about this anymore. We don't want to interpret > 7.3.2(11/3) to imply that we recheck the invariant on *every* call > even when the actual is already of type T. I think 11/3 needs to be > modified to say: > > * After successful conversion to type T {where the operand is not of > type T}, the check is performed on the result of the conversion; > > and perhaps modified further to say: > > * After successful conversion to type T {where the operand is not of > type T nor, if tagged, has a tag that identifies T}, the check is > performed on the result of the conversion; Ignoring the merits of the change, as soon as you make this conversion conditional, you are making it much harder to implement the check inside of the subprogram body (or wrapper, as appropriate). In particular, for a dispatching call, when you reach the body, you know longer know the type of the operand. I think you're trying to mitigate that by using the tag, but that would have the effect of checking some invariants in statically bound calls that you wouldn't otherwise check. Or you're requiring different bodies (really, different wrappers) for the target of dispatching calls vs. normal calls. In any case, I don't think it matters too much how this gets changed until we figure out how to make 7.3.2(12/3) implementable without distributed overhead. Your message is primarily answering my confused message, which doesn't help any. Let's look at longer and very painful (with the current wording) example: package PR is type Root is abstract tagged ... procedure Op (P : in out Root) is abstract; end PR; with PR; package P1 is type T1 is new PR.Root with private with Type_Invariant => Exp1(T1); procedure Op (P : in out T1); private ... end P1; with PR, P1; package P2 is type T2 is new P1.T1 with private with Type_Invariant => Exp2(T2); procedure Op (P : in out T2); procedure Do_It (P : in out Root'Class); private ... end P2; package body P2 is procedure Do_It (P : in out Root'Class) is begin P.Op; -- (1) end Do_It; ... end P2; with P2, PR; package P3 is type T3 is new P2.T2 with private with Type_Invariant => Exp3(T3); procedure Op (P : in out T3); function Leaky return PR.Root'Class; -- Might leak out an unchecked object of T3 private ... end P3; with PR, P2, P3; procedure Main is Obj2 : P3.T3 := P3.T3(P3.Leaky); -- Assume Leaky returns an object with the tag of type T3. Obj3 : PR.Root'Class := P3.Leaky; -- Assume Leaky returns an object with the tag of type T3. Obj4 : P2.T2'Class := P2.T2'Class(P3.Leaky); -- Assume Leaky returns an object with the tag of type T3. begin P2.Do_It (Obj2); -- (2) P2.Do_It (Obj3); -- (3) P2.Do_It (Obj4); -- (4) end Main; The explicit conversion to P3.T3 checks the invariant of T3. There is no check for Obj3, of course. Call (2) does not check any invariants of Obj, as there is no invariant on the target of the implicit conversion of the parameter of Do_It which is Root'Class. Nor does call (3), as there is no (non-trivial) conversion. The dispatching call at (1) [with the existing 7.3.2(11.3) wording] will check the invariant of T3 (Exp3(T3)) during the inbound call. So far, so good. Let's now consider the rule of 7.3.2(12-14/3). My original concern was how that interacts with dispatching calls. I think I've convinced myself (in writing this note), that it can never be triggered in a dispatching call (such as (1)). The reason is that a dispatching call always has an actual of some class-wide type, which is then converted to some specific descendant type. So the view conversion must always go from some ancestor to some descendant, and as such cannot trigger 7.3.2(12-14/3). That at least means that there isn't any distributed overhead here. 7.3.2(12-14/3) *is* triggered by (2). We know both the target (Root'Class) and source (T3) types, we're clearly outside of the scope of either, and we'll need to check each invariant in turn (Exp1, Exp2, Exp3) when the call returns. (T3 being a descendant of T2 and T1, so we need to check them all.) It appears to me that 7.3.2(12-14/3) is not triggered by call (3), because the source and target types are the same (Root'Class). I'm not quite sure what is supposed to happen for call (4). The AARM note 7.3.2(14.c/3) implies that the check depends on the actual tag of the object -- but nothing in the wording seems to imply that. The wording appears to say that we have a view conversion from T2'Class to Root'Class, so we need to check Exp1 and Exp2 on return. That's implementable, because the rule can be determined for each type that's involved. Note that if we move call (4) into the body of package P2 (as part of a class-wide routine, perhaps), then we would *not* check the invariant of T2 (as we'd be in its scope), but we still would check the invariant of T1 (because we wouldn't be in its scope). If the rule did somehow depend on the actual tag, we wouldn't know at compile-time which rules to check, and a simple dispatching routine as described in the note wouldn't work right, either, because we also have to check whether we're within the scope at each step. I don't think that we can get back inside if we are once outside, so at least it would be possible to start in the middle somehow. If we imagine that Op and Do_It have only an "out" parameter, then it seems that we'd have made the needed checks to prevent leaking, but only when the target object has type T3. If it has some other type with the tag of T3, we'd still be leaking the value, but a later implicit conversion should make the check before it gets back inside. All this means that I think we're OK so long as we keep the runtime tags out of it. But perhaps there is an example where including them is necessary (I haven't been able to find it). P.S. Man, this stuff is hard to understand, made worse because the 7.3.2(12-14/3) necessarily has the conversion described backwards (since it is the return conversion that we're checking). **************************************************************** From: Tucker Taft Sent: Sunday, December 22, 2013 9:59 PM > Ignoring the merits of the change, as soon as you make this conversion > conditional, you are making it much harder to implement the check > inside of the subprogram body (or wrapper, as appropriate). In > particular, for a dispatching call, when you reach the body, you no > longer know the type of the operand. Good point. It might be better to leave it as is, and then give an implementation permission to omit the check when the tag identifies T or the type of the operand is already T. I still like the idea of requiring that all objects of a class-wide type have already had the invariant checked, as part of converting to the class-wide type. What that means is that you can rely on all class-wide objects already obeying the invariant of their tag-identified type. > I think you're trying to mitigate that by using the tag, but that > would have the effect of checking some invariants in statically bound > calls that you wouldn't otherwise check. Or you're requiring different > bodies (really, different wrappers) for the target of dispatching calls vs. normal calls. > > In any case, I don't think it matters too much how this gets changed > until we figure out how to make 7.3.2(12/3) implementable without > distributed overhead. Your message is primarily answering my confused > message, which doesn't help any. > > Let's look at longer and very painful (with the current wording) example: > > package PR is > type Root is abstract tagged ... > procedure Op (P : in out Root) is abstract; > end PR; > > with PR; > package P1 is > type T1 is new PR.Root with private > with Type_Invariant => Exp1(T1); > procedure Op (P : in out T1); > private > ... > end P1; > > with PR, P1; > package P2 is > type T2 is new P1.T1 with private > with Type_Invariant => Exp2(T2); > procedure Op (P : in out T2); > procedure Do_It (P : in out Root'Class); > private > ... > end P2; > > package body P2 is > procedure Do_It (P : in out Root'Class) is > begin > P.Op; -- (1) > end Do_It; > ... > end P2; > > with P2, PR; > package P3 is > type T3 is new P2.T2 with private > with Type_Invariant => Exp3(T3); > procedure Op (P : in out T3); > function Leaky return PR.Root'Class; -- Might leak out an > -- unchecked object of T3 It won't "leak" if we require the invariant being checked on conversion to a class-wide type. > private > ... > ... > All this means that I think we're OK so long as we keep the runtime > tags out of it. But perhaps there is an example where including them > is necessary (I haven't been able to find it). I didn't follow your complete example, but I agree that we are OK. I still think we need to settle the question of whether inherited class-wide invariants apply to all primitives of a record extension or just the ones that correspond to primitives of the nearest private (extension) ancestor. I have come around to thinking it should apply to all of them. **************************************************************** From: Randy Brukardt Sent: Monday, December 23, 2013 4:40 PM > Good point. It might be better to leave it as is, and then give an > implementation permission to omit the check when the tag identifies T > or the type of the operand is already T. > > I still like the idea of requiring that all objects of a class-wide > type have already had the invariant checked, as part of converting to > the class-wide type. What that means is that you can rely on all > class-wide objects already obeying the invariant of their > tag-identified type. Careful: when talking about class-wide types, you have to worry about ancestor class-wide types (like Root'Class in these examples). If you require an invariant check on those, that has to be a dispatching call to an invariant check subprogram, and that would be a sort of distributed overhead in that you'd have to do it whether or not the type itself has an invariant (because some extension could add it). If you only have it apply to descendant class-wide types (as it arguably does now), you avoid that problem, but then there is a possibility of holes using the root type. (At least we haven't seen an example with a clear hole yet, so maybe that's more of a worry than a real problem.) In any case, we need to determine whether descendant class-wide types are covered by the current wording or not (it's not clear to me) -- this is mainly about T'Class in a package defining T (remember that T is formally a descendant of itself). ... > I didn't follow your complete example, but I agree that we are OK. I > still think we need to settle the question of whether inherited > class-wide invariants apply to all primitives of a record extension or > just the ones that correspond to primitives of the nearest private > (extension) ancestor. I have come around to thinking it should apply > to all of them. Certainly it should apply to all (at least in my view), because it avoids surprises that could otherwise come via dispatching. I suppose we'll need to settle that at a meeting, but as far as this e-mail thread is concerned, I think it is settled. (At least until someone else joins in!) **************************************************************** From: Tucker Taft Sent: Monday, December 23, 2013 9:51 PM > Careful: when talking about class-wide types, you have to worry about > ancestor class-wide types (like Root'Class in these examples). If you > require an invariant check on those, that has to be a dispatching call > to an invariant check subprogram, and that would be a sort of > distributed overhead in that you'd have to do it whether or not the > type itself has an invariant (because some extension could add it)... I meant that the invariant check occurs on conversion from a *specific* type to a class-wide type. At that point you know which invariant to apply. The one you are converting *from*. And the check only needs to occur when this conversion happens *within* the immediate scope of the type. **************************************************************** From: Randy Brukardt Sent: Thursday, December 26, 2013 1:08 PM I'm not even sure that we're talking about the same problems anymore. Anyway, I think it would be best if you sat down and figured out what you think we need to do and present it in the clear way that you can (and I can't, unfortunately). Then I can try to figure out whether or not it makes sense to me. Rather than us talking about slightly different issues and confusing everyone (including ourselves). **************************************************************** From: Randy Brukardt Sent: Thursday, December 19, 2013 10:12 PM Here's a summary of changes that appear to be required to AI12-0042-1; hopefully this will help Tucker out on this AI. (This is from the previous mail thread, which I just finished filing. [But note: the last six messages above came after this summary was created - Editor.]) [A] Add a language design principle along the lines of: "Inheritance cannot add requirements (postconditions and invariants) to an existing subprogram; subprograms have to be overridden to add requirements." (I'd suggest that this be a language-design principle, in fact.)" [Or perhaps just for invariants.] The reason is that the existence of an explicit body provides a key to provers (both human and automatic) that a new proof is required (which it is whenever a new requirement is added). [B] An inherited class-wide invariant should apply to any primitive operations of a record extension, but not to other subprograms that happen to be in the package specification. The merged wording that was proposed covered too many subprograms. Here's wording that's correct (I hope) but definitely needs wordsmithing. (Note that the last bullet includes "primitive operation" while the penultimate bullet does not.) * An invariant is checked upon successful return from a call on any subprogram or entry that: * is declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is 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, and] {* and either:} {*} has a result with a part of type T, or {* has} one or more {OUT or IN OUT} parameters with a part of type T, or {* has} an access{-to-object}[ to variable] parameter whose designated type has a part of type T[.]{, or} {* is a procedure or entry that has an IN parameter with a part of type T,} {* and either: * T is a private type or a private extension, and the subprogram or entry is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T, or * T is a record extension, and the subprogram or entry is a primitive operation visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T.} [C] The new wording for 7.4.3(6/3) has to cover the case of record extensions as well, since with this new wording, the same thing can happen on record extension inheritance. [D] The summary and discussion ought to be updated as needed. [E] There is something weird about the rules for dispatching calls and view conversions. The view conversion check is only performed outside of the scope of T -- but that means it depends on the location of the call. OTOH, the check needed is only known via dispatching (because the actual target type isn't known). So it seems like there is no place where we know both the visibility and the types involved. Moreover, when multiple checks are needed because multiple types are crossed, it seems like not all of the checks might be needed depending on where the call is. Perhaps the wording is confusing the issue. In any case, it sounds like implementation trouble. Possibly that should be a separate AI. [Note that there is later discussion on this point, filed above. - Editor] [There is also an issue with how invariants are checked for class-wide operations. It appears that class-wide invariants need to apply to operations and objects of descendant class-wide types, as well as the specific types. The current wording is unclear. See end of thread above. - Editor] ****************************************************************