7.3.2 Type Invariants
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.
Aspect Description for Type_Invariant:
A condition that must hold true for all objects of a type.
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,
or a full_type_declaration
for an interface type.
Type_Invariant'Class determines a class-wide type invariant for
a tagged type.
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.
Aspect Description for Type_Invariant'Class:
A condition that must hold true for all objects in a class of types.
Name Resolution Rules
{
AI05-0146-1}
The expected type for an invariant expression is any boolean type.
{
AI05-0146-1}
{
AI12-0150-1}
{
AI12-0159-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
for the Type_Invariant
aspect of a associated with type
T, the type of
this the
current instance is
T. Within an invariant
expression for the Type_Invariant aspect
and T'Class 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.].
Proof: The first sentence is given formally
in
13.1.1.
Reason: {
AI12-0159-1}
The rules for Type_Invariant'Class ensure that
the invariant expression is well-defined for any type descended from
T.
Legality Rules
{
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.
Proof: The first sentence is given formally
in
13.1.1.
{
AI12-0042-1}
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
{
AI05-0250-1}
[If the Type_Invariant aspect is specified for a type
T, then
the invariant expression applies to
T.]
{
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.]
Proof: "Applies" is formally
defined in
13.1.1.
Dynamic Semantics
{
AI12-0133-1}
After successful
default 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;
Reason: {
AI12-0133-1}
The check applies everywhere, even in the package
body, because default initialization has to work the same for clients
as it does within the package. As such, checks within the package are
either harmless or will uncover a bug that could also happen to a client.
However, if the partial view of the type has unknown discriminants, no
client of the package can declare a default-initialized object. Therefore,
no invariant check is needed, as all default initialized objects are
necessarily inside the package.
{
AI12-0049-1}
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;
After successful conversion to type T, the
check is performed on the result of the conversion;
{
AI05-0146-1}
{
AI05-0269-1}
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.
Ramification: For a single view conversion
that converts between distantly related types, this rule could be triggered
for multiple types and thus multiple invariant checks may be needed.
Implementation Note: {
AI05-0299-1}
For calls to inherited subprograms (including dispatching calls), the
implied view conversions mean that a wrapper is probably needed. (See
the Note at the bottom of this subclause for more on the model of checks
for inherited subprograms.)
For view conversions involving class-wide types,
the exact checks needed may not be known at compile-time. One way to
deal with this is to have an implicit dispatching operation that is given
the object to check and the tag of the target of the conversion, and
which first checks if the passed tag is not for itself, and if not, checks
the its invariant on the object and then calls the operation of its parent
type. If the tag is for itself, the operation is complete.
{
AI12-0146-1}
After a successful call on the Read or Input
stream-oriented stream
attribute of the type
T, the check is performed on the object
initialized by the
stream attribute;
{
AI05-0146-1}
{
AI05-0269-1}
An invariant is checked upon successful return from a call on any subprogram
or entry that:
{
AI05-0146-1}
{
AI05-0269-1}
{
AI12-0042-1}
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
This paragraph
was deleted.{
AI12-0042-1}
is visible outside the immediate scope of type
T or overrides an operation that is visible outside the immediate
scope of T, and
{
AI05-0289-1}
{
AI12-0042-1}
{
AI12-0044-1}
and either: 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.
{
AI12-0044-1}
has one or more out or in out parameters
with a part of type T, or
{
AI12-0044-1}
{
AI12-0149-1}
has an access-to-object parameter or result whose
designated type has a part of type T, or
Discussion: We
don't check in parameters for functions to avoid infinite recursion
for calls to public functions appearing in invariant expressions. Such
function calls are unavoidable for class-wide invariants and likely for
other invariants. This is the simplest rule that avoids trouble, and
functions are much more likely to be queries that don't modify their
parameters than other callable entities.
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
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.
{
AI12-0042-1}
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.
Reason: Class-wide
objects are treated as though they exist outside the scope of every type,
and may be passed across package "boundaries" freely without
further invariant checks.
{
AI05-0290-1}
{
AI12-0080-1}
{
AI12-0159-1}
If performing checks is required by the
Type_Invariant Invariant
or
Type_Invariant'Class 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.
Ramification: If a class-wide invariant
expression is enabled for a type, it remains enabled when inherited by
descendants of that type, even if the policy in effect is Ignore for
the inheriting type.
{
AI05-0146-1}
{
AI05-0250-1}
{
AI05-0289-1}
{
AI05-0290-1}
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.
{
AI12-0150-1}
{
AI12-0159-1}
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.
{
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.
Ramification: {
AI12-0149-1}
Invariant checks on subprogram return are not performed on objects that
are accessible only through access values
that
are subcomponents of some other object. 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
. The designer of the package
has to declare a visible type with an access-to-T subcomponent
and use it as a parameter or result to subprograms in the package, or
pass the client an access-to-subprogram value representing a private
operation of the package. In the absence of such things, all values that
the client can see will be checked for a private type or extension without help for the designer of the package containing T.
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.
13 {
AI05-0250-1}
{
AI05-0269-1}
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.
Proof: This follows from the definition
of a call on an inherited subprogram as view conversions of the parameters
of the type and a call to the original subprogram (see
3.4),
along with the normal invariant checking rules. In particular, the call
to the original subprogram takes care of any checks needed on type
T,
and the checks required on view conversions take care of any checks needed
on type
NT, specifically on
in out and
out parameters.
We require this in order that the semantics of an explicitly defined
wrapper that does nothing but call the original subprogram is the same
as that of an inherited subprogram.
Extensions to Ada 2005
Inconsistencies With Ada 2012
{
AI12-0042-1}
Corrigendum: Clarified
the definition of when invariant checks occur for inherited subprograms.
This might cause checks to be added or removed in some cases. These are
all rare cases involving class-wide type invariants and either record
extensions or multiple levels of derivation. Additionally, implementations
probably make the checks as the intent seems clear, even though the formal
language did not include them. So we do not expect this to be a problem
in practice.
{
AI12-0042-1}
Corrigendum: Added invariant checks for
conversions to class-wide types. This might cause an invariant check
to fail in some cases where they would not be made in the original definition
of Ada 2012. Such cases represent a hole where a value that fails an
invariant could "leak out" of a package, and as such will detect
far more bugs than it causes.
{
AI12-0044-1}
Corrigendum: Removed the invariant check
for in parameters of functions, so that typical invariants don't
cause infinite recursion. This is strictly inconsistent, as the Ada 2012
definition has this check; therefore, programs could depend on Assertion_Error
being raised upon the return from some call on a public function. However,
as the intent of assertion checking is to uncover bugs, a program that
depends on a bug occurring seems very unlikely.
{
AI12-0049-1}
{
AI12-0149-1}
Corrigendum: Added an invariant check for
deferred constants and for access values returned from functions, so
they cannot be used to “leak” values that violate the invariant
from a package. This is strictly inconsistent, as the Ada 2012 definition
is missing these checks; therefore, programs could depend on using values
that violate an invariant outside of the package of definition. These
will not raise Assertion_Error in Ada 2012 as defined in the Ada 2012
Standard, but ought to do so (as noted by this change). As these are
a violation of the intent of invariants, we think that this change will
mainly reveal bugs rather than cause them.
{
AI12-0150-1}
{
AI12-0159-1}
Corrigendum: Eliminated unintentional redispatching
from class-wide type invariants. This means that a different body might
be evaluated for a type invariant check where the value has a different
tag than that of the type. The change means that the behavior of Type_Invariant
and Type_Invariant'Class will be the same for a particular subprogram,
and that the known behavior of the operations can be assumed. We expect
that this change will primarily fix bugs, as it will make class-wide
type invariants work more like expected. In the case where redispatching
is desired, an explicit conversion to a class-wide type can be used.
Incompatibilities With Ada 2012
{
AI12-0042-1}
Corrigendum: A private
operation that is inherited in the visible part of a package to which
a class-wide invariant applies now requires overriding. This is a very
unlikely situation, and will prevent problems with invariant checks being
added to routines that assume that they don't need them.
Extensions to Ada 2012
{
AI12-0041-1}
Corrigendum: Class-wide
type invariants can now be specified on interfaces as well as private
types.
Wording Changes from Ada 2012
{
AI12-0133-1}
Corrigendum: Clarified that all objects
that are initialized by default should have an invariant check, and added
an exception for types with unknown discriminants, as in that case the
client cannot declare a default-initialized object. This exception to
the check is formally inconsistent, but since it is only removing an
assertion failure that occurs where no assertion should be checked anyway
(meaning it's more likely to fix a bug than cause one), and programs
depending on assertion failure should be very rare outside of test cases,
we don't document this as inconsistent.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe