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

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

!standard 7.3.2(5/4)          16-11-14 AI12-0199-1/03
!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 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)
Replace the paragraph:
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) 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.
by:
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.
!corrigendum 7.3.2(8/3)
Replace the paragraph:
If the Type_Invariant'Class aspect is specified for a tagged type T, then the invariant expression applies to all descendants of T.
by:
If the Type_Invariant'Class aspect is specified for a tagged type T, then a /corresponding expression/ also applies to each nonabstract descendant T1 of T (including T itself if it is nonabstract). The corresponding expression is constructed from the associated expression as follows:
!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.

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


Questions? Ask the ACAA Technical Agent