!standard 7.3.2(5/4) 17-04-20 AI12-0199-1/04
!standard 7.3.2(8/3)
!class binding interpretation 16-07-21
!status Amendment 1-2012 16-11-14
!status ARG Approved 7-0-2 16-10-09
!status work item 16-07-21
!status received 16-06-11
!priority Low
!difficulty Hard
!qualifier Omission
!subject Abstract subprogram calls in class-wide invariant expressions
!summary
Class-wide type invariants do not apply to abstract types, to avoid various
problems. Define the notion of a "corresponding expression" for a class-wide
type invariant, replacing references to components as appropriate, taking into
account rules for corresponding and specified discriminants when applying them
to a nonabstract descendant.
!question
Consider:
package Pkg is
type Ifc is interface
with Type_Invariant'Class => F1 (Ifc);
function F1 (X : Ifc) return Boolean is abstract;
end Pkg;
Does the call to F1 violate the rule against nondispatching calls to abstract
subprograms?
(No, because the aspect is reinterpreted using notional, nonabstract
descendant)
!recommendation
(See Summary.)
!wording
Modify 7.3.2(5/4):
Within an invariant expression, the identifier of the first subtype of
the associated type denotes the current instance of the type. Within
an invariant expression for the Type_Invariant aspect of a type T, the
type of this current instance is T. Within an invariant expression for
the Type_Invariant'Class aspect of a type T, the type of this current
instance is interpreted as though it had a (notional) {nonabstract}
type NT that is a visible formal derived type whose ancestor type is
T. The effect of this interpretation is that the only operations that
can be applied to this current instance are those defined for such a
formal derived type.
Modify 7.3.2(8/3):
If the Type_Invariant'Class aspect is specified for a tagged type T,
then [the invariant expression applies to all descendants of T] {a
/corresponding expression/ also applies to each nonabstract
descendant T1 of T [(including T itself if it is nonabstract)]}. {The
corresponding expression is constructed from the associated expression
as follows:
* References to non-discriminant components of T (or to T itself) are
replaced with references to the corresponding components of T1 (or
to T1 as a whole).
AARM Ramification: The only nondiscriminant components visible at the
point of such an aspect specification are necessarily inherited from some
nonprivate ancestor.
* References to discriminants of T are replaced with references to the
corresponding discriminant of T1, or to the specified
value for the discriminant, if the discriminant is specified by the
derived_type_definition for some type that is an ancestor of T1 and
a descendant of T (see 3.7).}
!discussion
For simplicity, we say that class-wide type invariants only apply to
nonabstract types. For an abstract type, no type invariant checks are
performed, nor should the type invariant expression be presumed true.
This AI provides rules for class-wide type invariants analogous to those
for class-wide pre- and postconditions found in 6.1.1(18-18.2/4). In
particular, we define the "corresponding expression", taking into
account components which are directly visible in this expression as well
as the type name itself.
We avoid the need for a rule like 6.1.1(18.2/4), by saying that
class-wide type invariants do not apply to abstract types. Otherwise,
the Bairdian example could be constructed for this case as well:
package Pkg2 is
type T is tagged null record
with Type_Invariant'Class => Is_OK (X);
function Is_Ok (X : T) return Boolean;
procedure Proc (X : in out T);
end Pkg2;
If we allowed class-wide type invariants to apply to abstract types,
then a call on Proc would make invariant checks on the value of X.
with Pkg2;
package Pkg3 is
type NT is abstract new Pkg2.T with null record;
-- inherits Type_Invariant'Class => Is_OK (X);
function Is_Ok (X : NT) return Boolean is abstract;
-- inherits Proc.
end Pkg3;
If the call on the (concrete) inherited Proc were required to make
invariant checks, it would call the abstract Is_OK, which wouldn't work.
Note that a statically bound call on Pkg3.Proc can be created by type
converting an object of a type that is a descendant of NT to the type NT.
This approach of not applying class-wide invariants to abstract types also
eliminates problems associated with type conversions to or across
abstract types, and so on.
!corrigendum 7.3.2(5/4)
@drepl
Within an invariant expression, the identifier of
the first subtype of the associated type denotes the current instance
of the type. Within an invariant expression for the Type_Invariant aspect
of a type @i, the type of this current instance is @i. Within
an invariant expression for the Type_Invariant'Class aspect of a type
@i, the type of this current instance is interpreted as though it
had a (notional) type @i that is a visible formal derived type whose
ancestor type is @i. The effect of this interpretation is that the
only operations that can be applied to this
current instance are those defined for such a formal derived type.
@dby
Within an invariant expression, the identifier of
the first subtype of the associated type denotes the current instance
of the type. Within an invariant expression for the Type_Invariant aspect
of a type @i, the type of this current instance is @i. Within
an invariant expression for the Type_Invariant'Class aspect of a type
@i, the type of this current instance is interpreted as though it
had a (notional) nonabstract type @i that is a visible formal derived
type whose ancestor type is @i. The effect of this interpretation is that
the only operations that can be applied to this
current instance are those defined for such a formal derived type.
!corrigendum 7.3.2(8/3)
@drepl
If the Type_Invariant'Class aspect is specified for a tagged type @i,
then the invariant expression applies to all descendants of @i.
@dby
If the Type_Invariant'Class aspect is specified for a tagged type @i,
then a @i also applies to each nonabstract
descendant @i of @i (including @i itself if it is nonabstract).
The corresponding expression is constructed from the associated expression
as follows:
@xbullet (or to @i
itself) are replaced with references to the corresponding components of @i
(or to @i as a whole).>
@xbullet are replaced with references to
the corresponding discriminant of @i, or to the specified value for the
discriminant, if the discriminant is specified by the
@fa for some type that is an ancestor of @i and
a descendant of @i (see 3.7).>
!ASIS
No ASIS effect.
!ACATS test
An ACATS B-Test should be created to check the examples (if they aren't
already covered).
!appendix
From: Randy Brukardt
Sent: Thursday, July 21, 2016 8:04 PM
In creating the mostly empty template for this AI from the type invariant part
of AI12-0170-1, I have some rather pithy thoughts on the problem that I thought
I would share, in large part because we probably need some Bairdian examples in
order to chose a rule (Luckily, this AI isn't assigned to me, so I don't have
to come up with a rule.)
The basic problem is that we have two conflicting requirements:
(1) We want to be able to specify class-wide type invariants on abstract
(tagged) types. Otherwise, it wouldn't be possible to define an invariant for
an interface, and we definitely wanted to do that enough that we have a
separate AI for the purpose.
This would look like:
package Pkg is
type Ifc is interface
with Type_Invariant'Class => F1 (Ifc); -- Better be legal.
function F1 (X : Ifc) return Boolean is abstract;
end Pkg;
(2) But it cannot be the case that an actual class-wide type invariant check
calls an abstract function (for obvious reasons).
I can show the problem for the second by using a modification of Steve's
original precondition example:
package Pkg2 is
type T is tagged null record
with Type_Invariant'Class => Is_OK (X); -- OK.
function Is_Ok (X : T) return Boolean;
procedure Proc (X : in out T);
end Pkg2;
A call on Proc will make invariant checks on the value of X.
with Pkg2;
package Pkg3 is
type NT is abstract new Pkg2.T null record;
-- inherits Type_Invariant'Class => Is_OK (X); -- ??
function Is_Ok (X : NT) return Boolean is abstract;
-- inherits Proc.
end Pkg3;
A call like:
Pkg3.Proc (Pkg3.NT(Obj));
is legal and raises no exceptions if Obj has a concrete type that is
descended from type NT. But in this case, we will make a class-wide type
invariant check that will call Pkg3.Is_OK, which is abstract. Bang!
(Note that abstract subprograms can only be written on abstract types in this
case, so we do have some limits.)
The straighforward version of the 6.1.1(18.2/4) rule would be something like:
A nonabstract type T is illegal if corresponding expression for a
Type_Invariant'Class or Post'Class aspect would be illegal.
But that doesn't fix the bug (NT is abstract in the example above). And
dropping "nonabstract" runs afoul of (1) above: it would make all invariants
of interfaces illegal.
It seems easy enough to craft a rule to plug this particular bug:
If the corresponding class-wide invariant expression for an abstract type
T contains a call to an abstract routine, then there cannot be any
nonabstract subprograms in the immediately enclosing scope (including in
nested scopes) that have a parameter with a part of T.
But that has issues:
* It only covers one possible way for a type invariant check to be triggered.
There are 21 paragraphs regarding such checks! I especially worry about the
view conversion checks.
* It doesn't cover any future issues, like 6.1.1(18.2/4) does. If we discover
an example of a problem with accessibility of a coextension, 6.1.1(18.2/4)
will cover it, as it just talks about the legality of the expression. The
above only covers calling abstract routines.
Luckily, I don't have to solve this problem, Tucker does. ;-) And I'm sure
Steve can cook up some juicy new problems.
At least type invariants are much less useful than the 3 P's, so any loss of
functionality will hardly be noticed.
****************************************************************
From: Tucker Taft
Sent: Wednesday, October 5, 2016 12:12 AM
Here is the first real version of AI2-0199, which was spun off from AI12-0170.
[This is version /02 of the AI - Editor.] The main concern was how class-wide
type invariants interacted with abstract subprograms. I took the simple way out
-- class-wide type invariants don't apply to abstract types. They only apply to
non-abstract descendants.
****************************************************************