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

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

!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.

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

Questions? Ask the ACAA Technical Agent