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,
a private_extension_declaration,
a formal_private_type_definition,
or a formal_derived_type_definition.
[The Default_Initial_Condition
aspect is not inherited, but its effects are additive, as defined below.]
Aspect Description
for Default_Initial_Condition: A
condition that will hold true after the default initialization of an
object.
Term entry: default
initial condition — property that holds for every default-initialized
object of a given type
Name Resolution Rules
{
AI12-0265-1}
The expected type for a default initial condition
expression is any boolean type.{
AI12-0397-1}
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
operations.Reason: This is
analogous to the rule for Post'Class (see 6.1.1)
and ensures that the expression is well-defined for any descendant of
type T.
Ramification: The
operations of NT are also nonabstract, so the rule against a call of
an abstract subprogram does not trigger for a default initial condition
for an abstract type. Note that, presuming T is tagged, it is possible
to call class-wide operations of the type T given an object of type NT.
Similarly it is possible to explicitly convert an object of type NT to
a subtype of T, and pass it to a nonprimitive operation expecting a parameter
of type T. [Note that one cannot directly convert to (the first subtype
of) T since it represents the current instance of the type within the
aspect expression, but one can convert to a subtype of T (including a
subtype that matches the first subtype).]
Legality Rules
{
AI12-0265-1}
The Default_Initial_Condition aspect shall not
be specified for a type whose partial view has unknown discriminants[,
whether explicitly declared or inherited].Static Semantics
{
AI12-0265-1}
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.Dynamic Semantics
{
AI12-0265-1}
{
AI12-0397-1}
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).Proof: {
AI12-0397-1}
If T is an abstract type, then there will never
be an initialization of an object of the type.
{
AI12-0265-1}
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.{
AI12-0265-1}
{
AI12-0397-1}
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.Ramification: {
AI12-0397-1}
Just as is true for a formal derived type (see
12.5.1), for a tagged type T, the controlling
tag of a call on a primitive of NT will cause the body of the corresponding
primitive of T to be executed. For an untagged type T, invoking a primitive
of NT will cause the body of the operation of the type where the aspect
originated to be executed, with conversions performed as for an inherited
subprogram.
{
AI12-0272-1}
[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.
Implementation Permissions
{
AI12-0332-1}
Implementations may extend the syntax or semantics
of the Default_Initial_Condition aspect in an implementation-defined
manner.Implementation defined:
Any extensions of the Default_Initial_Condition
aspect.
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 subclause
will be accepted by any Ada implementation, regardless of any implementation-defined
extensions.
NOTE {
AI12-0312-1}
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
