Version 1.16 of ai12s/ai12-0042-1.txt

Unformatted version of ai12s/ai12-0042-1.txt version 1.16
Other versions for file ai12s/ai12-0042-1.txt

!standard 7.3.2(6/3)          14-07-22 AI12-0042-1/10
!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 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 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. In each of these cases, the visible components can be modified independent of the package boundaries, which could make the invariant False. 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 independent 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 its 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)
Insert after the paragraph:
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.
the new paragraph:
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)
Replace the paragraph:
by:
!corrigendum 7.3.2(18/3)
Delete the paragraph:
!corrigendum 7.3.2(19/3)
Replace the paragraph:
by:
!corrigendum 7.3.2(20/3)
Insert after the paragraph:
The check is performed on each such part of type T.
the new paragraph:
!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]

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


Questions? Ask the ACAA Technical Agent