7.3.3 Default Initial Conditions
This aspect shall be specified by an expression,
called a default initial condition expression. Default_Initial_Condition
may be specified on a private_type_declaration,
or a formal_derived_type_definition.
for Default_Initial_Condition: A
condition that must hold true after the default initialization of an
Glossary entry: A
property that holds for every default-initialized object of a given type.
Name Resolution Rules
The expected type for a default initial condition
expression is any boolean type.
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 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
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. 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.]
Proof: This follows
from the general dynamic semantics rules given above, but we mention
it explicitly so that there can be no doubt that it is intended.
Implementations may extend the syntax or semantics
of the Default_Initial_Condition aspect in an implementation-defined
Any extensions of the Default_Initial_Condition
Reason: This is
intended to allow preexisting usages from SPARK 2014 to remain acceptable
in conforming implementations, as well as to provide future flexibility.
Note the word “extend” in this permission; we expect that
any aspect usage that conforms with the (other) rules of this clause
will be accepted by any Ada implementation, regardless of any implementation-defined
For an example of the use of this aspect, see the
Vector container definition in A.18.2.
Extensions to Ada 2012
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe