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.
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}
[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.
Proof: The first sentence is given formally
in
13.1.1.
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.
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
{
AI05-0146-1}
{
AI05-0247-1}
{
AI05-0290-1}
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;
{
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.
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;
{
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}
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
{
AI05-0289-1}
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.
{
AI05-0290-1}
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.
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.
{
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: 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.
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
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe