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 (see 13.1.1):

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 operations.

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 manner.