Version 1.2 of ai12s/ai12-0133-1.txt

Unformatted version of ai12s/ai12-0133-1.txt version 1.2
Other versions for file ai12s/ai12-0133-1.txt

!standard 7.3.2(10.3/3)          14-10-13 AI05-0133-1/02
!class binding interpretation 14-10-09
!status work item 14-10-09
!status received 14-08-28
!priority Low
!difficulty Easy
!qualifier Clarification
!subject Type invariants and default initialized objects
Type invariants are checked on all objects of the type that are initialized by default.
7.3.2(10/3) talks of "default initialization" which isn't obviously defined (it's not in the index of the Standard). Was "initialized by default" intended? (Yes?)
Typically, invariant checks are not made on objects declared within the package body. But 7.3.2(10/3) has no such exception. That means that temporary objects and <> in aggregates are at risk of Assertion_Error even in the body. Is this intended? (Yes??)
(See Summary.)
Modify 7.3.2(10/3):
After successful [default] initialization of an object of type T that{ is initialized by default (see 3.3.1)}, the check is performed on the new object;
The term "default initialization" is not defined. It makes more sense to to use a defined term.
Note that this assumes that the rule was intended to apply to all objects initialized by default (including <> components of aggregates, components of larger objects, stand-alone objects, etc.). If the rule was only intended to apply to object declarations, then it needs rewording.
The author had some concern about the ordering rules that get dragged along with "initialized by default". However, those aren't a problem here, because this wording only applies "after initialization", and all of the ordering issues will have been sorted out first.
For the second question, we believe that no special exception is needed. Default initialization of a type is the same inside or outside of a unit, so it needs to pass the checks no matter where it occurs. As such, the rule is simplified by having it apply everywhere. As such, we make no change.
However, the author is dubious of this rationale. (He isn't willing to try to reword this rule to make a body exception, so he came up with the best rationale for no change possible. :-) If the private type with a type invariant has unknown discriminants, then no default initialization is allowed outside of the package. In that case, checking the invariant could only happen inside the package, which makes no sense (and could make it difficult to construct objects as default initialized objects and components could raise Assertion_Error).
Less likely is the case where Assertion_Error is raised by some but not all possible discriminant values.
Perhaps all we ought to do is except default initialized objects if the partial view has unknown discriminants?
package P is type T (<>) is private; function Make (Val : Integer) return T; private type T is record A : access Integer := null; end record with Type_Invariant => Is_OK(T); function Is_OK (Obj : T) return Boolean is (Obj.A /= null); end P;
package body P is -- Declare a linked list node: type Node; type Ptr is access Node; type Node is record C : T; N : Ptr; end record;
function Make (Val : Integer) return T is begin if Val = 1 then declare Temp : T; -- Raises Assertion_Error during default init. begin Temp.A := new Integer'(1); return Temp; end; elsif Val = 2 then return Foo : T := (A => <>) do -- OK, no exception. Foo.A := new Integer'(Val); end return; else -- The following structure is likely if there is a linked list -- in the body (although it would probably be in some other -- subprogram): declare N : Node := (C => <>, N => null); -- Raises Assertion_Error. begin N.C.A := new Integer'(Val); return N.C; end; end if; end Make; end P;
Neither of the places where "Raises Assertion_Error" should do so, since they're inside of the package and are just constructing values to return.
No ASIS effect.
!ACATS test
This should be tested in the ACATS test that checks that 7.3.2(10/3) is implemented; a separate test is not needed.

[Privately] From: Jeff Cousins
Sent: Monday, October 13, 2014  6:26 AM

When I first tried using a type invariant, I assumed that "default
initialization" just meant objects whose subtype declarations are such as:

type Complex is record
   Re : Float := 0.0;
   Im : Float := 0.0;
end record;


subtype Day is Integer range 1 .. 31
 with Default_Value => 0;

It was AdaCore who claimed that it meant "initialized by default" as described
in 3.3.1.

But I shouldn't just be taking their word for it, as you say it requires

But either way, I'm surprised that there's no exclusion to say that it doesn't
apply within the body of the package that defines the type, as the
Introduction to the Rationale says:
"Note that any subprograms internal to the package and not visible to the
user can do what they like. It is only when a value of the type Stack emerges
into the outside world that the invariant is checked."
It seems bizarre to me that within the package body the programmer can declare
an object of the type with explicit initialisation to a known invalid value
and not get an Assertion_Error, but can't declare an object of the type
without explicit initialisation without getting an invariant check.


[Privately] From: Randy Brukardt
Sent: Monday, October 13, 2014  6:01 PM

I'd guess that's because one uses the same default initialization inside the
package as outside, so it doesn't make much sense for it not to work -- and it
makes the rule easier to state (and probably implement) this way.

But I don't totally buy this rationale. The default initialization can depend
on discriminants, so an inside usage could fail. And of course the bounding
case is when the public view has unknown discriminants and it's not possible
for a default initialized object to be created outside of the body. So I think
you are right that there ought to be some exclusion.

I've appended your quoted mail and this reply to the AI so we can consider
this point as well as your original point.


Questions? Ask the ACAA Technical Agent