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
