Ada Conformity Assessment Authority      Home Conformity Assessment   Test Suite ARGAda Standard
 
Annotated Ada Reference Manual (Ada 202x Draft 11)Legal Information
Contents   Index   References   Search   Previous   Next 

7.3.2 Type Invariants

1/4
{AI05-0146-1} {AI12-0041-1} For a private type, or private extension, or interface, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
2/3
{AI05-0146-1} {AI05-0250-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.
2.a/3
Aspect Description for Type_Invariant: A condition that must hold true for all objects of a type.
3/4
{AI05-0146-1} {AI12-0041-1} {AI12-0150-1} 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, 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.
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/4
{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) 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.].
5.a/3
Proof: The first sentence is given formally in 13.1.1
5.b/4
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

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.1.1
6.1/4
 {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

7/3
{AI05-0250-1} [If the Type_Invariant aspect is specified for a type T, then the invariant expression applies to T.]
8/5
{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: the invariant expression applies to all descendants of T.
8.1/5
{AI12-0199-1} References to non-discriminant components of T (or to T itself) are replaced with references to the corresponding components of T1 (or to T1 as a whole).
8.a.1/5
Ramification: {AI12-0199-1} The only nondiscriminant components visible at the point of such an aspect specification are necessarily inherited from some nonprivate ancestor. 
8.2/5
{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). 
8.a/5
This paragraph was deleted.Proof: "Applies" is formally defined in 13.1.1. 
8.b/5
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. 

Dynamic Semantics

9/4
{AI05-0146-1} {AI05-0247-1} {AI05-0290-1} {AI12-0150-1} 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):
10/4
{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;
10.a/4
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. 
10.1/4
{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;
11/3
After successful conversion to type T, the check is performed on the result of the conversion;
12/3
{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:
13/3
after assigning to the view conversion; and
14/3
after successful return from a call that passes the view conversion as an in out or out parameter.
14.a/3
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.
14.b/3
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.)
14.c/3
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. 
15/4
{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;
16/3
{AI05-0146-1} {AI05-0269-1} An invariant is checked upon successful return from a call on any subprogram or entry that: 
17/4
{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
18/4
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
19/4
{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.
19.1/4
{AI12-0044-1} has a result with a part of type T, or
19.2/4
{AI12-0044-1} has one or more out or in out parameters with a part of type T, or
19.3/4
{AI12-0044-1} {AI12-0149-1} has an access-to-object parameter or result whose designated type has a part of type T, or
19.4/4
{AI12-0042-1} {AI12-0044-1} is a procedure or entry that has an in parameter with a part of type T,
19.a/4
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. 
19.5/4
{AI12-0042-1} and either:
19.6/4
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
19.7/4
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.
20/5
{AI05-0146-1} {AI05-0269-1} {AI12-0193-1} The check is performed on each such part of type 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.
20.a.1/5
To be honest: {AI12-0167-1} In all of the above, for a class-wide object, we are only referring to the parts of the specific root type of the class. We don't want the overhead of checking every class-wide object in case some future extension component might have type T (contrast this to finalization, where we do intend that overhead). 
20.1/4
{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.
20.a/4
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.
20.b/5
{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. 
21/4
{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.
21.a/3
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. 
22/3
{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.
22.1/4
  {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.
23/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.
23.a/5
Ramification: {AI12-0149-1} {AI12-0167-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. Similar holes exist for class-wide objects as discussed above.
23.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.
NOTES
24/3
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.
24.a/3
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

24.b/3
{AI05-0146-1} {AI05-0247-1} {AI05-0250-1} {AI05-0289-1} Type_Invariant aspects are new. 

Inconsistencies With Ada 2012

24.c/4
{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.
24.d/4
{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.
24.e/4
{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.
24.f/4
{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.
24.g/4
{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.
24.h/5
{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

24.i/4
{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 have them. 

Extensions to Ada 2012

24.j/4
{AI12-0041-1} Corrigendum: Class-wide type invariants can now be specified on interfaces as well as private types. 

Wording Changes from Ada 2012

24.k/4
{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.
24.l/5
{AI12-0193-1} Correction: Clarified when type invariant checks happen for protected actions and entry calls. 

Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe