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

6.1.2 The Global and Global'Class Aspects

{AI12-0425-1} The Global and Global'Class aspects of a program unit are used to identify the objects global to the unit that might be read or written during its execution. 


{AI12-0079-3} {AI12-0380-1} {AI12-0425-1} global_aspect_definition ::= 
  | Unspecified
  | global_mode global_designator
  | (global_aspect_element{; global_aspect_element})
{AI12-0079-3} {AI12-0380-1} global_aspect_element ::= 
    global_mode global_set
  | global_mode all
  | global_mode synchronized
global_mode ::= 
  | extended_global_mode
basic_global_mode ::= in | in out | out
global_set ::= global_name {, global_name}
global_designator ::= all | synchronized | global_name
{AI12-0079-1} {AI12-0310-1} global_name ::= object_name | package_name

Name Resolution Rules

{AI12-0079-3} {AI12-0425-1} {AI12-0427-1} A global_name shall resolve to statically name an object or a package (including a limited view of a package). 

Static Semantics

{AI12-0079-3} For a subprogram, an entry, an access-to-subprogram type, a task unit, a protected unit, or a library package or generic library package, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1):
{AI12-0079-3} {AI12-0425-1} Global

The Global aspect shall be specified with a global_aspect_definition.
Aspect Description for Global: Global object usage contract.
{AI12-0079-3} {AI12-0422-1} The Global aspect identifies the set of variables (which, for the purposes of this clause, includes all constants except those which are known to have no variable views (see 3.3)) that are global to a callable entity or task body, and that are read or updated as part of the execution of the callable entity or task body. If specified for a protected unit, it refers to all of the protected operations of the protected unit. Constants of any type may also be mentioned in a Global aspect.
{AI12-0079-3} If not specified or otherwise defined below, the aspect defaults to the Global aspect for the enclosing library unit if the entity is declared at library level, and to Unspecified otherwise. If not specified for a library unit, the aspect defaults to Global => null for a library unit that is declared Pure, and to Global => Unspecified otherwise. 
{AI12-0079-3} For a dispatching subprogram, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1):
{AI12-0079-3} {AI12-0425-1} Global'Class

The Global'Class aspect shall be specified with a global_aspect_definition. This aspect identifies an upper bound on the set of variables global to a dispatching operation that can be read or updated as a result of a dispatching call on the operation. If not specified, the aspect defaults to the Global aspect for the dispatching subprogram.
Aspect Description for Global'Class: Global object usage contract inherited on derivation.
{AI12-0380-1} Together, we refer to the Global and Global'Class aspects as global aspects.
{AI12-0079-3} A global_aspect_definition defines the Global or Global'Class aspect of some entity. The Global aspect identifies the sets of global variables that can be read, written, or modified as a side effect of executing the operation(s) associated with the entity. The Global'Class aspect associated with a dispatching operation of type T represents a restriction on the Global aspect on a corresponding operation of any descendant of type T.
{AI12-0079-3} {AI12-0416-1} The Global aspect for a callable entity defines the global variables that might be referenced as part of a call on the entity, including any assertion expressions that apply to the call (even if not enabled), including preconditions, postconditions, predicates, and type invariants.
{AI12-0079-3} The Global aspect for an access-to-subprogram object (or subtype) identifies the global variables that might be referenced when calling via the object (or any object of that subtype) including assertion expressions that apply.
{AI12-0079-3} {AI12-0405-1} For a predefined operator of an elementary type, the function representing an enumeration literal, or any other static function (see 4.9), the Global aspect is null. For a predefined operator of a composite type, the Global aspect of the operator defaults to that of the enclosing library unit (unless a Global aspect is specified for the type — see H.7).
{AI12-0079-3} {AI12-0380-1} The following is defined in terms of operations that are performed by or on behalf of an entity. The rules on operations apply to the entity(s) associated with those operations.
Discussion: {AI12-0380-1} The operations performed by a callable entity are those associated with the body of the entity. For other kinds of entities (such as subtypes, see H.7), we explicitly list the associated operations. 
{AI12-0079-3} The global variables associated with any global_mode can be read as a side effect of an operation. The in out and out global_modes together identify the set of global variables that can be updated as a side effect of an operation. Creating an access-to-variable value that designates an object is considered an update of the designated object, and creating an access-to-constant value that designates an object is considered a read of the designated object.
{AI12-0079-3} The overall set of objects associated with each global_mode includes all objects identified for the mode in the global_aspect_definition.
{AI12-0079-3} A global_set identifies a global variable set as follows:
all identifies the set of all global variables;
synchronized identifies the set of all synchronized variables (see 9.10), as well as variables of a composite type all of whose non-discriminant subcomponents are synchronized;
global_name{, global_name} identifies the union of the sets of variables identified by the global_names in the list, for the following forms of global_name:
object_name identifies the specified global variable (or constant);
package_name identifies the set of all variables declared in the private part or body of the package, or anywhere within a private descendant of the package.

Legality Rules

{AI12-0079-1} Within a global_aspect_definition, a given global_mode shall be specified at most once. Similarly, within a global_aspect_definition, a given entity shall be named at most once by a global_name.
{AI12-0079-3} If an entity (other than a library package or generic library package) has a Global aspect other than Unspecified or in out all, then the associated operation(s) shall read only those variables global to the entity that are within the global variable set associated with the in, in out, or out global_modes, and the operation(s) shall update only those variables global to the entity that are within the global variable set associated with either the in out or out global_modes. In the absence of the No_Hidden_Indirect_Globals restriction (see H.4), this ignores objects reached via a dereference of an access value. The above rule includes any possible Global effects of calls occurring during the execution of the operation, except for the following excluded calls:
calls to formal subprograms;
calls associated with operations on formal subtypes;
calls through formal objects of an access-to-subprogram type;
calls through access-to-subprogram parameters;
calls on operations with Global aspect Unspecified.
{AI12-0079-3} The possible Global effects of these excluded calls (other than those that are Unspecified) are taken into account by the caller of the original operation, by presuming they occur at least once during its execution. For calls that are not excluded, the possible Global effects of the call are those permitted by the Global aspect of the associated entity, or by its Global'Class aspect if a dispatching call.
Ramification: For a predefined equality operator of a composite type, the possible Global effects includes those of the equality operations invoked as part of the evaluation of the operator (which might not be predefined and thus might have a different Global specification than the component types).
{AI12-0079-3} If a Global aspect other than Unspecified or in out all applies to an access-to-subprogram type, then the prefix of an Access attribute_reference producing a value of such a type shall denote a subprogram whose Global aspect is not Unspecified and is covered by that of the result type, where a global aspect G1 is covered by a global aspect G2 if the set of variables that G1 identifies as readable or updatable is a subset of the corresponding set for G2. Similarly on a conversion to such a type, the operand shall be of a named access-to-subprogram type whose Global aspect is covered by that of the target type.
{AI12-0079-3} If an implementation-defined global_mode applies to a given set of variables, an implementation-defined rule determines what sort of references to them are permitted.
{AI12-0079-1} For a subprogram that is a dispatching operation of a tagged type T, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the in out mode, of the Global'Class aspect of a corresponding dispatching subprogram of any ancestor of T, unless the aspect of that ancestor is Unspecified.

Implementation Permissions

{AI12-0079-3} An implementation need not require that all references to a constant object be accounted for by the Global or Global'Class aspect when it is considered a variable in the above rules if the implementation can determine that the object is in fact immutable.
Ramification: In particular, this allows the implementation to violate privacy in order to determine whether a constant needs to be covered by a Global aspect.
{AI12-0079-3} Implementations may perform additional checks on calls to operations with an Unspecified Global aspect to ensure that they do not violate any limitations associated with the point of call.
Discussion: In this sense, Global => Unspecified is not permission to violate the caller's Global restrictions. It is rather that the implementor of the subprogram is presuming other means are being used to ensure safety. Note the No_Unspecified_Globals Restriction (H.4), which prevents the use of Unspecified with the Global aspect in a given partition. 
{AI12-0079-3} Implementations may extend the syntax or semantics of the Global aspect in an implementation-defined manner[; for example, supporting additional global_modes].
Implementation defined: Any extensions of the Global aspect.
Reason: This is intended to allow preexisting usages from SPARK 2014 to remain acceptable in conforming implementations, as well as to provide flexibility for future enhancements. Note the word “extend” in this permission; we expect that any aspect usage that conforms with the (other) rules of this clause will be accepted by any Ada implementation, regardless of any implementation-defined extensions. 
7  {AI12-0312-1} For an example of the use of these aspects and attributes, see the Vector container definition in A.18.2.

Extensions to Ada 2012

{AI12-0079-1} {AI12-0240-6} {AI12-0310-1} The Global and Global'Class aspects are new. 

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