Ada Conformity Assessment Authority      Home Conformity Assessment   Test Suite ARGAda Standard
Annotated Ada Reference Manual (Ada 202x Draft 25)Legal Information
Contents   Index   References   Search   Previous   Next 

7.3.3 Default Initial Conditions

{AI12-0265-1} {AI12-0272-1} For a private type or private extension (including a generic formal type), the following language-defined aspect may be specified with an aspect_specification (see 13.1.1):
{AI12-0265-1} Default_Initial_Condition

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.
Aspect Description for Default_Initial_Condition: A condition that must hold true after the default initialization of an object.
Glossary entry: A 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.

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} 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 (see 7.6).
{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} 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.
{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 clause will be accepted by any Ada implementation, regardless of any implementation-defined extensions. 
14  {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

{AI12-0265-1} {AI12-0272-1} Aspect Default_Initial_Condition is new. 

Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe