7.3 Private Types and Private Extensions
This Reference Manual output has not been verified, and may contain omissions or errors. Report any problems on the tracking issue
[The declaration (in the visible part of a package) of a type as a private type or private extension serves to separate the characteristics that can be used directly by outside program units (that is, the logical properties) from other characteristics whose direct use is confined to the package (the details of the definition of the type itself). See 3.9.1 for an overview of type extensions. ]
Language Design Principles
Syntax
2/3private_type_declaration ::=
type defining_identifier [discriminant_part] is [[abstract] tagged] [limited] private
[aspect_specification];
private_extension_declaration ::=
type defining_identifier [discriminant_part] is
[abstract] [limited | synchronized] new ancestor_subtype_indication
[and interface_list] with private
[aspect_specification];
Legality Rules
4A private_type_declaration or private_extension_declaration declares a partial view of the type; such a declaration is allowed only as a declarative_item of the visible part of a package, and it requires a completion, which shall be a full_type_declaration that occurs as a declarative_item of the private part of the package. [ The view of the type declared by the full_type_declaration is called the full view.] A generic formal private type or a generic formal private extension is also a partial view.
[A type shall be completely defined before it is frozen (see 3.11.1 and 13.14). Thus, neither the declaration of a variable of a partial view of a type, nor the creation by an allocator of an object of the partial view are allowed before the full declaration of the type. Similarly, before the full declaration, the name of the partial view cannot be used in a generic_instantiation or in a representation item.]
[A private type is limited if its declaration includes the reserved word limited; a private extension is limited if its ancestor type is a limited type that is not an interface type, or if the reserved word limited or synchronized appears in its definition.] If the partial view is nonlimited, then the full view shall be nonlimited. If a tagged partial view is limited, then the full view shall be limited. [On the other hand, if an untagged partial view is limited, the full view may be limited or nonlimited.]
If the partial view is tagged, then the full view shall be tagged. [On the other hand, if the partial view is untagged, then the full view may be tagged or untagged.] In the case where the partial view is untagged and the full view is tagged, no derivatives of the partial view are allowed within the immediate scope of the partial view; [derivatives of the full view are allowed.]
package P1 is
type T1 is tagged limited private;
procedure Foo(X : in T1'Class);
private
type T1 is tagged null record; -- Illegal!
-- This should say “tagged limited null record”.
end P1;
7.f/1package body P1 is
type A is access T1'Class;
Global : A;
procedure Foo(X : in T1'Class) is
begin
Global := new T1'Class'(X);
-- This would be illegal if the full view of
-- T1 were limited, like it's supposed to be.
end Foo;
end P1;
7.g/2with P1;
package P2 is
type T2(D : access Integer)
is new P1.T1 with
record
My_Task : Some_Task_Type; -- Trouble!
end record;
end P2;
7.h/1with P1;
with P2;
procedure Main is
Local : aliased Integer;
Y : P2.T2(D => Local'Access);
begin
P1.Foo(Y);
end Main;
package P is
type Parent is private;
private
type Parent is tagged
record
X: Integer;
end record;
end P;
7.m/1with P;
package Q is
type T is new P.Parent;
end Q;
7.nwith Q; use Q;
package body P is
... T'Class ... -- Illegal!
Object: T;
... Object.X ... -- Illegal!
... Parent(Object).X ... -- OK.
end P;
type_conversion.If a full type has a partial view that is tagged, then:
- the partial view shall be a synchronized tagged type (see 3.9.4) if and only if the full type is a synchronized tagged type;
- the partial view shall be a descendant of an interface type (see 3.9.4) if and only if the full type is a descendant of the interface type.
package P is
package Pkg is
type Ifc is interface;
procedure Foo (X : Ifc) is abstract;
end Pkg;
7.r/2type Parent_1 is tagged null record;
7.s/2type T1 is new Parent_1 with private;
private
type Parent_2 is new Parent_1 and Pkg.Ifc with null record;
procedure Foo (X : Parent_2); -- Foo #1
7.t/2type T1 is new Parent_2 with null record; -- Illegal.
end P;
7.u/2with P;
package P_Client is
type T2 is new P.T1 and P.Pkg.Ifc with null record;
procedure Foo (X : T2); -- Foo #2
X : T2;
end P_Client;
7.v/2with P_Client;
package body P is
...
7.w/5procedure Bar (X : T1'Class) is
begin
Pkg.Foo (Pkg.Ifc'Class (X) ); -- should call Foo #1 or an override thereof
end;
7.x/2begin
Pkg.Foo (Pkg.Ifc'Class (P_Client.X)); -- should call Foo #2
Bar (T1'Class (P_Client.X));
end P;
The ancestor subtype of a private_extension_declaration is the subtype defined by the ancestor_subtype_indication; the ancestor type shall be a specific tagged type. The full view of a private extension shall be derived (directly or indirectly) from the ancestor type. In addition to the places where Legality Rules normally apply (see 12.3), the requirement that the ancestor be specific applies also in the private part of an instance of a generic unit.
generic_instantiations. If the reserved word limited appears in a private_extension_declaration, the ancestor type shall be a limited type. If the reserved word synchronized appears in a private_extension_declaration, the ancestor type shall be a limited interface.
If the declaration of a partial view includes a known_discriminant_part, then the full_type_declaration shall have a fully conforming [(explicit)] known_discriminant_part [(see 6.3.1 )]. [The ancestor subtype may be unconstrained; the parent subtype of the full view is required to be constrained (see 3.7).]
known_discriminant_part, then the full view has to be a composite, non-array type, since only such types may have known discriminants. Also, the full view cannot inherit the discriminants in this case; the known_discriminant_part has to be explicit.package P is
type T(D : Integer) is private;
private
type T is new Some_Other_Type; -- Illegal!
end P;
unknown_discriminant_part. If a private extension inherits known discriminants from the ancestor subtype, then the full view shall also inherit its discriminants from the ancestor subtype, and the parent subtype of the full view shall be constrained if and only if the ancestor subtype is constrained.
If the full_type_declaration for a private extension includes a derived_type_definition, then the reserved word limited shall appear in the full_type_declaration if and only if it also appears in the private_extension_declaration.
derived_type_definition, as we want to allow task and protected types to complete extensions of synchronized interfaces. [If a partial view has unknown discriminants, then the full_type_declaration may define a definite or an indefinite subtype, with or without discriminants.]
If a partial view has neither known nor unknown discriminants, then the full_type_declaration shall define a definite subtype.
If the ancestor subtype of a private extension has constrained discriminants, then the parent subtype of the full view shall impose a statically matching constraint on those discriminants.
package P is
type T2 is new T1(Discrim => 3) with private;
private
type T2 is new T1(Discrim => 999) -- Illegal!
with record ...;
end P;
type One_Discrim(A: Integer) is tagged ...;
...
package P is
type Two_Discrims(B: Boolean; C: Integer) is new One_Discrim with private;
private
type Two_Discrims(B: Boolean; C: Integer) is new One_Discrim(A => C) with
record
...
end record;
end P;
Static Semantics
14A private_type_declaration declares a private type and its first subtype. Similarly, a private_extension_declaration declares a private extension and its first subtype.
private_type_declaration; that is, a private type other than a generic formal private type. Similarly, a package-private extension is one declared by a private_extension_declaration. These terms are not used in the RM95 version of this document. A declaration of a partial view and the corresponding full_type_declaration define two views of a single type. The declaration of a partial view together with the visible part define the operations that are available to outside program units; the declaration of the full view together with the private part define other operations whose direct use is possible only within the declarative region of the package itself. Moreover, within the scope of the declaration of the full view, the characteristics (see 3.4) of the type are determined by the full view; in particular, within its scope, the full view determines the classes that include the type, which components, entries, and protected subprograms are visible, what attributes and other predefined operations are allowed, and whether the first subtype is static. See 7.3.1.
For a private extension, the characteristics (including components, but excluding discriminants if there is a new discriminant_part specified), 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 record extension are determined by those of its parent type and its progenitor types (see 3.4 and 7.3.1).
Dynamic Semantics
17The elaboration of a private_type_declaration creates a partial view of a type. The elaboration of a private_extension_declaration elaborates the ancestor_subtype_indication, and creates a partial view of a type.
private_type_declaration is defined to be a composite view (in 3.2). The full view of the type can be elementary or composite. A private extension is also composite, as is its full view.unknown_discriminant_part is a way of preventing clients from creating uninitialized objects of the type; they are then forced to initialize each object by calling some operation declared in the visible part of the package. full_type_declaration that specifies implementation details of the private type. The clients of the package are like the body of the generic; usage of the private type in these places is restricted to the operations defined by the contract.private_type_declaration to be a subtype_declaration, but the semantics just won't work.) This difference is behind the fact that a generic actual type can be class-wide, whereas the completion of a private type always declares a specific type. private_extension_declaration and the parent type specified in the corresponding declaration of a record extension given in the private part can be different . If the ancestor type is not an interface type, the parent type of the full view can be any descendant of the ancestor type. In this case, for a primitive subprogram that is inherited from the ancestor type and not overridden, the formal parameter names and default expressions (if any) come from the corresponding primitive subprogram of the specified ancestor type, while the body comes from the corresponding primitive subprogram of the parent type of the full view. See 3.9.2.private_extension_declaration is an interface type, the parent type can be any type so long as the full view is a descendant of the ancestor type. The progenitor types specified in a private_extension_declaration and the progenitor types specified in the corresponding declaration of a record extension given in the private part are not necessarily the same — it is only necessary that the private extension and the record extension be descended from the same set of interfaces. Examples
22Examples of private type declarations:
type Key is private;
type File_Name is limited private;
Example of a private extension declaration:
type List is new Ada.Finalization.Controlled with private;
Extensions to Ada 83
private_type_declaration is augmented to allow the reserved word tagged.Wording Changes from Ada 83
Extensions to Ada 95
interface_list to private extensions to support interfaces and multiple inheritance (see 3.9.4).Extensions to Ada 2005
aspect_specification can be used in a private_type_declaration and a private_extension_declaration. This is described in 13.1.1. Wording Changes from Ada 2005
7.3.1 Private Operations
1[For a type declared in the visible part of a package or generic package, certain operations on the type do not become visible until later in the package — either in the private part or the body. Such private operations are available only inside the declarative region of the package or generic package.]
Static Semantics
2The predefined operators that exist for a given type are determined by the classes to which the type belongs. For example, an integer type has a predefined "+" operator. In most cases, the predefined operators of a type are declared immediately after the definition of the type; the exceptions are explained below. Inherited subprograms are also implicitly declared immediately after the definition of the type, except as stated below.
{8652/0019} For a composite type, the characteristics (see 7.3) of the type are determined in part by the characteristics of its component types. At the place where the composite type is declared, the only characteristics of component types used are those characteristics visible at that place. If later immediately within the declarative region in which the composite type is declared additional characteristics become visible for a component type, then any corresponding characteristics become visible for the composite type. Any additional predefined operators are implicitly declared at that place. If there is no such place, then additional predefined operators are not declared at all, but they still exist.
{8652/0019} The corresponding rule applies to a type defined by a derived_type_definition, if there is a place immediately within the declarative region in which the type is declared where additional characteristics of its parent type become visible.
{8652/0019} [For example, an array type whose component type is limited private becomes nonlimited if the full view of the component type is nonlimited and visible at some later place immediately within the declarative region in which the array type is declared. In such a case, the predefined "=" operator is implicitly declared at that place, and assignment is allowed after that place.]
The characteristics and constraints of the designated subtype of an access type follow a somewhat different rule. The view of the designated subtype of (a view of) an access type at a given place is determined by the view of the designated subtype that is visible at that place, rather than the view at the place where the access type is declared.
A type is a descendant of the full view of some ancestor of its parent type only if the current view it has of its parent is a descendant of the full view of that ancestor. More generally, at any given place, a type is descended from the same view of an ancestor as that from which the current view of its parent is descended. This view determines what characteristics are inherited from the ancestor[, and, for example, whether the type is considered to be a descendant of a record type, or a descendant only through record extensions of a more distant ancestor].
[Furthermore, it is possible for there to be places where a derived type is known to be derived indirectly from an ancestor type, but is not a descendant of even a partial view of the ancestor type, because the parent of this derived type is not visibly a descendant of the ancestor. In this case, the derived type inherits no characteristics from that ancestor, but nevertheless is within the derivation class of the ancestor for the purposes of type conversion, the "covers" relationship, and matching against a formal derived type. In this case the derived type is effectively a descendant of an incomplete view of the ancestor.]
package P is
type T is private;
C : constant T;
private
type T is new Integer;
C : constant T := 42;
end P;
5.c/4with P;
package Q is
type T2 is new P.T; -- T2 is not a descendant of Integer
end Q;
5.d/4with Q;
package P.Child is
type T3 is new Q.T2;
private
-- Here T3 is known to be indirectly derived from Integer, but inherits
-- no characteristics from Integer, since T2 inherits no characteristics
-- from Integer.
-- However, we allow an explicit conversion of T3 to/from Integer.
-- Hence, T3 is effectively a descendant of an "incomplete" view of Integer.
Int : Integer := 52;
V : T3 := T3(P.C); -- Legal: conversion allowed
W : T3 := T3(Int); -- Legal: conversion allowed
X : T3 := T3(42); -- Error: T3 is not a numeric type
Y : T3 := X + 1; -- Error: no visible "+" operator
Z : T3 := T3(Integer(W) + 1); -- Legal: convert to Integer first
end P.Child;
{8652/0019} Inherited primitive subprograms follow a different rule. For a derived_type_definition, each inherited primitive subprogram is implicitly declared at the earliest place, if any, immediately within the declarative region in which the type_declaration occurs, but after the type_declaration, where the corresponding declaration from the parent is visible. If there is no such place, then the inherited subprogram is not declared at all, but it still exists. [For a tagged type, it is possible to dispatch to an inherited subprogram that is not declared at all.]
For a private_extension_declaration, each inherited subprogram is declared immediately after the private_extension_declaration if the corresponding declaration from the ancestor is visible at that place. Otherwise, the inherited subprogram is not declared for the private extension, [though it can be for the full type].
private_extension_declaration will be completed with a full_type_declaration, so we can hang the necessary private implicit declarations on the full_type_declaration. package Parent is
type Root is tagged null record;
procedure Op1(X : Root);
7.etype My_Int is range 1..10;
private
procedure Op2(X : Root);
7.ftype Another_Int is new My_Int;
procedure Int_Op(X : My_Int);
end Parent;
7.gwith Parent; use Parent;
package Unrelated is
type T2 is new Root with null record;
procedure Op2(X : T2);
end Unrelated;
7.hpackage Parent.Child is
type T3 is new Root with null record;
-- Op1(T3) implicitly declared here.
7.ipackage Nested is
type T4 is new Root with null record;
private
...
end Nested;
private
-- Op2(T3) implicitly declared here.
...
end Parent.Child;
7.jwith Unrelated; use Unrelated;
package body Parent.Child is
package body Nested is
-- Op2(T4) implicitly declared here.
end Nested;
7.ktype T5 is new T2 with null record;
end Parent.Child;
package P is
type Comp1 is private;
private
type Comp1 is new Boolean;
end P;
7.upackage P.Q is
package R is
type Comp2 is limited private;
type A is array(Integer range <>) of Comp2;
private
type Comp2 is new Comp1;
-- A becomes nonlimited here.
-- "="(A, A) return Boolean is implicitly declared here.
...
end R;
private
-- Now we find out what Comp1 really is, which reveals
-- more information about Comp2, but we're not within
-- the immediate scope of Comp2, so we don't do anything
-- about it yet.
end P.Q;
7.vpackage body P.Q is
package body R is
-- Things like "xor"(A,A) return A are implicitly
-- declared here.
end R;
end P.Q;
package Outer is
package Inner is
type Inner_Type is private;
private
type Inner_Type is new Boolean;
end Inner;
type Outer_Type is array(Natural range <>) of Inner.Inner_Type;
end Outer;
7.v.3/1package body Outer is
package body Inner is
-- At this point, we can see that Inner_Type is a Boolean type.
-- But we don't want Outer_Type to gain an "and" operator here.
end Inner;
end Outer;
[The Class attribute is defined for tagged subtypes in 3.9. In addition,] for every subtype S of an untagged private type whose full view is tagged, the following attribute is defined:
S'Class
- Denotes the class-wide subtype corresponding to the full view of S. This attribute is allowed only from the beginning of the private part in which the full view is declared, until the declaration of the full view. [After the full view, the Class attribute of the full view can be used.]
assignment_statements.Examples
14Example of a type with private operations:
package Key_Manager is
type Key is private;
Null_Key : constant Key; -- a deferred constant declaration (see 7.4)
procedure Get_Key(K : out Key);
function "<" (X, Y : Key) return Boolean;
private
type Key is new Natural;
Null_Key : constant Key := Key'First;
end Key_Manager;
16package body Key_Manager is
Last_Key : Key := Null_Key;
procedure Get_Key(K : out Key) is
begin
Last_Key := Last_Key + 1;
K := Last_Key;
end Get_Key;
17function "<" (X, Y : Key) return Boolean is
begin
return Natural(X) < Natural(Y);
end "<";
end Key_Manager;
Outside of the package Key_Manager, the operations available for objects of type Key include assignment, the comparison for equality or inequality, the procedure Get_Key and the operator "<"; they do not include other relational operators such as ">=", or arithmetic operators.
The explicitly declared operator "<" hides the predefined operator "<" implicitly declared by the full_type_declaration. Within the body of the function, an explicit conversion of X and Y to the subtype Natural is necessary to invoke the "<" operator of the parent type. Alternatively, the result of the function can be written as not (X >= Y), since the operator ">=" is not redefined.
The value of the variable Last_Key, declared in the package body, remains unchanged between calls of the procedure Get_Key. (See also the NOTEs of 7.2.)
Wording Changes from Ada 83
Wording Changes from Ada 95
assignment_statements. Wording Changes from Ada 2005
Wording Changes from Ada 2012
7.3.2 Type Invariants
1/5For 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 aprivate_type_declaration, on aprivate_extension_declaration, or on afull_type_declarationthat 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 aprivate_type_declaration, aprivate_extension_declaration, or afull_type_declarationfor 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
4/3The 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
6/3[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
7/3[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_definitionfor 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
9/4If 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.
- A boundary entity might assign an invariant-violating value to a global variable that is visible to client code.
- 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.
- 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.
- 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).
- 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.
Examples
25/5Example of a work scheduler where only urgent work can be scheduled for weekends:
package Work_Orders is
27/5-- See 3.5.1 for type declarations of Level, Day, and Weekday
28/5type Work_Order is private with
Type_Invariant => Day_Scheduled (Work_Order) in Weekday
or else Priority (Work_Order) = Urgent;
29/5function Schedule_Work (Urgency : in Level;
To_Occur : in Day) return Work_Order
with Pre => Urgency = Urgent or else To_Occur in Weekday;
30/5function Day_Scheduled (Order : in Work_Order) return Day;
31/5function Priority (Order : in Work_Order) return Level;
32/5procedure 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);
33/5private
34/5type Work_Order is record
Scheduled : Day;
Urgency : Level;
end record;
35/5end Work_Orders;
36/5package body Work_Orders is
37/5function Schedule_Work (Urgency : in Level;
To_Occur : in Day) return Work_Order is
(Scheduled => To_Occur, Urgency => Urgency);
38/5function Day_Scheduled (Order : in Work_Order) return Day is
(Order.Scheduled);
39/5function Priority (Order : in Work_Order) return Level is
(Order.Urgency);
40/5procedure 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;
41/5end Work_Orders;
Extensions to Ada 2005
Inconsistencies With Ada 2012
Incompatibilities With Ada 2012
Extensions to Ada 2012
Wording Changes from Ada 2012
7.3.3 Default Initial Conditions
1/5For a private type or private extension (including a generic formal type), the following language-defined assertion aspect may be specified with an aspect_specification (see 13.1.1):
Default_Initial_Condition
- This aspect shall be specified by an
expression, called a default initial condition expression. Default_Initial_Condition may be specified on aprivate_type_declaration, aprivate_extension_declaration, aformal_private_type_definition, or aformal_derived_type_definition. [The Default_Initial_Condition aspect is not inherited, but its effects are additive, as defined below.]
Name Resolution Rules
3/5The expected type for a default initial condition expression is any boolean type.
Within a default initial condition expression associated with a declaration for a type T, a name that denotes the declaration is interpreted as a current instance of a notional (nonabstract) formal derived type NT with ancestor T, that has directly visible primitive operations.
Legality Rules
5/5The Default_Initial_Condition aspect shall not be specified for a type whose partial view has unknown discriminants[, whether explicitly declared or inherited].
Static Semantics
6/5If the Default_Initial_Condition aspect is specified for a type T, then the default initial condition expression applies to T and to all descendants of T.
Dynamic Semantics
7/5If one or more default initial condition expressions apply to a [(nonabstract)] type T, then a default initial condition check is performed after successful initialization of an object of type T by default (see 3.3.1). In the case of a controlled type, the check is performed after the call to the type's Initialize procedure (see 7.6).
If performing checks is required by the Default_Initial_Condition assertion policy (see 11.4.2) in effect at the point of the corresponding aspect_specification applicable to a given type, then the respective default initial condition expression is considered enabled.
The default initial condition check consists of the evaluation of each enabled default initial condition expression that applies to T. Any operations within such an expression that were resolved as primitive operations of the (notional) formal derived type NT, are in the evaluation of the expression resolved as for a formal derived type in an instance with T as the actual type for NT (see 12.5.1). These evaluations, if there are more than one, are performed in an arbitrary order. If any of these evaluate to False, Assertions.Assertion_Error is raised at the point of the object initialization.
[For a generic formal type T, default initial condition checks performed are as determined by the actual type, along with any default initial condition of the formal type itself.]
Implementation Permissions
11/5Implementations may extend the syntax or semantics of the Default_Initial_Condition aspect in an implementation-defined manner.
Extensions to Ada 2012
7.3.4 Stable Properties of a Type
1/5Certain characteristics of an object of a given type are unchanged by most of the primitive operations of the type. Such characteristics are called stable properties of the type.
Static Semantics
2/5A property function of type T is a function with a single parameter of type T or of a class-wide type that covers T.
A type property aspect definition is a list of names written in the syntax of a positional_array_aggregate. A subprogram property aspect definition is a list of names, each optionally preceded by reserved word not, also written in the syntax of a positional_array_aggregate.
name would technically be a parenthesized expression rather than an aggregate; we mean to include that here. We say "syntax of a positional_array_aggregate" to hopefully clarify that the specification is in no other way an actual aggregate. For a nonformal private type, nonformal private extension, or full type that does not have a partial view, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
Stable_Properties
- This aspect shall be specified by a type property aspect definition; each
nameshall statically denote a single property function of the type. This aspect defines the specific stable property functions of the associated type.
Stable_Properties'Class
- This aspect shall be specified by a type property aspect definition; each
nameshall statically denote a single property function of the type. This aspect defines the class-wide stable property functions of the associated type. [Unlike most class-wide aspects, Stable_Properties'Class is not inherited by descendant types and subprograms, but the enhanced class-wide postconditions are inherited in the normal manner.]
The specific and class-wide stable properties of a type together comprise the stable properties of the type.
For a primitive subprogram, the following language-defined aspects may be specified with an aspect_specification (see 13.1.1):
Stable_Properties
- This aspect shall be specified by a subprogram property aspect definition; each
nameshall statically denote a single property function of a type for which the associated subprogram is primitive. 10/5
Stable_Properties'Class- This aspect shall be specified by a subprogram property aspect definition; each
nameshall statically denote a single property function of a tagged type for which the associated subprogram is primitive. [Unlike most class-wide aspects, Stable_Properties'Class is not inherited by descendant subprograms, but the enhanced class-wide postconditions are inherited in the normal manner.]
Legality Rules
11/5A stable property function of a type T shall have a nonlimited return type and shall be:
- a primitive function with a single parameter of mode in of type T; or
- a function that is declared immediately within the declarative region in which an ancestor type of T is declared and has a single parameter of mode in of a class-wide type that covers T.
In a subprogram property aspect definition for a subprogram S:
- all or none of the items shall be preceded by not;
- any property functions mentioned after not shall be a stable property function of a type for which S is primitive.
If a subprogram_renaming_declaration declares a primitive subprogram of a type T, then the renamed callable entity shall also be a primitive subprogram of type T and the two primitive subprograms shall have the same specific stable property functions and the same class-wide stable property functions (see below).
Static Semantics
18/5For a primitive subprogram S of a type T, the specific stable property functions of S for type T are:
- if S has an aspect Stable_Properties specified that does not include not, those functions denoted in the aspect Stable_Properties for S that have a parameter of T or T'Class;
- if S has an aspect Stable_Properties specified that includes not, those functions denoted in the aspect Stable_Properties for T, excluding those denoted in the aspect Stable_Properties for S;
- if S does not have an aspect Stable_Properties, those functions denoted in the aspect Stable_Properties for T, if any.
A similar definition applies for class-wide stable property functions by replacing aspect Stable_Properties with aspect Stable_Properties'Class in the above definition.
The explicit specific postcondition expression for a subprogram S is the expression directly specified for S with the Post aspect. Similarly, the explicit class-wide postcondition expression for a subprogram S is the expression directly specified for S with the Post'Class aspect.
For a primitive subprogram S of a type T that has a parameter P of type T, the parameter is excluded from stable property checks if:
- S is a stable property function of T;
- P has mode out;
- the Global aspect of S is null, and P has mode in and the mode is not overridden by a global aspect.
For every primitive subprogram S of a type T that is not an abstract subprogram or null procedure, the specific postcondition expression of S is modified to include expressions of the form F(P) = F(P)'Old, all anded with each other and any explicit specific postcondition expression, with one such equality included for each specific stable property function F of S for type T that does not occur in the explicit specific postcondition expression of S, and P is each parameter of S that has type T and is not excluded from stable property checks. The resulting specific postcondition expression of S is used in place of the explicit specific postcondition expression of S [when interpreting the meaning of the postcondition as defined in 6.1.1].
For every primitive subprogram S of a type T, the class-wide postcondition expression of S is modified to include expressions of the form F(P) = F(P)'Old, all anded with each other and any explicit class-wide postcondition expression, with one such equality included for each class-wide stable property function F of S for type T that does not occur in any class-wide postcondition expression that applies to S, and P is each parameter of S that has type T and is not excluded from stable property checks. The resulting class-wide postcondition expression of S is used in place of the explicit class-wide postcondition expression of S [when interpreting the meaning of the postcondition as defined in 6.1.1].
The equality operation that is used in the aforementioned equality expressions is as described in the case of an individual membership test whose membership_choice is a choice_simple_expression (see 4.5.2).
The Post expression additions described above are enabled or disabled depending on the Post assertion policy that is in effect at the point of declaration of the subprogram S. A similar rule applies to the Post'Class expression additions.