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

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

!standard 7.3.2(6/3)          12-11-29 AI12-0042-1/01
!class binding interpretation 12-11-29
!status work item 12-11-29
!status received 12-04-09
!priority Medium
!difficulty Medium
!subject Type invariants cannot be inherited by non-private extensions
!summary
A record extension whose ancestor has a Type_Invariant'Class specified is illegal.
!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_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.
!discussion
Type invariants were designed assuming that they only apply to private types declared in packages. That is necessary to have any sort of safety associated with them -- if they can apply to non-private types, pretty much anything can cause the invariant to be violated. On the other hand, 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. [Truth in advertising - the package designer can introduce holes in rare cases; but these are easily avoided.]
It's too early in the life of Ada 2012 to be abandoning the model of type invariants (or any other model, for that matter) [Note: this is being written in November 2012]. Thus, it is best to make the simplest fix that preserves the model.
This rule doesn't introduce a generic contract problems, as extensions from generic formal types are prohibited in generic bodies for other reasons (see 3.9.1(4)).
The part about completions exists simply so that the completions of private extensions aren't illegal. (It also serves to prevent "hidden class-wide invariants", which would make enforcing the rule problematical.)
[Should we define the term "class-wide invariant", it might make this wording a bit easier?]
This rule is not incompatible with any existing (Ada 2005 or before) code; it only affects users of Type_Invariant'Class.
!ACATS test
An ACATS B-Test should be created to test this rule.
!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.

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


Questions? Ask the ACAA Technical Agent