H.7.1 The Use_Formal and Dispatching Aspects

The Use_Formal and Dispatching aspects are provided to more precisely describe the use of generic formal parameters and dispatching calls within the execution of an operation, enabling more precise checking of conformance with the Nonblocking and global aspects that apply at the point of invocation of the operation.

For any declaration within a generic unit for which a global or Nonblocking aspect may be specified, other than a generic_formal_parameter_declaration, the following aspect may be specified to indicate which generic formal parameters are used by the associated entity:

For any declaration for which a global or Nonblocking aspect may be specified, other than for a library package, a generic library package, or a generic formal, the following aspect may be specified:

A formal_parameter_name in a Use_Formal aspect shall resolve to statically denote a formal subtype, a formal subprogram, or a formal object of an anonymous access-to-subprogram type of an enclosing generic unit or visible formal package.

The object_name of a dispatching_operation_specifier shall resolve to statically name an object (including possibly a formal parameter) of a tagged class-wide type T'Class, or of an access type designating a tagged class-wide type T'Class; the dispatching_operation_name of the dispatching_operation_specifier shall resolve to statically denote a dispatching operation associated with T. 

The formal parameter set is identified by a set of formal_parameter_names. Alternatively, the reserved word null may be used to indicate none of the generic formal parameters, or all to indicate all of the generic formal parameters, of any enclosing generic unit (or visible formal package) can be used within the execution of the operation. If there is no formal parameter set specified for an entity declared within a generic unit, it defaults to all.

The dispatching operation set is identified by a set of dispatching_operation_specifiers. It indicates that the Nonblocking and global effects of dispatching calls that match one of the specifiers, rather than being accounted for by the Nonblocking or global aspect, are instead to be accounted for by the invoker of the operation. A dispatching call matches a dispatching_operation_specifier if the name or prefix of the call statically denotes the same operation(s) as that of the dispatching_operation_specifier, and at least one of the objects controlling the call is denoted by, or designated by, a name that statically names the same object as that denoted by the object_name of the dispatching_operation_specifier.

In the absence of any dispatching_operation_specifiers, or if none of them match a dispatching call C within an operation P, Nonblocking and global aspects checks are performed at the point of the call C within P using the Nonblocking and Global'Class aspects that apply to the dispatching operation named in call C. If there is a match, any global access or potential blocking within the subprogram body invoked by the call C is ignored at the point of call within P. Instead, when the operation P itself is invoked, Nonblocking and global aspect checks are performed presuming each named dispatching operation is called at least once (with the named object controlling the call), but similarly ignoring those dispatching calls that would match a dispatching_operation_specifier applicable at the point of invocation of P.

Within an operation to which a Use_Formal aspect applies, if the formal parameter set is anything but all, then the only generic formal subtypes that may be used, the only formal subprograms that may be called, and the only formal objects of an anonymous access-to-subprogram type that may be dereferenced as part of a call or passed as the actual for an access parameter, are those included in the formal parameter set.

When an operation (or instance thereof) to which a Use_Formal aspect applies is invoked, Nonblocking and global aspect checks are performed presuming each generic formal parameter (or corresponding actual parameter) of the formal parameter set is used at least once.

An example of use of the Dispatching aspect: