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 will 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,
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.
[The Type_Invariant'Class aspect is not inherited, but its effects are
additive, as defined below.]
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 will hold true for all objects in a class of types.
Term entry: invariant —
assertion that is expected to be True for all objects of a given private
type when viewed from outside the defining package
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}
{
AI12-0199-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 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) nonabstract
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}
{
AI12-0382-1}
If a type extension occurs immediately within the visible part of a package
specification, 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}
{
AI12-0199-1}
If the Type_Invariant'Class aspect is specified for a tagged type
T,
then a
corresponding expression also applies to each nonabstract
descendant
T1 of
T [(including
T itself if it is
nonabstract)]. The corresponding expression is constructed from the associated
expression as follows:
{
AI12-0199-1}
References to nondiscriminant components of
T (or to
T
itself) are replaced with references to the corresponding components
of
T1 (or to
T1 as a whole).
Ramification: {
AI12-0199-1}
The only nondiscriminant components visible at the point of such an aspect
specification are necessarily inherited from some nonprivate ancestor.
{
AI12-0199-1}
References to discriminants of
T are replaced with references
to the corresponding discriminant of
T1, or to the specified value
for the discriminant, if the discriminant is specified by the
derived_type_definition
for some type that is an ancestor of
T1 and a descendant of
T
(see
3.7).
This paragraph
was deleted.
Discussion: The associated expression
from which the corresponding expression is constructed is the one that
applies to the descendant type; "applies" is formally defined
in
13.1.1.
{
AI12-0075-1}
{
AI12-0191-1}
For a nonabstract type
T, a callable entity is said to be a
boundary
entity for
T if it is declared within
the immediate scope of
T (or by an instance of a generic unit,
and the generic is declared within the immediate scope of type
T),
or is the Read or Input stream-oriented attribute of type
T, and
either:
T is a private type or a private extension
and the callable entity 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 callable
entity 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.
Reason: {
AI12-0191-1}
A boundary entity for type
T is one that might require an invariant
check for
T. It includes subprograms that don't (visibly) involve
T; since we don't want to break privacy, we can't statically know if
some private type has some part of
T. We'll reduce the set when
we describe the actual checks.
Dynamic Semantics
{
AI12-0133-1}
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;
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}
{
AI12-0191-1}
After successful explicit initialization of the completion of a deferred
constant whose nominal type has 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}
{
AI12-0075-1}
{
AI12-0191-1}
{
AI12-0193-1}
Upon successful return from a call on any callable entity which is a
boundary entity for
T, an invariant check is performed on each
object which is subject to an invariant check for
T. In the case
of a call to a protected operation, the check is performed before the
end of the protected action. In the case of a call to a task entry, the
check is performed before the end of the rendezvous. The following objects
of a callable entity are subject to an invariant check for
T:
Paragraph
16 was merged above.
{
AI12-0075-1}
{
AI12-0191-1}
an access-to-object parameter or result whose designated nominal type
has a part of type
T; or
Ramification: {
AI12-0167-1}
{
AI12-0191-1}
This is a Dynamic Semantics rule, so we ignore privacy when determining
if a check is needed. We do, however, use the nominal type of objects
to determine if a part of type
T is present; therefore, parts
that aren't known at compile-time (after ignoring privacy) are never
subject to an invariant check. This is preferable, as we don't want overhead
associated with the possibility that there
might exist an extension
of a tagged type that has a part of type
T. (See the "leaks"
note below for avoidance advice.)
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.
{
AI05-0146-1}
{
AI05-0269-1}
{
AI12-0075-1}
{
AI12-0338-1}
If the nominal type of a formal parameter (or the designated nominal
type of an access-to-object parameter or result) is incomplete at the
point of the declaration of the callable entity, and if the completion
of that incomplete type does not occur in the same declaration list as
the incomplete declaration, then for purposes of the preceding rules
the nominal type is considered to have no parts of type
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.
{
AI12-0167-1}
Despite this model, if an object of type
T that is a component
of a class-wide object is modified within the scope of the full view
of type
T, then there is no invariant check for
T at that
point.
{
AI05-0290-1}
{
AI12-0080-1}
{
AI12-0159-1}
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.
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}
{
AI12-0167-1}
{
AI12-0210-1}
Type invariant checks are intended to prevent invariant-violating values
from inadvertently "leaking out"; that is, code which cannot
see the completion of the private type should not be able to reference
invariant-violating values of the type (assuming the type invariant condition
itself is well behaved - for example, no uses of global variables during
evaluation of the invariant expression). This goal is not completely
achieved; such leaking is possible but, importantly, it requires assistance
(deliberate or not) of some form from the package that declares the invariant-bearing
private type (or a child unit thereof); a client of a well-crafted package
cannot use these holes to obtain an invariant-violating value without
help.
{
AI12-0210-1}
The list of known techniques whereby this kind of leak can occur (ignoring
things like erroneous execution and the various forms of unchecked type
conversion) consists of:
A boundary entity might assign an invariant-violating
value to a global variable that is visible to client code.
{
AI12-0149-1}
Invariant checks on subprogram return are not performed on objects that
are accessible only through access-valued components of other objects.
This can only cause a leak if there is a type with access-valued components
that is used as a parameter or result type of a boundary entity. For
a type
T that has a type invariant, avoiding the declaration of
types with access-valued components designating objects with parts of
T in the package that contains
T is sufficient to prevent
this leak.
A client could call through an access-to-subprogram
value and reach a subprogram body that has visibility on the full declaration
of a type; no invariant checks will be performed if the designated subprogram
is not itself a boundary subprogram. This leak can only happen if an
access-to-subprogram value of a subprogram that is not visible to clients
is passed out to clients.
{
AI12-0167-1}
{
AI12-0191-1}
Invariant checks are only performed for parts of the nominal type for
tagged parameters and function results. This means that components of
extensions are not checked (these would be very expensive to check as
any tagged type
might have such an extension in the future, even
though that would be very unlikely). For this leak to occur for a type
T that has a type invariant, the body of a boundary entity of
T needs to have visibility on a type extension that has components
of
T or access-to-
T and also has an ancestor type (or class)
as a parameter or result of the subprogram.
{
AI12-0338-1}
Invariant checks are not performed for parts of incomplete types when
the completion is not available. For this leak to occur for a type
T
that has a type invariant and is declared in a package
P, one
has to use a
limited with on a package that has
P in its
semantic closure, and then use a type from that package as a parameter
or result of a boundary subprogram for
T (or as the designated
type of a parameter or result of such a subprogram).
{
AI12-0210-1}
Consider a package
P which declares an invariant-bearing private
type
T and a generic package
P.G1, which in turn declares
another generic package
P.G1.G2. Outside of package
P,
there are declarations of an instantiation
I1 of
P.G1 and
an instantiation
I2 of
I1.G2.
I2 can declare visible
subprograms whose bodies see the full view of
T and yet these
subprograms are not boundary subprograms (because the generic
I1.G2
is not declared within the immediate scope of
T -
G1.G2
is, but that's irrelevant). So a call to one of these subprograms from
outside of
P could yield an invariant-violating value. So long
as a nested generic of a nested generic unit of
P is not declared,
no such leaks are possible.
{
AI12-0210-1}
All of these leaks require cooperation of some form (as detailed above)
from within the immediate scope of the invariant-bearing type.
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.
NOTE {
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.
Examples
package Work_Orders is
-- See 3.5.1 for type declarations of Level, Day, and Weekday
type Work_Order is private with
Type_Invariant => Day_Scheduled (Work_Order) in Weekday
or else Priority (Work_Order) = Urgent;
function Schedule_Work (Urgency : in Level;
To_Occur : in Day) return Work_Order
with Pre => Urgency = Urgent or else To_Occur in Weekday;
function Day_Scheduled (Order : in Work_Order) return Day;
function Priority (Order : in Work_Order) return Level;
procedure Change_Priority (Order : in out Work_Order;
New_Priority : in Level;
Changed : out Boolean)
with Post => Changed = (Day_Scheduled(Order) in Weekday
or else Priority(Order) = Urgent);
private
type Work_Order is record
Scheduled : Day;
Urgency : Level;
end record;
end Work_Orders;
package body Work_Orders is
function Schedule_Work (Urgency : in Level;
To_Occur : in Day) return Work_Order is
(Scheduled => To_Occur, Urgency => Urgency);
function Day_Scheduled (Order : in Work_Order) return Day is
(Order.Scheduled);
function Priority (Order : in Work_Order) return Level is
(Order.Urgency);
procedure Change_Priority (Order : in out Work_Order;
New_Priority : in Level;
Changed : out Boolean) is
begin
-- Ensure type invariant is not violated
if Order.Urgency = Urgent or else (Order.Scheduled in Weekday) then
Changed := True;
Order.Urgency := New_Priority;
else
Changed := False;
end if;
end Change_Priority;
end Work_Orders;
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 Reference Manual,
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.
{
AI12-0199-1}
Correction: Class-wide type invariants are no longer checked for
abstract types. Thus, a program that previously raised Assertion_Error
because of a call to a concrete subprogram of an abstract type will no
longer do so. However, programs that depend on assertion failure are
likely to be very rare, some explicit conversion to the abstract type
is needed to get static binding, and additionally many such checks would
call abstract functions (likely causing some compiler failure). As such,
this incompatibility most likely will never be seen in practice.
Incompatibilities With Ada 2012
{
AI12-0042-1}
{
AI12-0382-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 have them. Note: The original wording was missing the
restriction to the visible part of the package, this was added later
for Ada 2022.
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.
{
AI12-0075-1}
{
AI12-0191-1}
Defined the term “boundary entity” to separate the static
rules from the dynamic rules, and allow rules in other subclauses to
reference these rules. No semantic change is intended.
{
AI12-0191-1}
Clarified that invariant checks only apply to parts of the nominal type
of objects.
{
AI12-0193-1}
Correction: Clarified when type invariant checks happen for protected
actions and entry calls.
{
AI12-0338-1}
Correction: Clarified that type invariant checks do not occur
for parts of incomplete types unless the completion is available.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe
