7.3.3 Default Initial Conditions
For a private type
or private extension (including a generic formal type), the following
language-defined assertion aspect may be specified with an aspect_specification
This aspect shall be specified by an expression
called a default initial condition expression
may be specified on a private_type_declaration
or a formal_derived_type_definition
aspect is not inherited, but its effects are additive, as defined below.
Name Resolution Rules
The expected type for a default initial condition
expression is any boolean type.
Within a default initial condition expression associated
with a declaration for a type T, a name that denotes the declaration
is interpreted as a current instance of a notional (nonabstract) formal
derived type NT with ancestor T, that has directly visible primitive
The Default_Initial_Condition aspect shall not be
specified for a type whose partial view has unknown discriminants, whether
explicitly declared or inherited.
If the Default_Initial_Condition aspect is specified
for a type T, then the default initial condition expression applies to
T and to all descendants of T.
If one or more default initial condition expressions
apply to a (nonabstract) type T, then a default initial condition check
is performed after successful initialization of an object of type T by
default (see 3.3.1
). In the case of a controlled
type, the check is performed after the call to the type's Initialize
procedure (see 7.6
If performing checks is required by the Default_Initial_Condition
assertion policy (see 11.4.2
) in effect
at the point of the corresponding aspect_specification
applicable to a given type, then the respective default initial condition
expression is considered enabled.
The default initial condition check consists of the
evaluation of each enabled default initial condition expression that
applies to T. Any operations within such an expression that were resolved
as primitive operations of the (notional) formal derived type NT, are
in the evaluation of the expression resolved as for a formal derived
type in an instance with T as the actual type for NT (see 12.5.1
These evaluations, if there are more than one, are performed in an arbitrary
order. If any of these evaluate to False, Assertions.Assertion_Error
is raised at the point of the object initialization.
For a generic formal type T, default initial condition
checks performed are as determined by the actual type, along with any
default initial condition of the formal type itself.
Implementations may extend the syntax or semantics
of the Default_Initial_Condition aspect in an implementation-defined
NOTE For an example of the use of
this aspect, see the Vector container definition in A.18.2
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe