7.3.2 Type Invariants
For a private type,
private extension, or interface, the following language-defined assertion
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,
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.
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 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.
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.
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
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 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:
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).
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).
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.
Dynamic Semantics
If one or more invariant
expressions apply to a nonabstract type
T, then an invariant check
is performed at the following places, on the specified object(s):
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;
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;
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.
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.
a result with a nominal type that has
a part of type T;
an out or in out parameter
whose nominal type has a part of type T;
an access-to-object parameter or result
whose designated nominal type has a part of type T; or
for a procedure or entry, an in
parameter whose nominal type has a part of type T.
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.
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.
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.
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.
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.
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.
NOTE 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.
Examples
Example of a work scheduler where only urgent
work can be scheduled for weekends:
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;
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe
