!standard 7.3.2(19.1/4) 16-06-06 AI12-0191-1/01 !standard 7.3.2(19.2/4) !standard 7.3.2(19.3/4) !standard 7.3.2(19.4/4) !class binding interpretation 16-06-06 !status work item 16-06-06 !status received 16-05-31 !priority Low !difficulty Medium !qualifier Omission !subject Clarify "part" for type invariants !summary ** TBD. !question The term "part" is used several times in the section on Type Invariants. Does this usage of "part" include the "parent part"? (No.) !recommendation (See Summary.) !wording ** Not a clue ** (We might want to try to clarify that this is a statically determined part [which is what we want here] rather than a dynamically determined part [which what the similar wording for finalization means]. This problem was discussed - and punted - in AI12-0167-1. - Editor.) !discussion If the programmer wants the invariant to be enforced on all descendants, she can use Type_Invariant'Class on the original type. Therefore, we want Type_Invariant to work differently. Also note that it is unusual to have a type extension in the same package as its parent. If, at a later point, the type extension is given its own package, we'd prefer that the invariant enforcement change as little as possible. !example with Derived; use Derived; procedure Testinv is X : D; begin Create (X); end Testinv; --- package Derived is type T is tagged private; type D is tagged private; procedure Create (X : out T); procedure Create (X : out D); private type T is tagged record C : Integer; end record with Type_Invariant => T.C /= 0; type D is new T with null record; end Derived; --- package body Derived is procedure Create (X : out T) is begin X.C := 1; end Create; procedure Create (X : out D) is begin X.C := 0; -- Parent part type-invariant failure on return? (No.) end Create; end Derived; !ASIS No ASIS effect. !ACATS test !appendix From: Tucker Taft Sent: Tuesday, May 31, 2016 2:13 PM The term "part" is used several times in the section on Type Invariants. The question is whether this always is meant to apply to the "parent part" (and for that matter, every ancestor part) of the object. My view is that when the RM says "any part", we usually want it to mean precisely "any subcomponent, or the object as a whole." The definition of "part" also talks about sets of subcomponents, and mentions it use in terms like the "parent part" and the "extension part." But I think those usages only make sense when we are talking about untyped sets of things. For a type invariant, clearly we are only talking about "typed" parts, and I don't believe the parent part has a type in the normal sense. You can create a "typed view" of the parent part by a view conversion, but until you do that, the parent part is not an object, but rather just a collection of components. Below is an example that shows the issue. The question is whether the call on Create for type D should fail on return, because the parent part doesn't satisfy its invariant: ---- with Derived; use Derived; procedure Testinv is X : D; begin Create (X); end Testinv; --- package Derived is type T is tagged private; type D is tagged private; procedure Create (X : out T); procedure Create (X : out D); private type T is tagged record C : Integer; end record with Type_Invariant => T.C /= 0; type D is new T with null record; end Derived; --- package body Derived is procedure Create (X : out T) is begin X.C := 1; end Create; procedure Create (X : out D) is begin X.C := 0; -- Parent part type-invariant failure on return? end Create; end Derived; **************************************************************** From: Randy Brukardt Sent: Tuesday, May 31, 2016 6:48 PM > The term "part" is used several times in the section on Type > Invariants. The question is whether this always is meant to apply to > the "parent part" (and for that matter, every ancestor part) of the > object. My view is that when the RM says "any part", we usually want > it to mean precisely "any subcomponent, or the object as a whole." > The definition of "part" also talks about sets of subcomponents, and > mentions it use in terms like the "parent part" and the "extension > part." But I think those usages only make sense when we are talking > about untyped sets of things. For a type invariant, clearly we are > only talking about "typed" parts, and I don't believe the parent part > has a type in the normal sense. You can create a "typed view" of the > parent part by a view conversion, but until you do that, the parent > part is not an object, but rather just a collection of components. As usual, it's probably better to figure out what we want and then decide whether the words say that, rather than try to figure out what the words actually say. We already know (at least those of us that have tried to write ACATS tests and objectives) that the wording of 7.3.2 is pretty fast-and-loose about what is and is not included. (Steve's notes about "parts" known dynamically vs. "parts" known statically are a big deal to this check being efficient, but the wording is interpreted 100% differently than the very similar wording for finalization.) And I think that it doesn't make much sense for the parent extension to get enforced separately for a type extension. If a programmer wants to ensure that an invariant is enforced on extensions, they can use a Type_Invariant'Class. Otherwise, as with all derived types, nothing gets inherited. > Below is an example that shows the issue. The question is whether the > call on Create for type D should fail on return, because the parent > part doesn't satisfy its invariant: > ---- > > with Derived; use Derived; > procedure Testinv is > X : D; > begin > Create (X); > end Testinv; > --- > package Derived is > > type T is tagged private; > type D is tagged private; > > procedure Create (X : out T); > procedure Create (X : out D); > > private > > type T is tagged record > C : Integer; > end record > with Type_Invariant => T.C /= 0; > > type D is new T with null record; > > end Derived; > --- > package body Derived is > > procedure Create (X : out T) is > begin > X.C := 1; > end Create; > > procedure Create (X : out D) is > begin > X.C := 0; -- Parent part type-invariant failure on return? > end Create; > > end Derived; It's of course unusual to put a type and its extension into the same package, so the answer here isn't terrible critical. But it's probably best for the behavior to change as little as possible when these two types are inevitably split into separate packages. **************************************************************** From: Steve Baird Sent: Friday, August 19, 2016 2:24 PM Pisa minutes say: Steve volunteers to help find out what GNAT does on cases of “parts” that are only dynamically known for type invariant checks. No checks for these guys. For the following example (with all assertions enabled) compiled with the GNAT compiler, procedure Type_Invariant_Breaker is type Root is tagged null record; package Pkg is type Has_Invariant is private; procedure Oops (X : in out Root'Class); procedure Rely_On_Incoming_Invariant (Y : Has_Invariant); private type Has_Invariant is record Lo, Hi : Integer := 0; end record with Type_Invariant => (Has_Invariant.Lo <= Has_Invariant.Hi); end Pkg; type Ext is new Root with record Field : Pkg.Has_Invariant; end record; package body Pkg is procedure Break_It (Xx : out Has_Invariant) is begin Xx := (Lo => 1, Hi => 0); end; procedure Oops (X : in out Root'Class) is begin if X in Ext'Class then Break_It (Ext (X).Field); end if; end; procedure Rely_On_Incoming_Invariant (Y : Has_Invariant) is begin pragma Assert (Y.Lo <= Y.Hi); end; end Pkg; Ext_Var : Ext; begin Pkg.Oops (Ext_Var); Pkg.Rely_On_Incoming_Invariant (Ext_Var.Field); end; we fail the assertion in Rely_On_Incoming_Invariant, which means that the preceding call to Oops didn't fail any checks. I believe this implementation is correct and should not be changed. The problem here is that the RM wording doesn't make this clear (which is the topic of this AI). The other interpretation (i.e., the one where the call to Oops would be required to fail an invariant check) would be better in some sense but I don't know how to implement it without introducing distributed overhead and a lot more implementation complexity than than this feature would be worth. ***************************************************************