Version 1.15 of ai12s/ai12-0191-1.txt

Unformatted version of ai12s/ai12-0191-1.txt version 1.15
Other versions for file ai12s/ai12-0191-1.txt

!standard 3.9.1(4.1/2)          19-06-05 AI12-0191-1/11
!standard 7.3.2(10.1/4)
!standard 7.3.2(15/5)
!class binding interpretation 16-06-06
!status Amendment 1-2012 19-05-09
!status work item 19-06-05
!status ARG Approved 11-0-0 19-05-09
!status work item 16-06-06
!status received 16-05-31
!priority Low
!difficulty Medium
!qualifier Omission
!subject Clarify "part" for type invariants
!summary
Components that are not components of the nominal type are not checked even if a type invariant check would apply to them.
!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
Add after AARM 3.1(7.d/3): [continuing the AARM note]
For example, a reference to the components of an object in a rule that is interpreted at compile-time would not apply to components that are not visible. On the other hand, a reference to the components of an object in a dynamic semantics rule would apply to all components of the object, visible or not, including (for tagged objects) components which are not components of the nominal type of the object (see 3.9.1). Other terms, such as "subcomponent" and "part", are interpreted analogously.
Modify 3.3(23/5):
At the place where a view of an object is defined, a nominal subtype is associated with the view.{ The nominal type of a view is the type of the nominal subtype.} ...
Add after 3.9.1(4.1/2):
In the case where the (compile-time) view of an object X is of a tagged type T1 or T1'Class and the (run-time) tag of X is T2'Tag, only the components (if any) of X that are components of T1 (or that are discriminants which correspond to a discriminant of T1) are said to be "components of the nominal type" of X. Similarly, only parts (respectively, subcomponents) of T1 are parts (respectively, subcomponents) of the nominal type of X.
AARM Ramification: For example, if T2 is an undiscriminated extension of T1 which declares a component named Comp, then X.Comp is not a component of the nominal type of X.
AARM note: For example, there is a dynamic semantics rule that finalization of an object includes finalization of its components (see 7.6.1). In the following case
type T1 is tagged null record; type T2 is new T1 with record Comp : Some_Controlled_Type; end record; function Func return T1'Class is (T2'(others => <>)); X : T1'Class := Func;
the rule that "every component of the object is finalized" (as opposed to something like "every component of the nominal type of the object is finalized") means that the finalization of X will include finalization of X.Comp. For another example, see the rule about accessibility checking of access discriminants of parts of function results in 6.5. In contrast, the rules in 7.3.2 explicitly state that type invariant checks are only performed for parts which are of the type-invariant bearing type and which are parts of the nominal type of the object (as opposed to for all parts, whether part of the nominal type or not, which are of the invariant-bearing type). Similarly, the rule in 13.13.2 governing which components of a composite value are read and written by the default implementations of Read and Write for a composite type states that only the components of the object which are components of the nominal type of the object are read or written.
Replace 6.8(5.8/5): [from AI12-0075-1]
* for result type R, if the function is a boundary entity for type R (see 7.3.2), no type invariant applies to type R; if R has a component type C, a similar rule applies to C.
Replace 7.3.2(8.3-8.12/5) with: [from AI12-0075-1]
For a nonabstract type T, a callable entity is said to be a boundary entity for T if it is declared within the immediate scope of T (or by an instance of a generic unit, and the generic is declared within the immediate scope of type T), or is the Read or Input stream-oriented attribute of type T, and either:
* T is a private type or a private extension and the callable entity 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 callable entity 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.
AARM Reason: A boundary entity is one that might require an invariant check for T. It includes subprograms that don't (visibly) involve T; since we don't want to break privacy, we can't statically know if some private type has some part of T. We'll reduce the set when we describe the actual checks.
Modify 7.3.2(10.1/4):
After successful explicit initialization of the completion of a deferred constant [with]{whose nominal type has} a part of type T, if the completion is inside the immediate scope of the full view of T, and the deferred constant is visible outside the immediate scope of T, the check is performed on the part(s) of {the nominal type of the object that have }type T;
Replace 7.3.2(15/5) with: [most recent version for AI12-0075-1]
Upon successful return from a call on any callable entity which is a boundary entity for T, an invariant check is performed on each object subject to an invariant check for T. In the case of a call to a protected operation, the check is performed before the end of the protected action. In the case of a call to a task entry, the check is performed before the end of the rendezvous the object initialized by the stream attribute. The following objects of a callable entity are subject to an invariant check for T:
* a result with a nominal type that has a part of type T;
* an *out* or *in out* parameter whose nominal type has a part of type T;
* an access-to-object parameter or result whose designated nominal type has a part of type T; or
[Author's question: is "designated nominal type" OK? Or do we have to say "whose
nominal type of its designated type"?]
* for a procedure or entry, an *in* parameter of whose nominal type has a part of type T.
AARM Ramification: This is a Dynamic Semantics rule, so we ignore privacy when determining if a check is needed. We do, however, use the nominal type to determine if a part of type T is present; therefore, parts that aren't known at compile-time (after ignoring privacy) are never subject to invariant checks. This is preferable, as we don't want overhead associated with the possibility that there might exist an extension of a tagged type that has a part of type T. (See the "leaks" note below for avoidance advice.) [Editor's note: The "leaks" note is actually in AI12-0210-1.]
AARM Discussion: We don't check in parameters for functions to avoid infinite recursion for calls to public functions appearing in invariant expressions. Such function calls are unavoidable for class-wide invariants and likely for other invariants. This is the simplest rule that avoids trouble, and functions are much more likely to be queries that don't modify their parameters than other callable entities. [Editor's note: This is an existing note that just getting moved with the associated wording.]
Delete AARM 7.3.2(20.a.1/5). [This is rewritten into a Ramification above.]
Modify in 13.13.2(9/3):
... the Write or Read attribute for each component {(excluding those, if any, that are not components of the nominal type of the object)} is called ...
!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.
The wording does not guarantee that every use of "component", "subcomponent", and "part" in the RM has the correct meaning with respect to "hidden" components of tagged types, but it fixes the problematic cases that we know about and provides a framework so that fixing any further problems that are discovered should be straightforward.
Note that we don't use the word "hidden" in the proposed wording because that seems too tied to visibility, which is not what we are talking about. We are talking about components whose existence is likely to be unknown at compile-time even if the compiler looks through all private types and expands all generic instances (specs and bodies). The implementation of any dynamic semantics rule requiring that some action needs to be performed for such components (for instance, finalization) will typically require dispatching.
AI12-0075-1 moved much of the 7.3.2 wording to Static Semantics. That, however, doesn't work, as Static Semantics rules do not break privacy, meaning that in many cases, the "parts of T" and whether or not a type invariant applies is not known at the point of the subprogram definition. Therefore, we move most of the 7.3.2 rules back to the Dynamic Semantics part, and adjust the AI12-0075-1 Legality Rules accordingly.
The AI12-0075-1 Legality Rules don't have to be very general, as the other rules of static expression functions ensure that the parameters and result all have static subtypes (thus eliminating partial views, access types, and composite types other than string types) and the parameters are all of mode in (so no invariants are checked on the parameters, ever). Thus, the only case to worry about is of the result type, and only when the full type has already happened (so privacy is not an issue).
!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;
!corrigendum 3.3(23/3)
Replace the paragraph:
At the place where a view of an object is defined, a nominal subtype is associated with the view. The object's actual subtype (that is, its subtype) can be more restrictive than the nominal subtype of the view; it always is if the nominal subtype is an indefinite subtype. A subtype is an indefinite subtype if it is an unconstrained array subtype, or if it has unknown discriminants or unconstrained discriminants without defaults (see 3.7); otherwise, the subtype is a definite subtype (all elementary subtypes are definite subtypes). A class-wide subtype is defined to have unknown discriminants, and is therefore an indefinite subtype. An indefinite subtype does not by itself provide enough information to create an object; an additional constraint or explicit initialization expression is necessary (see 3.3.1). A component cannot have an indefinite nominal subtype.
by:
At the place where a view of an object is defined, a nominal subtype is associated with the view. The nominal type of a view is the type of the nominal subtype of the view. The object's actual subtype (that is, its subtype) can be more restrictive than the nominal subtype of the view; it always is more restrictive if the nominal subtype is an indefinite subtype. A subtype is an indefinite subtype if it is an unconstrained array subtype, or if it has unknown discriminants or unconstrained discriminants without defaults (see 3.7); otherwise, the subtype is a definite subtype (all elementary subtypes are definite subtypes). A class-wide subtype is defined to have unknown discriminants, and is therefore an indefinite subtype. An indefinite subtype does not by itself provide enough information to create an object; an additional constraint or explicit initialization expression is necessary (see 3.3.1). A component cannot have an indefinite nominal subtype.
!corrigendum 3.9.1(4.1/2)
Insert after the paragraph:
A record extension is a null extension if its declaration has no known_discriminant_part and its record_extension_part includes no component_declarations.
the new paragraph:
In the case where the (compile-time) view of an object X is of a tagged type T1 or T1'Class and the (run-time) tag of X is T2'Tag, only the components (if any) of X that are components of T1 (or that are discriminants which correspond to a discriminant of T1) are said to be components of the nominal type of X. Similarly, only parts (respectively, subcomponents) of T1 are parts (respectively, subcomponents) of the nominal type of X.
!corrigendum 6.8(5/4)
!AI-0075-1
!AI-0191-1
@dinsa If the result subtype has one or more unconstrained access discriminants, the accessibility level of the anonymous access type of each access discriminant, as determined by the @fa<expression> or @fa<aggregate> of the @fa<expression_function_declaration>, shall not be statically deeper than that of the master that elaborated the @fa<expression_function_declaration>. @dinss Aspect Static shall be specified to have the value True only if the associated @fa<expression_function_declaration>: @xbullet<is not a completion;> @xbullet<has an @fa<expression> that is a potentially static expression;> @xbullet<contains no calls to itself;> @xbullet<each parameter (if any) is of mode @b<in> and is of a static subtype;> @xbullet<has a result subtype that is a static subtype;> @xbullet<has no applicable precondition or postcondition expression; and> @xbullet<for result type @i<R>, if the function is a boundary entity for type @i<R> (see 7.3.2), no type invariant applies to type @i<R>; if @i<R> has a component type @i<C>, a similar rule applies to @i<C>.>
!corrigendum 7.3.2(8/3)
Replace the paragraph:
If the Type_Invariant'Class aspect is specified for a tagged type T, then the invariant expression applies to all descendants of T.
by:
If the Type_Invariant'Class aspect is specified for a tagged type T, then a corresponding expression also applies to each nonabstract descendant T1 of T (including T itself if it is nonabstract).
For a nonabstract type T, a callable entity is said to be a boundary entity for T if it is declared within the immediate scope of T (or by an instance of a generic unit, and the generic is declared within the immediate scope of type T), or is the Read or Input stream-oriented attribute of type T, and either:
!corrigendum 7.3.2(10.1/4)
Replace the paragraph:
by:
!corrigendum 7.3.2(15/4)
Replace the paragraph:
by:
!corrigendum 7.3.2(17/4)
Replace the paragraph:
by:
!corrigendum 7.3.2(19/3)
Replace the paragraph:
by:
!corrigendum 13.13.2(9/3)
Replace the paragraph:
For elementary types, Read reads (and Write writes) the number of stream elements implied by the Stream_Size for the type T; the representation of those stream elements is implementation defined. For composite types, the Write or Read attribute for each component is called in canonical order, which is last dimension varying fastest for an array (unless the convention of the array is Fortran, in which case it is first dimension varying fastest), and positional aggregate order for a record. Bounds are not included in the stream if T is an array type. If T is a discriminated type, discriminants are included only if they have defaults. If T is a tagged type, the tag is not included. For type extensions, the Write or Read attribute for the parent type is called, followed by the Write or Read attribute of each component of the extension part, in canonical order. For a limited type extension, if the attribute of the parent type or any progenitor type of T is available anywhere within the immediate scope of T, and the attribute of the parent type or the type of any of the extension components is not available at the freezing point of T, then the attribute of T shall be directly specified.
by:
For elementary types, Read reads (and Write writes) the number of stream elements implied by the Stream_Size for the type T; the representation of those stream elements is implementation defined. For composite types, the Write or Read attribute for each component (excluding those, if any, that are not components of the nominal type of the object) is called in canonical order, which is last dimension varying fastest for an array (unless the convention of the array is Fortran, in which case it is first dimension varying fastest), and positional aggregate order for a record. Bounds are not included in the stream if T is an array type. If T is a discriminated type, discriminants are included only if they have defaults. If T is a tagged type, the tag is not included. For type extensions, the Write or Read attribute for the parent type is called, followed by the Write or Read attribute of each component of the extension part, in canonical order. For a limited type extension, if the attribute of the parent type or any progenitor type of T is available anywhere within the immediate scope of T, and the attribute of the parent type or the type of any of the extension components is not available at the freezing point of T, then the attribute of T shall be directly specified.
!ASIS
No ASIS effect.
!ACATS test
We could write a test to check that such components aren't checked (as in the example), but that doesn't seem to be very valuable.
!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.

****************************************************************

From: Jeff Cousins
Sent: Tuesday, August 23, 2016  9:34 AM

Thanks for looking into that Steve.  I think we have accepted that invariant
checking can't check everything all of the time, and is just providing a
limited number of check points.

****************************************************************

From: Steve Baird
Sent: Wednesday, February  6, 2019  7:18 PM

Here is some proposed wording for this AI, although I still have not gone 
through the RM with a fine-toothed comb reviewing each use of the terms 
"component", "subcomponent", and "part" with these issues in mind.

Many thanks to Randy for much helpful review, although (as usual) don't 
blame him for anything here that you don't like.

[This is version /02 of the AI - Editor.]

****************************************************************

From: Randy Brukardt
Sent: Wednesday, February  6, 2019  10:06 PM

> Here is some proposed wording for this AI, ...

>!discussion (in addition to existing !discussion section)
>
>The following wording ...

Ahem. !wording *precedes* any !discussion. I dropped the word "following".

Also:

> ... The current write-up of the AI uses "screened", ...

Ahem, the reader is currently reading the AI, so this is mostly noise. I 
replaced this with "We used "screened", ..."

>append after 3.1(7.d/3), continuing the AARM note

As I noted before (and in the formatting rules I posted to the list), this 
should read something like:

Add after AARM 3.1(7.d/3): [continuing the AARM note]

Similar comments apply to the rest of this wording section.

Otherwise, looks good.

****************************************************************

From: Steve Baird
Sent: Tuesday, February 12, 2019  7:32 PM

Here is another version of this AI, reflecting feedback received since the
previous version was distributed on Feb 6 2019, notably at the last phone 
meeting.

Two changes:
    1) The term "screened" has been replaced with "supplementary"
       throughout the AI as per the guidance of the group.

    2) The rules about which components are streamed in and out in
       the default implementations of 'Read and 'Write for a
       a tagged type are clarified.

[This is version /03 of the AI - Editor.]

****************************************************************

From: Tucker Taft
Sent: Tuesday, February 12, 2019  8:01 PM

The term "supplementary" is growing on me.  The !discussion should still 
come afterward.

I am somewhat worried we are combining the rules for class-wide objects
with the rules for "shortened" specific views of objects.  By "shortened" I 
mean a specific view of a type extension like T2 through a T1 "lens," where T1
is an ancestor of T2.  A class-wide view and a "shortened" view generally seem
to behave pretty differently.  For example on assignment, clearly you finalize 
the whole left-hand side in the case of a class-wide assignment, but for a 
"shortened" specific view, I would think the "supplementary" components are 
completely untouched as far as finalization and adjustment.  Is there really 
*any* case where for a shortened view, we touch the supplementary components?

For type invariants, we have an elaborate set of rules on type conversions, 
so that we start looking at the masked components (hmm -- "masked" vs. 
"supplementary"?) as we unwind the conversions.  But when you have the 
shortened view, you don't do anything with those supplementary/masked 
components.

****************************************************************

From: Tucker Taft
Sent: Tuesday, February 12, 2019  9:03 PM

How about "masked" vs. "unmasked" components?
Not sure if it is better...

****************************************************************

From: Steve Baird
Sent: Tuesday, February 12, 2019  9:12 PM

I prefer "masked" to "supplementary".

****************************************************************

From: Randy Brukardt
Sent: Tuesday, February 12, 2019  9:22 PM

Of course, if the concern is about implying something about visibility,
"screened" or "masked" certainly have that flavor, while "supplementary"
does not.

The correct flavor would be more like "unknown components", since they are 
completely unknown to the implementation at the interesting point. "Unknown"
doesn't appear in my thesaurus, someone else will have to look for 
alternatives to that...

****************************************************************

From: Randy Brukardt
Sent: Tuesday, February 12, 2019  9:29 PM

> I am somewhat worried we are combining the rules for class-wide 
> objects with the rules for "shortened" specific views of objects.  By 
> "shortened" I mean a specific view of a type extension like T2 through 
> a T1 "lens," where T1 is an ancestor of T2.  A class-wide view and a 
> "shortened" view generally seem to behave pretty differently.  For 
> example on assignment, clearly you finalize the whole left-hand side 
> in the case of a class-wide assignment, but for a "shortened"
> specific view, I would think the "supplementary" components are 
> completely untouched as far as finalization and adjustment.  Is there 
> really *any* case where for a shortened view, we touch the 
> supplementary components?

Dunno. I didn't know/remember that assignment isn't supposed to finalize such
components. I doubt that there is any ACATS test like that (assignments to 
[entire] tagged objects are rare in real code) -- I wonder if anyone gets that 
right?

> For type invariants, we have an elaborate set of rules on type 
> conversions, so that we start looking at the masked components (hmm -- 
> "masked" vs. "supplementary"?) as we unwind the conversions.  But when 
> you have the shortened view, you don't do anything with those 
> supplementary/masked components.

But specifically for type conversions, if you have a class-wide view (that 
is, T'Class) in the spec of an invariant-preserving , then you want to check 
the T components (only). That is what is different here, I think.

If that's not the case, then there's an argument that there never was a bug 
in the first place. That is, the (dynamic) components are *always* those of 
the view of the object (where the runtime view ignores any privacy). When 
one finalizes a stand-alone object or component of such an object, you always 
have the original view of that object/component, so of course you can see all 
of the subcomponents. And if you always see all of the components of a 
class-wide object, then QED (since that would cover any "interesting"
deallocations).

****************************************************************

From: Tucker Taft
Sent: Wednesday, February 13, 2019  11:02 AM

> But specifically for type conversions, if you have a class-wide view 
> (that is, T'Class) in the spec of an invariant-preserving , then you 
> want to check the T components (only). That is what is different here, I 
> think.

I am not convinced we have this right.  In my understanding of the intent, 
any class-wide object is presumed to satisfy all of its invariants.  Another 
way of thinking about it is when you create a class-wide object, you are 
effectively passing outside of the package barrier, and you must be sure the 
object satisfies all invariants that apply to it.

> If that's not the case, then there's an argument that there never was 
> a bug in the first place. That is, the (dynamic) components are 
> *always* those of the view of the object (where the runtime view 
> ignores any privacy). When one finalizes a stand-alone object or 
> component of such an object, you always have the original view of that 
> object/component, so of course you can see all of the subcomponents. 
> And if you always see all of the components of a class-wide object, then 
> QED (since that would cover any "interesting" deallocations).

Class-wide objects generally worry about all of their components.  The weird 
case is an object of a specific type, that was produced by doing a view 
conversion on an object with more components.  These are the real oddball 
guys, and we need to decide how these are to be handled.

****************************************************************

From: Steve Baird
Sent: Wednesday, February 13, 2019  12:29 PM

> For example on assignment, clearly you finalize the whole left-hand 
> side in the case of a class-wide assignment, but for a "shortened" 
> specific view, I would think the "supplementary" components are completely
> untouched as far as finalization and adjustment.

That's certainly true, but maybe this ought to be stated more clearly (perhaps 
in an AARM note) in the section on assignment statements. If we want to do 
that, that should probably be included in this AI.

> Is there really *any* case where for a shortened view, we touch the 
> supplementary components?
I can't think of any. The two cases that came to mind are finalization and 
the accessibility checks for access discriminants of a function result. But 
if the function result type is specific then there are no supplementary 
components of the function result object. And the cases where we get 
"shortened" views of longer objects (e.g., via parameter passing or 
View_Conversion'Access) are not cases where exiting a scope causes 
finalization of that shortened object.

****************************************************************

From: Tucker Taft
Sent: Wednesday, February 13, 2019  1:23 PM

>I am not convinced we have this right.  In my understanding of the intent, 
>any class-wide object is presumed to satisfy all of its invariants.  Another 
>way of thinking about it is when you create a class-wide object, you are 
>effectively passing outside of the package barrier, and you must be sure the 
>object satisfies all invariants that apply to it.

See AARM 7.3.2(20.a/4) for this "intent":

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.

****************************************************************

From: Randy Brukardt
Sent: Wednesday, February 13, 2019  3:50 PM

>See AARM 7.3.2(20.a/4) for this "intent":
>
>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.

This note is on class-wide types that are in the tree-of-T. These are 
invariants that the package reasonably could know about. 

But Steve has pointed out this also happens in the case of extensions of 
otherwise unrelated types that contain objects of T. This intent is not 
covered by any current invariant checks, since nothing class-wide related to T 
is involved.

In the somewhat pathological case that the body has sufficient visibility to 
such an extension to pass/assign it an unchecked T, preventing that requires 
a dispatching check. Or some other substantial change to the model.

Since this case requires contortions, we don't want to require implementations 
to check it, but would rather would describe it as a hole.
At least that has been my understanding.

Steve shows the case in interest in the e-mail:

  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;

I was thinking a case with an interface:

    package Pkg2 is
       type Has_Invariant is private;

       procedure Rely_On_Incoming_Invariant (Y : Has_Invariant);

       type Some_Interface is interface;
       procedure Munge (I : in out Some_Interface; Z : Has_Invariant) is abstract;

       procedure Oops (X : in out Some_Interface'Class);

    private
       type Has_Invariant is record Lo, Hi : Integer := 0; end record
	with Type_Invariant => (Has_Invariant.Lo <= Has_Invariant.Hi);
    end Pkg2;

    package body Pkg2 is
       procedure Break_It (Xx : out Has_Invariant) is
       begin
  	    Xx := (Lo => 1, Hi => 0);
       end;

       procedure Oops (X : in out Some_Interface'Class) is
          Bad : Has_Invariant;
       begin
          Break_It (Bad);
          X.Munge (Bad);
       end;
    end Pkg2;

Here, the implementation of Munge (which is not related at all to the package, 
and thus will not be checking any invariants) can save Bad into an extension 
of X. Oops in theory should be checking that part when it exits, but there is 
no way for that to happen short of there being a dispatching routine that 
knows about all of the components of each extension of Some_Interface. (Again, 
Some_Interface itself is not related to T in any way.)

---

I also note that the original question was about "parent part", and was posed 
by one Tucker Taft. I'm not sure why this matters (the "parent part" is not a
"part" in the technical sense of "object or its components"), but I can see 
why it would confuse.
 
****************************************************************

From: Randy Brukardt
Sent: Wednesday, February 13, 2019  6:25 PM

> Here, the implementation of Munge (which is not related at all to the 
> package, and thus will not be checking any
> invariants) can save Bad into an extension of X. Oops in theory should 
> be checking that part when it exits, but there is no way for that to 
> happen short of there being a dispatching routine that knows about all 
> of the components of each extension of Some_Interface. (Again, 
> Some_Interface itself is not related to T in any
> way.)

You might want to claim that Munge should check the invariant (inbound) because 
the dispatching is to an abstract routine that is itself "invariant-preserving".
I think that's arguable, but in any case, if we change Munge to a function, it 
becomes irrelevant (invariants of inbound "in" parameters of functions are 
never checked). (And even if the invariant is checked in the procedure case, 
the object X is modified before the failure, meaning that the "leak" has 
already happened.)

One could also create this case by using two interfaces, I1 and I2, with I2 a 
descendant of I1, I2 being in a separate package C1 and containing the Munge 
operation (which is therefore not invariant-preserving itself). If the body 
of the invariant-containing package Pkg2 withs C1, it can dispatch to the 
Munge operation, and again we can have a leak.

As with all permitted holes in invariant protection, this sort of issue 
requires active participation of the package containing the invariant, so 
there is no reason to pay the steep cost to fix it. But we also want to ensure 
that (A) no one thinks that they have to implement such a check; and
(B) that we include it in the list of holes. Both of these require a 
reasonable definition of what is *not* checked.

****************************************************************

From: Randy Brukardt
Sent: Wednesday, February 13, 2019   6:47 PM

...
> Of course, if the concern is about implying something about 
> visibility, "screened" or "masked" certainly have that flavor, while 
> "supplementary"
> does not.
> 
> The correct flavor would be more like "unknown components", since they 
> are completely unknown to the implementation at the interesting point. 
> "Unknown"
> doesn't appear in my thesaurus, someone else will have to look for 
> alternatives to that...

I just ran across a thesaurus in LibreOffice (never thought to look there),
and it is happy to give alternatives to "unknown":

"unmapped"
"unbeknownst"
"unheard-of"
"unacknowledged"
"unfamiliar"
"dishonorable" :-)
"unidentified"
"anonynous" (um, no.)
"unsuspected"
"obscure"
"unsung"
"terra incognita" :-) :-)
"stranger"
"alien"
"variable" (um, really no.)

I have some favorites here, both serious and not so serious. Not sure how the 
rest of us feel.

****************************************************************

From: Tullio Vardanega
Sent: Thursday, February 14, 2019  2:17 AM

Seems like "obscure", to me.

****************************************************************

From: Tucker Taft
Sent: Thursday, February 14, 2019  7:39 AM

Here are two other pairs:

   *Overt* components, and *latent* components, of the current view.

   Components *included* in the current view, components *excluded* from the 
   current view.

I think it is worth using the term "view" when talking about this distinction, 
because it really is all about the view, not about the underlying object.

****************************************************************

From: Edmond Schonberg
Sent: Thursday, February 14, 2019  9:43 AM

“Overt” seems perfect. Maybe “implicit” instead of latent?

****************************************************************

From: Jean-Pierre Rosen
Sent: Thursday, February 14, 2019  9:54 AM

> I think it is worth using the term "view" when talking about this 
> distinction, because it really is all about the view, not about the 
> underlying object.

Agreed, but if a full phrase is acceptable, then "components that are/are not
part of the current view" would exactly describe what we mean.

****************************************************************

From: Tucker Taft
Sent: Thursday, February 14, 2019  11:16 AM

>“Overt” seems perfect. Maybe “implicit” instead of latent?

Alas, Ada already refers to the "implicit" components of a task or protected 
object, to represent entry queues.  And implicit is already pretty heavily 
used for "implicit declarations" of inherited operations.  I like "latent" in 
the sense of a "latent talent."  It is there, but it just hasn't yet been 
brought forward.

****************************************************************

From: Steve Baird
Sent: Thursday, February 14, 2019  11:54 AM

I agree.

I don't think an antonym of "active" would be confusing even though we already 
have active priorities, active partitions, active locales, and active tasks.

Interestingly, a variant part does not have an active variant; other 
terminology was used for that.

****************************************************************

From: Tucker Taft
Sent: Thursday, February 14, 2019  12:52 PM

Yes.  Let's leave "active" for something relating to tasks.

****************************************************************

From: Gary Dismukes
Sent: Thursday, February 14, 2019  12:49 PM

> Alas, Ada already refers to the "implicit" components of a task or protected 
> object, to represent entry queues.  And implicit is already pretty heavily 
> used for "implicit declarations" of inherited operations.  I like "latent" 
> in the sense of a "latent talent."  It is there, but it just hasn't yet been
> brought forward.

I had thought of mentioning "latent" at the meeting (as well as "concealed"), 
but didn't because it seemed to have too much of the sense of hidden, which 
was objected to.  I would be OK with that choice, but J-P's suggestion along 
the lines of "components that are part of the current view" seems reasonable, 
and would avoid the need to introduce another new term.

****************************************************************

From: Tucker Taft
Sent: Thursday, February 14, 2019  1:24 PM

> I had thought of mentioning "latent" at the meeting (as well as 
> "concealed"), but didn't because it seemed to have too much of the 
> sense of hidden, which was objected to.

"Latent" doesn't imply any sort of hiding in my view.  It just means it hasn't
been recognized yet.

> I would be OK with that choice, but J-P's suggestion along the lines 
> of "components that are part of the current view" seems reasonable, 
> and would avoid the need to introduce another new term.

I agree, it may be that if we use the term "current view" explicitly, that 
everything will be quite clear -- "part of the current view," "a component of 
the current view," etc. all seem pretty clear.

****************************************************************

From: Steve Baird
Sent: Thursday, February 14, 2019  3:22 PM

> I agree, it may be that if we use the term "current view" explicitly, that 
> everything will be quite clear -- "part of the current view," "a component 
> of the current view," etc. all seem pretty clear.

I'll take another look at the AI with this approach in mind.

****************************************************************

From: Steve Baird
Sent: Thursday, February 21, 2019  9:56 PM

I have attached two versions of this AI using the approach suggested by 
Jean-Pierre that Tuck referred to above.

I like the idea of using a phrase instead of a single word to capture the 
property in question, but I don't like the suggested phrase.

Nonetheless, in the attached v3 version (which I do not endorse) I used the 
suggested phrase.

[This is version /04 of the AI - Editor.]

It seems wrong to say that (by definition!) in a situation like

    package P1 is
       type T1 is private with Type_Invariant => ... ;

       package P2 is
         type T2 is private;
       private
         type T2 is record T1_Comp : T1; end record;
       end P1;

       procedure Foo (X : out P2.T2);
    private
       ...
    end P1;

when we are deciding what type invariant checks to perform as part of a return
from Foo, X.T2 is a component of the view of X.

To me, it seems clear that if we are at a point when we can see only the 
partial view of P2.T2, then saying that X.T2 is a component of the view of X 
will lead to confusion or worse.

So I used a different phrase in the attached v4 variant ("hidden by the 
nominal tag").

[This is version /05 of the AI - Editor.]

That's the one I endorse, although others might suggest better phrases now 
that we seem to have given up on single words like "latent" or "screened".

****************************************************************

From: Tucker Taft
Sent: Friday, February 22, 2019  11:49 AM

...
> when we are deciding what type invariant checks to perform as part of 
> a return from Foo, X.T2 is a component of the view of X.

I presume you meant "T1 is a component of the view of X."  And yes, I can see 
how partial views and the notion of "view" inherent in a "view conversion" 
could get confused with one another.
 
> To me, it seems clear that if we are at a point when we can see only 
> the partial view of P2.T2, then saying that X.T2 is a component of the 
> view of X will lead to confusion or worse.

Again, I presume you meant "... saying that T1 is a component of the view of 
X will lead ..."
 
> So I used a different phrase in the attached v4 variant ("hidden by 
> the nominal tag").

Hmm..  You are bringing back the notion of "hiding" and introducing the 
notion of a "nominal tag."  "Nominal tag" seems like a strange combination, 
because the tag is a run-time concept and never changes in the lifetime of 
the object.  I could see using the term "nominal type" where "nominal" is what 
is expressing the notion of "view," and "type" is what determines what 
components are relevant.  So I would suggest "part of the nominal type" or 
"components of the nominal type" both of which seem unambiguous.

****************************************************************

From: Steve Baird
Sent: Friday, February 22, 2019  11:58 AM

>    So I would suggest "part of the nominal type" or "components of the 
> nominal type" both of which seem unambiguous.

Sounds good to me.

I'll try to produce a version using this phrasing.

****************************************************************

From: Steve Baird
Sent: Friday, February 22, 2019  2:59 PM

See attached. [This is version /06 of the AI - Editor.]

This still suffers from the same problem I complained about (and thanks, Tuck, 
for deciphering the typos in my complaint) with the "part of the current view" 
phrasing (that was version v3).
That is, there seems to be some misleading (at best) confusion with 
visibility/privacy rules, but this seems slightly better than that earlier v3 
version.

****************************************************************

From: Tucker Taft
Sent: Friday, February 22, 2019  3:21 PM

Another confusion, at least for me, is sometimes we say "a part of type T" and
it is not clear whether we mean "a part *having* the type T" or a "part of 
some object O where O is of type T."

I wonder whether we could simplify the phraseology a bit further, as sentences 
like this:

  "... the check is performed on the part(s) of type T that are
    parts of the nominal type of the object..."

with:

    "... the check is performed on the part(s) of the nominal type of the
   object that have type T ..."

****************************************************************

From: Steve Baird
Sent: Friday, February 22, 2019  5:03 PM

I agree, that is clearer.

It is past the homework deadline, but I'll try to incorporate this approach.

****************************************************************

From: Randy Brukardt
Sent: Friday, February 22, 2019   5:21 PM

I still have to file all of the previous attempts on this topic, so you 
probably have an hour or a bit more.

****************************************************************

From: Steve Baird
Sent: Friday, February 22, 2019  5:53 PM

See attached. [This is version /07 of the AI - Editor.]

****************************************************************

From: Tucker Taft
Sent: Saturday, February 23, 2019  6:57 AM

Looks good in general.  I wonder about the new normative wording after 
3.9.1(4.1/2).  The first sentence uses a double negative, and the illustrative 
example doesn't read quite like normal normative RM text, and might better be 
an AARM note.  Currently you propose:

append after 3.9.1(4.1/2) (i.e., at the end of the Static Semantics section):

  In the case where the (compile time) view of an object X is of a
  tagged type T1 or T1'Class and the (runtime) tag of X is T2'Tag,
  the components (if any) of X which are not components of T1
  (and which are not discriminants which correspond to a discriminant
  of T1) are said to not be "components of the nominal type" of the object.
  For example, if T2 is an
  undiscriminated extension of T1 which declares a component named Comp,
  then X.Comp is not a component of the nominal type of X.
  Similarly, a part (respectively, subcomponent) of an object might or might
  not be a part (respectively, subcomponent) of the nominal type of
  the object.

Here is a possible re-wording:

  In the case where the (compile-time) view of an object X is of a
  tagged type T1 or T1'Class and the (run-time) tag of X is T2'Tag,
  only the components (if any) of X that are components of T1
  (or that are discriminants which correspond to a discriminant
  of T1) are said to be "components of the nominal type" of X.
  Similarly, only parts (respectively, subcomponents) of T1 are parts
  (respectively, subcomponents) of the nominal type of X.

     AARM Ramification:   For example, if T2 is an
     undiscriminated extension of T1 which declares a component named Comp,
     then X.Comp is not a component of the nominal type of X.

****************************************************************

From: Steve Baird
Sent: Monday, February 25, 2019  1:08 PM

I like it, and I agree that getting rid of the double negatives is a 
significant improvement.

****************************************************************

From: Randy Brukardt
Sent: Monday, February 25, 2019  8:10 PM

Sigh. OK, I've posted an update [/08 of the AI] with this wording for
discussion tomorrow.

****************************************************************

From: Randy Brukardt
Sent: Friday, May 10, 2019  7:25 PM

I was asked to research the uses of the term "nominal type" in the RM and 
AARM, and check that they are compatible with the proposed definition:

    The *nominal type* of a view is the type of the nominal subtype of the 
    view.

The search engine finds only two uses in AARM notes:

4.3.4(14.b/5):
   This requires that the underlying tag (if any) associated with the 
   delta_aggregate is that of the base_expression in the delta_aggregate and 
   not that of the nominal type of the base_expression in the delta_aggregate.

6.1.1(26.b/4):
   This means that the underlying tag associated with X'Old is that of X and 
   not that of the nominal type of X. 

These are compatible with the proposed definition. I note in passing that both 
of these notes are in areas that Steve Baird was a primary author of, as was 
the case of this AI. I detect a pattern. :-)

****************************************************************

From: Randy Brukardt
Sent: Tuesday, May 14, 2019  1:51 AM

One of the wording changes of AI12-0191-1 is:

* Upon successful return from a call on any subprogram or entry which is
  type-invariant preserving for T, an invariant check is
  performed on each part of {the nominal type of the object that has}
  type T which is subject to an invariant check for T.  ...

"*the* object"??? We're talking about a call, and suddenly "the object"
appears out of nowhere. The original wording carefully avoided talking about
specific objects, probably because the pile of bullets calling out what is 
subject to invariant checks is massive. On top of which, there's very likely
to be multiple objects here, so "the" is wrong in any case.

We're probably talking about some object that is "subject to an invariant 
check", so perhaps we need to say that somehow:

* Upon successful return from a call on any subprogram or entry which is
  type-invariant preserving for T, an invariant check is
  performed on each object which is subject to an invariant check for T
  for each part of the nominal type of the object that has type T .  ...

However, this is all rather bogus, since the entire point of the "part of the 
nominal type of the object" rule is that such parts are *not* subject to an 
invariant check. Indeed, it seems bizarre to say such parts are subject to a
check and then essentially erase that check at the last instant. You could 
even imagine cases where  entire subprograms qualify as type-invariant 
preserving only because of components that aren't even known at compile-time. 
That seems completely wrong.

So I'm thinking that this wording change is applied in the wrong place
(7.3.2(15/5) rather than 7.3.2 (8.8-8.11/5). I could even make the argument 
that since 7.3.2(8.8-8.11/5) is labeled as a "static semantics" rule, there's
no issue in the first place: the parts talked about in 7.3.2(8.8-8.11/5) are 
clearly compile-time views [that is, "parts of the nominal type"] and other 
parts aren't "subject to an invariant check" in the first place (regardless 
of if they have a part of T). (Note that the rewording of 7.3.2(8.8-8.11/5) 
probably happened after AI12-0191-1 was opened, so this later rewording 
inadvertently fixed the AI-191's issue.)

So the easiest fix is to completely eliminate the change to 7.3.2(15/5), and 
then just fix up the existing AARM note (probably reclassifying as a
Ramification):

Invariant checks are only performed on parts of the nominal type of objects.
We don't have to say that for calls, since the objects that are "subject to 
an invariant check" are determined at compile-time (as the appropriate rules
are Static Semantic rules), and parts not known at compile-time (that is, 
those not parts of the nominal type) are never subject to an invariant check.
This is preferable anyway, as we don't want overhead associated with the 
possibility that there *might* exist an extension of a tagged type that has 
a part of type T. (See the "leaks" note below for avoidance advice.)

[Note: The "holes" AARM note needs to be updated to mention this hole, but 
there is a complete overhaul of that note proposed in AI12-0210-1 (including
talking about "leaks" rather than "holes}. We were supposed to discuss these
two AIs together (since they're related), but we ran out of time before doing
that. And I just noticed that that AI used "screened" several times.
So I just updated it.]

Thoughts on this wording? 

****************************************************************

From: Jean-Pierre Rosen
Sent: Tuesday, May 14, 2019  4:03 AM

> call on any subprogram or entry
Nitpicking: isn't "callable entity" the official term rather than "subprogram 
or entry" ?

****************************************************************

From: Steve Baird
Sent: Tuesday, May 14, 2019  8:11 PM

...
> Thoughts on this wording?

Makes sense.

An object which is "subject to an invariant check for T" is known to be of 
type T (this follows from the definition of the term).

So could we eliminate the "of type T" qualifier in the "Upon successful return
from a call" paragraph on the grounds that it is redundant?
This would leave us with

   Upon successful return from a call on any subprogram or entry which is
   type-invariant preserving for T, an invariant check is performed on
   each object that is subject to an invariant check for T.

It's always nice to eliminate wording like "a part of type T" because, 
strictly speaking, there is an ambiguity there (even if the resolution is 
"obvious").

****************************************************************

Questions? Ask the ACAA Technical Agent