6.1.2 The Global and Global'Class Aspects
{
AI12-0079-3}
For a subprogram, an entry, a named 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):
The syntax for the
aspect_definition
used to define a Global aspect is as follows:
Aspect Description for Global: Global
object usage contract.
basic_global_mode ::= in |
in out |
out
global_designator ::= all |
synchronized |
global_name
{
AI12-0079-1}
{
AI12-0310-1}
global_name ::= object_name |
package_name
{
AI12-0079-3}
The Global aspect identifies the set of variables (which, for the purposes
of this clause includes all constants with some part being immutably
limited, or of a controlled type, private type, or private extension)
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.
The syntax for the
aspect_definition
used to define a Global'Class aspect is the same as that defined above
for
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.
Name Resolution Rules
{
AI12-0079-3}
A
global_name
shall resolve to statically denote an object or a package (including
a limited view of a package).
Static Semantics
{
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}
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 might be evaluated as part of the call, 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}
For a predefined operator of an elementary type, or the function representing
an enumeration literal, 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}
The following is defined in terms of operations; the rules apply to all
of the above kinds of entities.
{
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.
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;
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-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}
Implementations need not require that references to a constant object
that are considered variables in the above rules, be accounted for by
the Global or Global'Class aspect, if the implementation can determine
that the constant object is 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
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe