Ada Reference ManualLegal Information
Contents   Index   References   Search   Previous   Next 

7.3.2 Type Invariants

1/4
For a private type, private extension, or interface, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
2/3
Type_Invariant

This aspect shall be specified by an expression, called an invariant expression. Type_Invariant may be specified on a private_type_declaration, on a private_extension_declaration, or on a full_type_declaration that declares the completion of a private type or private extension.
3/4
Type_Invariant'Class

This aspect shall be specified by an expression, called an invariant expression. Type_Invariant'Class may be specified on a private_type_declaration, a private_extension_declaration, or a full_type_declaration for an interface type. Type_Invariant'Class determines a class-wide type invariant for a tagged type.

Name Resolution Rules

4/3
The expected type for an invariant expression is any boolean type.
5/4
Within an invariant expression, the identifier of the first subtype of the associated type denotes the current instance of the type. Within an invariant expression for the Type_Invariant aspect of a type T, the type of this current instance is T. Within an invariant expression for the Type_Invariant'Class aspect of a type T, the type of this current instance is interpreted as though it had a (notional) type NT that is a visible formal derived type whose ancestor type is T. The effect of this interpretation is that the only operations that can be applied to this current instance are those defined for such a formal derived type.

Legality Rules

6/3
The Type_Invariant'Class aspect shall not be specified for an untagged type. The Type_Invariant aspect shall not be specified for an abstract type.
6.1/4
 If a type extension occurs at a point where a private operation of some ancestor is visible and inherited, and a Type_Invariant'Class expression applies to that ancestor, then the inherited operation shall be abstract or shall be overridden. 

Static Semantics

7/3
If the Type_Invariant aspect is specified for a type T, then the invariant expression applies to T.
8/3
If the Type_Invariant'Class aspect is specified for a tagged type T, then the invariant expression applies to all descendants of T.

Dynamic Semantics

9/4
If one or more invariant expressions apply to a nonabstract type T, then an invariant check is performed at the following places, on the specified object(s):
10/4
After successful initialization of an object of type T by default (see 3.3.1), the check is performed on the new object unless the partial view of T has unknown discriminants;
10.1/4
After successful explicit initialization of the completion of a deferred constant with a part of type T, if the completion is inside the immediate scope of the full view of T, and the deferred constant is visible outside the immediate scope of T, the check is performed on the part(s) of type T;
11/3
After successful conversion to type T, the check is performed on the result of the conversion;
12/3
For a view conversion, outside the immediate scope of T, that converts from a descendant of T (including T itself) to an ancestor of type T (other than T itself), a check is performed on the part of the object that is of type T:
13/3
after assigning to the view conversion; and
14/3
after successful return from a call that passes the view conversion as an in out or out parameter.
15/4
After a successful call on the Read or Input stream-oriented attribute of the type T, the check is performed on the object initialized by the attribute;
16/3
An invariant is checked upon successful return from a call on any subprogram or entry that: 
17/4
is declared within the immediate scope of type T (or by an instance of a generic unit, and the generic is declared within the immediate scope of type T),
18/4
This paragraph was deleted.
19/4
and either:
19.1/4
has a result with a part of type T, or
19.2/4
has one or more out or in out parameters with a part of type T, or
19.3/4
has an access-to-object parameter or result whose designated type has a part of type T, or
19.4/4
is a procedure or entry that has an in parameter with a part of type T,
19.5/4
and either:
19.6/4
T is a private type or a private extension and the subprogram or entry is visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T, or
19.7/4
T is a record extension, and the subprogram or entry is a primitive operation visible outside the immediate scope of type T or overrides an inherited operation that is visible outside the immediate scope of T
20/3
The check is performed on each such part of type T.
20.1/4
For a view conversion to a class-wide type occurring within the immediate scope of T, from a specific type that is a descendant of T (including T itself), a check is performed on the part of the object that is of type T.
21/4
If performing checks is required by the Type_Invariant or Type_Invariant'Class assertion policies (see 11.4.2) in effect at the point of the corresponding aspect specification applicable to a given type, then the respective invariant expression is considered enabled.
22/3
The invariant check consists of the evaluation of each enabled invariant expression that applies to T, on each of the objects specified above. If any of these evaluate to False, Assertions.Assertion_Error is raised at the point of the object initialization, conversion, or call. If a given call requires more than one evaluation of an invariant expression, either for multiple objects of a single type or for multiple types with invariants, the evaluations are performed in an arbitrary order, and if one of them evaluates to False, it is not specified whether the others are evaluated. Any invariant check is performed prior to copying back any by-copy in out or out parameters. Invariant checks, any postcondition check, and any constraint or predicate checks associated with in out or out parameters are performed in an arbitrary order.
22.1/4
  For an invariant check on a value of type T1 based on a class-wide invariant expression inherited from an ancestor type T, any operations within the invariant expression that were resolved as primitive operations of the (notional) formal derived type NT are bound to the corresponding operations of type T1 in the evaluation of the invariant expression for the check on T1.
23/3
The invariant checks performed on a call are determined by the subprogram or entry actually invoked, whether directly, as part of a dispatching call, or as part of a call through an access-to-subprogram value.
NOTES
24/3
13  For a call of a primitive subprogram of type NT that is inherited from type T, the specified checks of the specific invariants of both the types NT and T are performed. For a call of a primitive subprogram of type NT that is overridden for type NT, the specified checks of the specific invariants of only type NT are performed.

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