7.3.2 Type Invariants
1/3
2/3
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.
2.a/3
Aspect Description
for Type_Invariant: A
condition that must hold true for all objects of a type.
3/3
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.
3.a/3
Reason: {
AI05-0254-1}
A class-wide type invariant cannot be hidden in
the private part, as the creator of an extension needs to know about
it in order to conform to it in any new or overriding operations. On
the other hand, a specific type invariant is not inherited, so that no
operation outside of the original package needs to conform to it; thus
there is no need for it to be visible.
3.b/3
Aspect Description
for Type_Invariant'Class: A
condition that must hold true for all objects in a class of types.
Name Resolution Rules
4/3
{
AI05-0146-1}
The expected type for an invariant expression is
any boolean type.5/3
{
AI05-0146-1}
[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.5.a/3
Proof: The first
sentence is given formally in 13.3.1.
Legality Rules
6/3
{
AI05-0146-1}
[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.a/3
Proof: The first
sentence is given formally in 13.3.1.
Static Semantics
7/3
{
AI05-0250-1}
[If the Type_Invariant aspect is specified for
a type T, then the invariant expression applies to T.]8/3
{
AI05-0146-1}
[If the Type_Invariant'Class aspect is specified
for a tagged type T, then the invariant expression applies to
all descendants of T.]8.a/3
Proof: "Applies"
is formally defined in 13.3.1.
Dynamic Semantics
9/3
{
AI05-0146-1}
{
AI05-0247-1}
If one or more invariant expressions apply to a
type T, and the assertion policy (see 11.4.2)
at the point of the partial view declaration for T is Check, then
an invariant check is performed at the following places, on the specified
object(s):10/3
After successful default
initialization of an object of type T, the check is performed
on the new object;
11/3
After successful conversion
to type T, the check is performed on the result of the conversion;
12/3
After assigning to a view
conversion, outside the immediate scope of T, that converts from
T or one or more record extensions (and no private extensions)
of T to an ancestor of type T, a check is performed on
the part of the object that is of type T; similarly, for passing
a view conversion as an out or in out parameter outside
the immediate scope of T, this check is performed upon successful
return;
13/3
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;
14/3
Upon
successful return from a call on any subprogram or entry that:
15/3
is explicitly 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
16/3
is visible outside
the immediate scope of type T or overrides an operation that is
visible outside the immediate scope of T, and
17/3
has a result with
a part of type T, or one or more in out or out parameters
with a part of type T, or an access to variable parameter whose
designated type has a part of type T.
18/3
the check is performed
on each such part of type T.
19/3
{
AI05-0146-1}
{
AI05-0250-1}
The invariant check consists of the evaluation
of each 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 checks associated with by-copy
in out or out parameters are performed in an arbitrary
order.20/3
{
AI05-0146-1}
{
AI05-0247-1}
{
AI05-0250-1}
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.21/3
{
AI05-0146-1}
{
AI05-0247-1}
[If the assertion policy in effect at the point
of a subprogram or entry declaration is Ignore, then no invariant check
is performed on a call on that subprogram or entry.]21.a/3
Ramification: Invariant
checks on subprogram return are not performed on objects that are accessible
only through access values. It is also possible to call through an access-to-subprogram
value and reach a subprogram body that has visibility on the full declaration
of a type, from outside the immediate scope of the type. No invariant
checks will be performed if the designated subprogram is not itself externally
visible. These cases represent "holes" in the protection provided
by invariant checks; but note that these holes cannot be caused by clients
of the type T with the invariant without help for the designer
of the package containing T.
21.b/3
Implementation Note:
The implementation might want to produce a warning if a private extension
has an ancestor type that is a visible extension, and an invariant expression
depends on the value of one of the components from a visible extension
part.
22/3
13 {
AI05-0250-1}
A call of a primitive subprogram of type NT
that is inherited from type T needs to satisfy the specific invariants
of both the types NT and T. A call of a primitive subprogram
of type NT that is overridden for type NT needs to satisfy
only the specific invariants of type NT.22.a/3
Proof: This follows
from the definition of inheritance as view conversions of the parameters
of the type, along with the rule require checks on such view conversions.
We require this in order that the semantics of an explicitly defined
wrapper that does nothing but call the original routine is the same as
that of an inherited routine.
Extensions to Ada 2005
22.b/3
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe
