Skip to main content

12.5 Formal Types

danger

This Reference Manual output has not been verified, and may contain omissions or errors. Report any problems on the tracking issue

1/2

[A generic formal subtype can be used to pass to a generic unit a subtype whose type is in a certain category of types.]

1.a
reason

We considered having intermediate syntactic categories formal_integer_type_definition, formal_real_type_definition, and formal_fixed_point_definition, to be more uniform with the syntax rules for non-generic-formal types. However, that would make the rules for formal types slightly more complicated, and it would cause confusion, since formal_discrete_type_definition would not fit into the scheme very well.

Syntax

2/3

formal_type_declaration ::=
formal_complete_type_declaration
| formal_incomplete_type_declaration

2.1/5

formal_complete_type_declaration ::=
type defining_identifier[discriminant_part] is formal_type_definition
[or use default_subtype_mark] [aspect_specification];

2.2/5

formal_incomplete_type_declaration ::=
type defining_identifier[discriminant_part] [is tagged]
[or use default_subtype_mark];

3/2

formal_type_definition ::=
formal_private_type_definition
| formal_derived_type_definition
| formal_discrete_type_definition
| formal_signed_integer_type_definition
| formal_modular_type_definition
| formal_floating_point_definition
| formal_ordinary_fixed_point_definition
| formal_decimal_fixed_point_definition
| formal_array_type_definition
| formal_access_type_definition
| formal_interface_type_definition

Legality Rules

4

For a generic formal subtype, the actual shall be a subtype_mark; it denotes the (generic) actual subtype.

4.a
ramification

When we say simply “formal” or “actual” (for a generic formal that denotes a subtype) we're talking about the subtype, not the type, since a name that denotes a formal_type_declaration denotes a subtype, and the corresponding actual also denotes a subtype.

Static Semantics

5

A formal_type_declaration declares a (generic) formal type, and its first subtype, the (generic) formal subtype.

5.a
ramification

A subtype (other than the first subtype) of a generic formal type is not a generic formal subtype.

6/3

The form of a formal_type_definition determines a category (of types) to which the formal type belongs. For a formal_private_type_definition the reserved words tagged and limited indicate the category of types (see 12.5.1). The reserved word tagged also plays this role in the case of a formal_incomplete_type_declaration. For a formal_derived_type_definition the category of types is the derivation class rooted at the ancestor type. For other formal types, the name of the syntactic category indicates the category of types; a formal_discrete_type_definition defines a discrete type, and so on.

6.a
reason

This rule is clearer with the flat syntax rule for formal_type_definition given above. Adding formal_integer_type_definition and others would make this rule harder to state clearly.

6.b/2

We use “category’ rather than “class” above, because the requirement that classes are closed under derivation is not important here. Moreover, there are interesting categories that are not closed under derivation. For instance, limited and interface are categories that do not form classes.

Legality Rules

7/2

The actual type shall be in the category determined for the formal.

7.a/2
ramification

For example, if the category determined for the formal is the category of all discrete types, then the actual has to be discrete.

7.b/2

Note that this rule does not require the actual to belong to every category to which the formal belongs. For example, formal private types are in the category of composite types, but the actual need not be composite. Furthermore, one can imagine an infinite number of categories that are just arbitrary sets of types (even though we don't give them names, since they are uninteresting). We don't want this rule to apply to those categories.

7.c/2

“Limited” is not an “interesting” category, but “nonlimited” is; it is legal to pass a nonlimited type to a limited formal type, but not the other way around. The reserved word limited really represents a category containing both limited and nonlimited types. “Private” is not a category for this purpose; a generic formal private type accepts both private and nonprivate actual types.

7.d/2

It is legal to pass a class-wide subtype as the actual if it is in the right category, so long as the formal has unknown discriminants.

7.1/5

The default_subtype_mark, if any, shall denote a subtype which is allowed as an actual subtype for the formal type.

7.e/5
ramification

This rule is observed at compile time of the generic_declaration, and is consistent with the handling of the default_name of a formal subprogram. This means that a type declared outside of the generic_declaration cannot be used as the default_subtype_mark for a formal type that depends on any other formal type.

Static Semantics

8/5

{8652/0037} [The formal type also belongs to each category that contains the determined category.] The primitive subprograms of the type are as for any type in the determined category. For a formal type other than a formal derived type, these are the predefined operators of the type. For an elementary formal type, the predefined operators are implicitly declared immediately after the declaration of the formal type. For a composite formal type, the predefined operators are implicitly declared either immediately after the declaration of the formal type, or later immediately within the declarative region in which the type is declared according to the rules of 7.3.1. In an instance, the copy of such an implicit declaration declares a view of the predefined operator of the actual type, even if this operator has been overridden for the actual type and even if it is never declared for the actual type, unless the actual type is an untagged record type, in which case it declares a view of the primitive (equality) operator. [The rules specific to formal derived types are given in 12.5.1.]

8.a/2
ramification

All properties of the type are as for any type in the category. Some examples: The primitive operations available are as defined by the language for each category. The form of constraint applicable to a formal type in a subtype_indication depends on the category of the type as for a nonformal type. The formal type is tagged if and only if it is declared as a tagged private type, or as a type derived from a (visibly) tagged type. (Note that the actual type might be tagged even if the formal type is not.)

8.a.1/5

If the primitive equality operator of the (actual) untagged record type is declared abstract, then Program_Error will be raised if the equality operator of the formal type is in fact invoked within an instance of a generic body (see 4.5.2). If the operator is invoked within an instance of the generic spec, the instance is illegal.

8.b/3
reason

The somewhat cryptic phrase “even if it is never declared” is intended to deal with the following oddity:

8.c/3

package Q is type T is limited private; private type T is range 1 .. 10; end Q; 8.d/3 generic type A is array (Positive range <>) of T; package Q.G is A1, A2 : A (1 .. 1); private B : Boolean := A1 = A2; end Q.G; 8.e/3 with Q.G; package R is type C is array (Positive range <>) of Q.T; 8.f/3 package I is new Q.G (C); -- Where is the predefined "=" for C? end R;

8.g/3

An "=" is available for the formal type A in the private part of Q.G. However, no "=" operator is ever declared for type C, because its component type Q.T is limited. Still, in the instance I the name "=" declares a view of the "=" for C which exists-but-is-never-declared.

9

NOTE 1 Generic formal types, like all types, are not named. Instead, a name can denote a generic formal subtype. Within a generic unit, a generic formal type is considered as being distinct from all other (formal or nonformal) types.

9.a
proof

This follows from the fact that each formal_type_declaration declares a type.

10

NOTE 2 A discriminant_part is allowed only for certain kinds of types, and therefore only for certain kinds of generic formal types. See 3.7.

10.a/5
ramification

The term “formal floating point type” refers to a type defined by a formal_floating_point_definition. It does not include a formal derived type whose ancestor is a floating point type. Similar terminology applies to the other kinds of formal_type_definition.

Examples

11

Examples of generic formal types:

12

type Item is private; type Buffer(Length : Natural) is limited private; 13 type Enum is (<>); type Int is range <>; type Angle is delta <>; type Mass is digits <>; 14 type Table is array (Enum) of Item;

15

Example of a generic formal part declaring a formal integer type:

16

generic type Rank is range <>; First : Rank := Rank'First; Second : Rank := First + 1; -- the operator "+" of the type Rank

Wording Changes from Ada 83

16.a

RM83 has separate sections “Generic Formal Xs” and “Matching Rules for Formal Xs” (for various X's) with most of the text redundant between the two. We have combined the two in order to reduce the redundancy. In RM83, there is no “Matching Rules for Formal Types” section; nor is there a “Generic Formal Y Types” section (for Y = Private, Scalar, Array, and Access). This causes, for example, the duplication across all the “Matching Rules for Y Types” sections of the rule that the actual passed to a formal type shall be a subtype; the new organization avoids that problem.

16.b

The matching rules are stated more concisely.

16.c

We no longer consider the multiplying operators that deliver a result of type universal_fixed to be predefined for the various types; there is only one of each in package Standard. Therefore, we need not mention them here as RM83 had to.

Wording Changes from Ada 95

16.d/2

{8652/0037} Corrigendum 1 corrected the wording to properly define the location where operators are defined for formal array types. The wording here was inconsistent with that in 7.3.1, “Private Operations”. For the Amendment, this wording was corrected again, because it didn't reflect the Corrigendum 1 revisions in 7.3.1.

16.e/2

Formal interface types are defined; see 12.5.5, “Formal Interface Types”.

16.f/2

We use “determines a category” rather than class, since not all interesting properties form a class.

Extensions to Ada 2005

16.g/3

An optional aspect_specification can be used in a formal_type_declaration. This is described in 13.1.1.

Wording Changes from Ada 2005

16.h/3

Correction: Updated the wording to acknowledge the possibility of operations that are never declared for an actual type but still can be used inside of a generic unit.

16.i/3

Formal incomplete types are added; these are documented as an extension in the next subclause.

Inconsistencies With Ada 2012

16.j/5
correction

Updated the wording to clarify that predefined record equality never reemerges in a generic instantiation. This model was presumed by 4.5.2, but the wording wasn't right for untagged record types with user-defined equality. Therefore, an implementation that strictly implemented the Ada 2012 wording would call the predefined equality for an actual type that is an untagged record type with a user-defined equality, while Ada 2022 implementations would call the primitive (user-defined) equality. This could change the runtime behavior in rare cases.

Extensions to Ada 2012

16.k/5

Generic formal types now can include an optional default subtype_mark.

12.5.1 Formal Private and Derived Types

1/5

[In its most general form, the category determined for a formal private type is all types, but the category can be restricted to only nonlimited types or to only tagged types. Similarly, the category for a formal incomplete type is all types but the category can be restricted to only tagged types; unlike other formal types, the actual type can be incompletely defined, and not ready to be frozen (see 13.14). The category determined for a formal derived type is the derivation class rooted at the ancestor type.]

1.a/3
proof

The first two rules are given normatively below, and the third rule is given normatively in 12.5; they are repeated here to give a capsule summary of what this subclause is about.

1.b/3
ramification

Since the actual of a formal incomplete type does not need to be able to be frozen, the actual can be an incomplete type or a partial view before its completion.

Syntax

2

formal_private_type_definition ::= [[abstract] tagged] [limited] private

3/5

formal_derived_type_definition ::=
[abstract] [limited | synchronized] new subtype_mark [[and interface_list] with private]

Legality Rules

4

If a generic formal type declaration has a known_discriminant_part, then it shall not include a default_expression for a discriminant.

4.a
ramification

Consequently, a generic formal subtype with a known_discriminant_part is an indefinite subtype, so the declaration of a stand-alone variable has to provide a constraint on such a subtype, either explicitly, or by its initial value.

5/3

The ancestor subtype of a formal derived type is the subtype denoted by the subtype_mark of the formal_derived_type_definition. For a formal derived type declaration, the reserved words with private shall appear if and only if the ancestor type is a tagged type; in this case the formal derived type is a private extension of the ancestor type and the ancestor shall not be a class-wide type. [Similarly, an interface_list or the optional reserved words abstract or synchronized shall appear only if the ancestor type is a tagged type]. The reserved word limited or synchronized shall appear only if the ancestor type [and any progenitor types] are limited types. The reserved word synchronized shall appear (rather than limited) if the ancestor type or any of the progenitor types are synchronized interfaces. The ancestor type shall be a limited interface if the reserved word synchronized appears.

5.a
reason

We use the term “ancestor” here instead of “parent” because the actual can be any descendant of the ancestor, not necessarily a direct descendant.

5.b/3

We require the ancestor type to be limited when limited appears so that we avoid oddities like limited integer types. Normally, limited means “match anything” for a generic formal, but it was felt that allowing limited elementary types to be declared was just too weird. Integer still matches a formal limited private type; it is only a problem when the type is known to be elementary. Note that the progenitors are required to be limited by rules in 3.9.4, thus that part of the rule is redundant.

5.c/2

We require that synchronized appear if the ancestor or any of the progenitors are synchronized, so that property is explicitly given in the program text – it is not automatically inherited from the ancestors. However, it can be given even if neither the ancestor nor the progenitors are synchronized.

5.1/5

The actual type for a formal derived type shall be a descendant of [the ancestor type and] every progenitor of the formal type. The actual type for a formal derived type shall be tagged if and only if the formal derived type is a private extension. If the reserved word synchronized appears in the declaration of the formal derived type, the actual type shall be a synchronized tagged type.

5.d/2
proof

The actual type has to be a descendant of the ancestor type, in order that it be in the correct class. Thus, that part of the rule is redundant.

5.e/3
discussion

For a nonformal private extension, we require the partial view to be synchronized if the full view is synchronized tagged. This does not apply to a formal private extension — it is OK if the formal is not synchronized. Any attempt to extend the formal type will be rechecked in the instance, where the rule disallowing extending a synchronized noninterface type will be enforced. This is consistent with the “no hidden interfaces” rule also applying only to nonformal private extensions, as well as the rule that a limited nonformal private extension implies a limited full type. Formal private extensions are exempted from all these rules to enable the construction of generics that can be used with the widest possible range of types. In particular, an indefinite tagged limited formal private type can match any “concrete” actual tagged type.

5.f/3

A type (including formal types) derived from a limited interface could be nonlimited; we do not want a limited type derived from such an interface to match a nonlimited formal derived type. Otherwise, we could assign limited objects. Thus, we have to explicitly ban this case.

5.g/5

If we allowed actual types whose kind differs from that of the formal derived type, we could allow type conversions that would not be allowed outside of the generic. That would be particularly problematical if the actual is a tagged type with extension components; we could have created an object of the type that is missing those components by converting from the ancestor type to a formal derived type that is not an extension.

6/5

If a formal private or derived subtype is definite, then the actual subtype shall also be definite. If the formal type is nonlimited, the actual type shall be nonlimited.

6.a
ramification

On the other hand, for an indefinite formal subtype, the actual can be either definite or indefinite.

6.b/5
discussion

The rule about nonlimited formals applies to both private and derived formal types.

6.1/3

A formal_incomplete_type_declaration declares a formal incomplete type. The only view of a formal incomplete type is an incomplete view. [Thus, a formal incomplete type is subject to the same usage restrictions as any other incomplete type — see 3.10.1.]

7/5

For a generic formal derived type with no discriminant_part, the actual subtype shall be statically compatible with the ancestor subtype. Furthermore:

8/5
  • If the ancestor subtype is constrained, the actual subtype shall be constrained;
8.a/5
ramification

In other words, any constraint on the ancestor subtype is considered part of the “contract”. Predicates are also considered part of the contract for any subtype, via the static compatibility requirement.

9
  • If the ancestor subtype is an unconstrained access or composite subtype, the actual subtype shall be unconstrained.
9.a
reason

This rule ensures that if a composite constraint is allowed on the formal, one is also allowed on the actual. If the ancestor subtype is an unconstrained scalar subtype, the actual is allowed to be constrained, since a scalar constraint does not cause further constraints to be illegal.

10
  • If the ancestor subtype is an unconstrained discriminated subtype, then the actual shall have the same number of discriminants, and each discriminant of the actual shall correspond to a discriminant of the ancestor, in the sense of 3.7.
10.a
reason

This ensures that if a discriminant constraint is given on the formal subtype, the corresponding constraint in the instance will make sense, without additional runtime checks. This is not necessary for arrays, since the bounds cannot be overridden in a type extension. An unknown_discriminant_part may be used to relax these matching requirements.

10.1/2
  • If the ancestor subtype is an access subtype, the actual subtype shall exclude null if and only if the ancestor subtype excludes null.
10.b/2
reason

We require that the “excludes null” property match, because it would be difficult to write a correct generic for a formal access type without knowing this property. Many typical algorithms and techniques will not work for a subtype that excludes null (setting an unused component to null, default-initialized objects, and so on). We want this sort of requirement to be reflected in the contract of the generic.

11/3

The declaration of a formal derived type shall not have a known_discriminant_part. For a generic formal private or incomplete type with a known_discriminant_part:

12
  • The actual type shall be a type with the same number of discriminants.
  • 13
  • The actual subtype shall be unconstrained.
  • 14
  • The subtype of each discriminant of the actual type shall statically match the subtype of the corresponding discriminant of the formal type.
14.a
reason

We considered defining the first and third rule to be called “subtype conformance” for discriminant_parts. We rejected that idea, because it would require implicit (inherited) discriminant_parts, which seemed like too much mechanism.

15/5

[For a generic formal type with an unknown_discriminant_part, the actual may have discriminants, though that is not required, and may be definite or indefinite.]

15.1/4

When enforcing Legality Rules, for the purposes of determining within a generic body whether a type is unconstrained in any partial view, a discriminated subtype is considered to have a constrained partial view if it is a descendant of an untagged generic formal private or derived type.

Static Semantics

16/2

The category determined for a formal private type is as follows:

17/2

Type Definition Determined Category

limited private the category of all types
private the category of all nonlimited types
tagged limited private the category of all tagged types
tagged private the category of all nonlimited tagged types

18

[The presence of the reserved word abstract determines whether the actual type may be abstract.]

18.1/3

The category determined for a formal incomplete type is the category of all types, unless the formal_type_declaration includes the reserved word tagged; in this case, it is the category of all tagged types.

19

A formal private or derived type is a private or derived type, respectively. A formal derived tagged type is a private extension. [A formal private or derived type is abstract if the reserved word abstract appears in its declaration.]

20/3

For a formal derived type, the characteristics (including components, but excluding discriminants if there is a new discriminant_part), predefined operators, and inherited user-defined primitive subprograms are determined by its ancestor type and its progenitor types (if any), in the same way that those of a derived type are determined by those of its parent type and its progenitor types (see 3.4 and 7.3.1).

21/3

{8652/0038} In an instance, the copy of an implicit declaration of a primitive subprogram of a formal derived type declares a view of the corresponding primitive subprogram of the ancestor or progenitor of the formal derived type, even if this primitive has been overridden for the actual type and even if it is never declared for the actual type. When the ancestor or progenitor of the formal derived type is itself a formal type, the copy of the implicit declaration declares a view of the corresponding copied operation of the ancestor or progenitor. [In the case of a formal private extension, however, the tag of the formal type is that of the actual type, so if the tag in a call is statically determined to be that of the formal type, the body executed will be that corresponding to the actual type.]

21.a/3
ramification

The above rule defining the properties of primitive subprograms in an instance applies even if the subprogram has been overridden or hidden for the actual type. This rule is necessary for untagged types, because their primitive subprograms might have been overridden by operations that are not subtype conformant with the operations defined for the class. For tagged types, the rule still applies, but the primitive subprograms will dispatch to the appropriate implementation based on the type and tag of the operands. Even for tagged types, the formal parameter names and default_expressions are determined by those of the primitive subprograms of the specified ancestor type (or progenitor type, for subprograms inherited from an interface type).

21.b/4

To be honest: The availability of stream attributes is not formally a characteristic of a type, but it is still determined by the ancestor type for a formal derived type in the same way as the characteristics are. Availability is rechecked in the instance specification.

21.1/5

In an instance, the implicitly composed and additive aspects (see 13.1.1) of a formal type are those of the actual; for a nonoverridable aspect, a formal derived type inherits the aspect if the ancestor or any progenitor has the aspect, according to the rules given in 13.1.

22/1

For a prefix S that denotes a formal indefinite subtype, the following attribute is defined:

23/3

S'Definite
S'Definite yields True if the actual subtype corresponding to S is definite; otherwise, it yields False. The value of this attribute is of the predefined type Boolean.
23.a/5
discussion

Whether an actual subtype is definite or indefinite may have a major effect on the algorithm used in a generic. For example, in a generic I/O package, whether to use fixed-length or variable-length records could depend on whether the actual is definite or indefinite. This attribute is essentially a replacement for the Constrained attribute, which is now obsolescent.

Dynamic Semantics

23.1/3

In the case where a formal type has unknown discriminants, and the actual type is a class-wide type T'Class:

23.2/2
  • For the purposes of defining the primitive operations of the formal type, each of the primitive operations of the actual type is considered to be a subprogram (with an intrinsic calling convention — see 6.3.1) whose body consists of a dispatching call upon the corresponding operation of T, with its formal parameters as the actual parameters. If it is a function, the result of the dispatching call is returned.
  • 23.3/2
  • If the corresponding operation of T has no controlling formal parameters, then the controlling tag value is determined by the context of the call, according to the rules for tag-indeterminate calls (see 3.9.2 and 5.2). In the case where the tag would be statically determined to be that of the formal type, the call raises Program_Error. If such a function is renamed, any call on the renaming raises Program_Error.
23.b/2
discussion

As it states in 6.3.1, the convention of an inherited subprogram of a generic formal tagged type with unknown discriminants is intrinsic.

23.c/2

In the case of a corresponding primitive of T with no controlling formal parameters, the context of the call provides the controlling tag value for the dispatch. If no tag is provided by context, Program_Error is raised rather than resorting to a nondispatching call. For example:

23.d/2

generic type NT(<>) is new T with private; -- Assume T has operation "function Empty return T;" package G is procedure Test(X : in out NT); end G; 23.e/2 package body G is procedure Test(X : in out NT) is begin X := Empty; -- Dispatching based on X'Tag takes -- place if actual is class-wide. declare Y : NT := Empty; -- If actual is class-wide, this raises Program_Error -- as there is no tag provided by context. begin X := Y; -- We never get this far. end; end Test; end G; 23.f/2 type T1 is new T with null record; package I is new G(T1'Class);

27

NOTE 1 The actual type can be abstract only if the formal type is abstract (see 3.9.3).

27.a
reason

This is necessary to avoid contract model problems, since one or more of its primitive subprograms are abstract; it is forbidden to create objects of the type, or to declare functions returning the type.

27.b
ramification

On the other hand, it is OK to pass a nonabstract actual to an abstract formal — abstract on the formal indicates that the actual might be abstract.

28/5

NOTE 2 If the formal has a discriminant_part, the actual can be either definite or indefinite. Otherwise, the actual can only be definite.

Incompatibilities With Ada 83

28.a

Ada 83 does not have unknown_discriminant_parts, so it allows indefinite subtypes to be passed to definite formals, and applies a legality rule to the instance body. This is a contract model violation. Ada 95 disallows such cases at the point of the instantiation. The workaround is to add (<>) as the discriminant_part of any formal subtype if it is intended to be used with indefinite actuals. If that's the intent, then there can't be anything in the generic body that would require a definite subtype.

28.b

The check for discriminant subtype matching is changed from a runtime check to a compile-time check.

Extensions to Ada 95

28.c/2

A generic formal derived type can include progenitors (interfaces) as well as a primary ancestor. It also may include limited to indicate that it is a limited type, and synchronized to indicate that it is a synchronized type.

Wording Changes from Ada 95

28.d/2

{8652/0038} Corrigendum: Corrected wording to define the operations that are inherited when the ancestor of a formal type is itself a formal type to avoid anomalies.

28.e/2

Added a semantic description of the meaning of operations of an actual class-wide type, as such a type does not have primitive operations of its own.

28.f/2

Added a matching rule for access subtypes that exclude null.

28.g/2

The wording for the declaration of implicit operations is corrected to be consistent with 7.3.1 as modified by Corrigendum 1.

28.h/2

We change to “determines a category” as that is the new terminology (it avoids confusion, since not all interesting properties form a class).

Incompatibilities With Ada 2005

28.i/3
correction

Added wording to prevent a limited type from being passed to a nonlimited formal derived type. While this was allowed, it would break the contract for the limited type, so hopefully no programs actually depend on that.

Extensions to Ada 2005

28.j/3

Formal incomplete types are a new kind of generic formal; these can be instantiated with incomplete types and unfrozen private types.

Wording Changes from Ada 2005

28.k/3
correction

Updated the wording to acknowledge the possibility of operations that are never declared for an actual type but still can be used inside of a generic unit.

28.l/3
correction

Fixed hole that failed to define what happened for "=" for an untagged private type whose actual is class-wide.

28.m/3
correction

Revised the wording for inheritance of characteristics and operations of formal derived types to be reuse the rules as defined for derived types; this should eliminate holes in the wording which have plagued us since Ada 95 was defined (it has been "corrected" four previous times).

28.n/3
correction

Added missing rule for the ancestors of formal derived types. The added rule would formally be incompatible, but since it would be impossible to instantiate any such generic, this cannot happen outside of test suites and thus is not documented as an incompatibility.

Incompatibilities With Ada 2012

28.o/4

Corrigendum: Added a requirement that a tagged type only match a formal derived type that is a private extension. This is necessary to prevent type conversions that would not be allowed outside of the generic. We expect that this will be rare, as it only can happen if the formal derived type does not accurately describe the actual type; in most such cases, extension will be desired and a private extension used so that is allowed.

28.p/5
correction

The predicates of an ancestor subtype are considered part of the contract for a formal derived type, even if the ancestor subtype is unconstrained. This means, for instance, if the ancestor subtype is a subtype of Float with a predicate, then an actual subtype with a different predicate is illegal in Ada 2022 while it would have been allowed in Ada 2012. Cases like this are quite unlikely and will be detected at compile-time if they occur.

Wording Changes from Ada 2012

28.q/4

Corrigendum: The assume the worst rule for determining within a generic body whether a type is unconstrained in any partial view was moved here. While AI05-0041-1 added it to 3.10.2, it's also needed (at least) in 4.6 and 6.4.1. Thus, it was moved here so that it applies generally.

12.5.2 Formal Scalar Types

1/2

A formal scalar type is one defined by any of the formal_type_definitions in this subclause. [The category determined for a formal scalar type is the category of all discrete, signed integer, modular, floating point, ordinary fixed point, or decimal types.]

1.a/2
proof

The second rule follows from the rule in 12.5 that says that the category is determined by the one given in the name of the syntax production. The effect of the rule is repeated here to give a capsule summary of what this subclause is about.

1.b/2
ramification

The “category of a type” includes any classes that the type belongs to.

Syntax

2

formal_discrete_type_definition ::= (<>)

3
formal_signed_integer_type_definition ::= range<>
4
formal_modular_type_definition ::= mod<>
5
formal_floating_point_definition ::= digits<>
6
formal_ordinary_fixed_point_definition ::= delta<>
7
formal_decimal_fixed_point_definition ::= delta<>digits<>

Legality Rules

8

The actual type for a formal scalar type shall not be a nonstandard numeric type.

8.a
reason

This restriction is necessary because nonstandard numeric types have some number of restrictions on their use, which could cause contract model problems in a generic body. Note that nonstandard numeric types can be passed to formal derived and formal private subtypes, assuming they obey all the other rules, and assuming the implementation allows it (being nonstandard means the implementation might disallow anything).

Wording Changes from Ada 95

9.a/2

We change to “determines a category” as that is the new terminology (it avoids confusion, since not all interesting properties form a class).

12.5.3 Formal Array Types

1/2

[The category determined for a formal array type is the category of all array types.]

1.a/2
proof

This rule follows from the rule in 12.5 that says that the category is determined by the one given in the name of the syntax production. The effect of the rule is repeated here to give a capsule summary of what this subclause is about.

Syntax

2
formal_array_type_definition ::= array_type_definition

Legality Rules

3

The only form of discrete_subtype_definition that is allowed within the declaration of a generic formal (constrained) array subtype is a subtype_mark.

3.a
reason

The reason is the same as for forbidding constraints in subtype_indications (see 12.1).

4

For a formal array subtype, the actual subtype shall satisfy the following conditions:

5
  • The formal array type and the actual array type shall have the same dimensionality; the formal subtype and the actual subtype shall be either both constrained or both unconstrained.
  • 6
  • For each index position, the index types shall be the same, and the index subtypes (if unconstrained), or the index ranges (if constrained), shall statically match (see 4.9.1).
  • 7
  • The component subtypes of the formal and actual array types shall statically match.
  • 8
  • If the formal type has aliased components, then so shall the actual.
8.a
ramification

On the other hand, if the formal's components are not aliased, then the actual's components can be either aliased or not.

Examples

9

Example of formal array types:

10

-- given the generic package 11 generic type Item is private; type Index is (<>); type Vector is array (Index range <>) of Item; type Table is array (Index) of Item; package P is ... end P; 12 -- and the types 13 type Mix is array (Color range <>) of Boolean; type Option is array (Color) of Boolean; 14 -- then Mix can match Vector and Option can match Table 15 package R is new P(Item => Boolean, Index => Color, Vector => Mix, Table => Option); 16 -- Note that Mix cannot match Table and Option cannot match Vector

Incompatibilities With Ada 83

16.a

The check for matching of component subtypes and index subtypes or index ranges is changed from a runtime check to a compile-time check. The Ada 83 rule that “If the component type is not a scalar type, then the component subtypes shall be either both constrained or both unconstrained” is removed, since it is subsumed by static matching. Likewise, the rules requiring that component types be the same is subsumed.

Wording Changes from Ada 95

16.b/2

We change to “determines a category” as that is the new terminology (it avoids confusion, since not all interesting properties form a class).

12.5.4 Formal Access Types

1/2

[The category determined for a formal access type is the category of all access types.]

1.a/2
proof

This rule follows from the rule in 12.5 that says that the category is determined by the one given in the name of the syntax production. The effect of the rule is repeated here to give a capsule summary of what this subclause is about.

Syntax

2
formal_access_type_definition ::= access_type_definition

Legality Rules

3

For a formal access-to-object type, the designated subtypes of the formal and actual types shall statically match.

4/2

If and only if the general_access_modifier constant applies to the formal, the actual shall be an access-to-constant type. If the general_access_modifier all applies to the formal, then the actual shall be a general access-to-variable type (see 3.10). If and only if the formal subtype excludes null, the actual subtype shall exclude null.

4.a
ramification

If no _modifier applies to the formal, then the actual type may be either a pool-specific or a general access-to-variable type.

4.a.1/1
reason

{8652/0109} Matching an access-to-variable to a formal access-to-constant type cannot be allowed. If it were allowed, it would be possible to create an access-to-variable value designating a constant.

4.b/2

We require that the “excludes null” property match, because it would be difficult to write a correct generic for a formal access type without knowing this property. Many typical algorithms and techniques will not work for a subtype that excludes null (setting an unused component to null, default-initialized objects, and so on). Even Ada.Unchecked_Deallocation would fail for a subtype that excludes null. Most generics would end up with comments saying that they are not intended to work for subtypes that exclude null. We would rather that this sort of requirement be reflected in the contract of the generic.

5/3

For a formal access-to-subprogram subtype, the designated profiles of the formal and the actual shall be subtype conformant.

Examples

6

Example of formal access types:

7

-- the formal types of the generic package 8 generic type Node is private; type Link is access Node; package P is ... end P; 9 -- can be matched by the actual types 10 type Car; type Car_Name is access Car; 11 type Car is record Pred, Succ : Car_Name; Number : License_Number; Owner : Person; end record; 12 -- in the following generic instantiation 13 package R is new P(Node => Car, Link => Car_Name);

Incompatibilities With Ada 83

13.a

The check for matching of designated subtypes is changed from a runtime check to a compile-time check. The Ada 83 rule that “If the designated type is other than a scalar type, then the designated subtypes shall be either both constrained or both unconstrained” is removed, since it is subsumed by static matching.

Extensions to Ada 83

13.b

Formal access-to-subprogram subtypes and formal general access types are new concepts.

Wording Changes from Ada 95

13.c/2

Added a matching rule for subtypes that exclude null.

13.d/2

We change to “determines a category” as that is the new terminology (it avoids confusion, since not all interesting properties form a class).

Incompatibilities With Ada 2005

13.e/3
correction

Matching of formal access-to-subprogram types now uses subtype conformance rather than mode conformance, which is needed to plug a hole. This could cause some instantiations legal in Ada 95 and Ada 2005 to be rejected in Ada 2012. We believe that formal access-to-subprogram types occur rarely, and actuals that are not subtype conformant are rarer still, so this should not happen often. (In addition, one popular compiler has a bug that causes such instances to be rejected, so no code compiled with that compiler could have an incompatibility.)

12.5.5 Formal Interface Types

1/2

[The category determined for a formal interface type is the category of all interface types.]

1.a/2
proof

This rule follows from the rule in 12.5 that says that the category is determined by the one given in the name of the syntax production. The effect of the rule is repeated here to give a capsule summary of what this subclause is about.

1.b/2
ramification

Here we're taking advantage of our switch in terminology from “determined class” to “determined category”; by saying “category” rather than “class”, we require that any actual type be an interface type, not just some type derived from an interface type.

Syntax

2/2
formal_interface_type_definition ::= interface_type_definition

Legality Rules

3/2

The actual type shall be a descendant of every progenitor of the formal type.

4/2

The actual type shall be a limited, task, protected, or synchronized interface if and only if the formal type is also, respectively, a limited, task, protected, or synchronized interface.

4.a/2
discussion

We require the kind of interface type to match exactly because without that it is almost impossible to properly implement the interface.

Examples

5/5

Example of the use of a generic with a formal interface type, to establish a standard interface that all tasks will implement so they can be managed appropriately by an application-specific scheduler:

6/2

type Root_Work_Item is tagged private; 7/2

generic type Managed_Task is task interface; type Work_Item(<>) is new Root_Work_Item with private; package Server_Manager is task type Server is new Managed_Task with entry Start(Data : in out Work_Item); end Server; end Server_Manager;

Extensions to Ada 95

8.a/2

The formal interface type is new.