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

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

!standard 7.3.2(10.3/3)          15-01-19 AI12-0133-1/04
!class binding interpretation 14-10-09
!status Corrigendum 1-2012 14-11-13
!status WG9 Approved 15-06-26
!status ARG Approved 7-0-1 14-10-18
!status work item 14-10-09
!status received 14-08-28
!priority Low
!difficulty Easy
!qualifier Clarification
!subject Type invariants and default initialized objects
!summary
Type invariants are checked on all objects of the type that are initialized by default.
!question
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.)
!recommendation
(See Summary.)
!wording
Modify 7.3.2(10/3):
After successful [default] initialization of an object of type T{ by default (see 3.3.1)}, the check is performed on the new object{ unless the partial view of T has unknown discriminants};
AARM Reason: The check applies everywhere, even in the package body, because default initialization has to work the same for clients as it does within the package. As such, checks within the package are either harmless or will uncover a bug that could also happen to a client. However, if the partial view of the type has unknown discriminants, no client of the package can declare a default-initialized object. Therefore, no invariant check is needed, as all default initialized objects are necessarily inside the package.
!discussion
The term "default initialization" is not defined. It makes more sense to to use a defined term. That ensures that it applies to all objects initialized by default (including <> components of aggregates, components of larger objects, stand-alone objects, etc.).
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, normally it does not matter whether or not it is checked within the package. 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.
However, if the private type with a type invariant has unknown discriminants, then no default initialization is allowed outside 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). Therefore, we add an exception specifically for this case.
Example of possible issues if a type with unknown discriminants is checked:
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; -- No check here. If there was one, the check would -- fail and raise 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 whether or not -- a check is made. 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); -- No check here. If there was -- one, the check would fail and raise Assertion_Error. begin N.C.A := new Integer'(Val); return N.C; end; end if; end Make; end P;
Neither of the places marked "no check here" should have a check, since they're inside of the package and are just constructing values to return to the client.
!corrigendum 7.3.2(10/3)
Replace the paragraph:
by:
!ASIS
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. The test should include an example like the one in the Discussion that no check is made for a private type with unknown discrimiants.
!appendix

[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;

and

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
clarification.

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