7.3.2 Type Invariants
For a private type
or private extension, the following language-defined aspects may be specified
with an
aspect_specification
(see
13.1.1):
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.
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
or a
private_extension_declaration.
Name Resolution Rules
The expected type for an invariant expression is
any boolean type.
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 associated with type T,
the type of the current instance is T for the Type_Invariant aspect
and T'Class for the Type_Invariant'Class aspect.
Legality Rules
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.
Static Semantics
If the Type_Invariant aspect is specified for a type
T, then the invariant expression applies to T.
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
If one or more invariant
expressions apply to a type
T, then an invariant check is performed
at the following places, on the specified object(s):
After successful default initialization of an object
of type T, the check is performed on the new object;
After successful conversion to type T, the
check is performed on the result of the conversion;
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:
after assigning to the view conversion;
and
after successful return from a call
that passes the view conversion as an in out or out parameter.
After a successful call on the Read or Input stream
attribute of the type T, the check is performed on the object
initialized by the stream attribute;
An invariant is checked
upon successful return from a call on any subprogram or entry that:
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), and
is visible outside the immediate scope
of type T or overrides an operation that is visible outside the
immediate scope of T, and
has a result with a part of type T,
or one or more parameters with a part of type T, or an access
to variable parameter whose designated type has a part of type T.
The check is performed on each such part
of type T.
If performing checks is required by the Invariant
or Invariant'Class assertion policies (see
11.4.2)
in effect at the point of corresponding aspect specification applicable
to a given type, then the respective invariant expression is considered
enabled.
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.
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.
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.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe