Version 1.10 of ai05s/ai05-0186-1.txt

Unformatted version of ai05s/ai05-0186-1.txt version 1.10
Other versions for file ai05s/ai05-0186-1.txt

!standard 13.3.4 (0)          10-02-03 AI05-0186-1/05
!class amendment 09-11-02
!status No Action (9-0-1) 10-06-19
!status work item 09-11-02
!status received 09-11-02
!priority Medium
!difficulty Medium
!subject Global-in and global-out annotations
!summary
Annotations are provided to describe the use of global objects by subprograms.
!problem
We're considering adding many aspects to Ada (see AI05-0145-1 and AI05-0146-1) in order to increase the ability of a programmer to specify contracts for types and subprograms. These contracts are defined to be checked at runtime, but are intended to be potentially checked (at least in part) statically.
However, without knowledge of side-effects of functions used in the aspects, a tool has to assume the worst about any user-defined functions. For example, that the result of a function can change even when called with the same operands. Other assumptions could cause incorrect programs to be accepted as correct, and if the assumptions were used to omit "proved" aspects, to erroneous execution. Both of these results are unacceptable for a feature intended to improve the correctness of programs.
The worst-case assumptions pretty much prevent any analysis unless the bodies of any user-defined functions used in the aspects are available. This is bad, as it prevents analysis of programs as they are constructed. If the body is not available, no analysis is possible. Moreover, analysis depending on a body require creating pseudo body dependencies (if the body is changed, any analysis depending on the properties of that body would have to be performed again); but the language does not allow these to be "real" body dependencies (any recompilation needed has to occur automatically).
Ideally, analysis at the initial compile-time of a unit would be possible, as it is important to detect errors as soon as possible. More information about function side-effects is needed in the specification of subprograms in order to accomplish that goal.
!proposal
Add global in and global out annotations to Ada, for subprograms, packages, and types. Add related annotations for dispatching subprograms and access-to-subprogram types.
The global annotations for types cover default initialization/adjustment/finalization. The global annotations for packages cover operations that occur as part of the elaboration for packages.
!wording
Add a new section:
13.3.4 Global usage annotation
Semi-formal description: [Editor's note: This part depends heavily on the unfinished AI05-0183-1; it's not worth trying to describe these rules until that AI is finished.]
Add to the aspect syntax given in AI05-0183-1:
Aspect_Mark [in|out|in out] => Annotation_List
Annotation_List ::= ( Annotation_Item {, Annotation_Item} )
Annotation_Item ::= object_name | access_subtype_mark |
NULL | ACCESS subtype_mark | OTHERS [IN packagename] | GENERIC formal_parameter_name
The names in these items resolve with the same visibility as other aspect expressions (that usually is the end of the visible part). The names must resolve without context.
[Editor's note: We need the keyword GENERIC here, so that we can tell the difference between references to the initialization and the referenced data for formal pool-specific access types in annotations. Both use the access type name. An alternative would be to add a keyword to the access_subtype_mark case instead, but nothing that isn't ambiguous seems appropriate. My best idea was access_subtype_mark.ALL .]
Aspect_Mark in out => Annotation_List is semantically equivalent to Aspect_Mark in => Annotation_List, Aspect_Mark out => Annotation_List.
AARM Discussion: All of the rules are defined in terms of "Aspect_Mark in" and "Aspect_Mark out". The rules are applied twice (once for "in" and once for "out") to "Aspect_Mark in out".
Aspects Global, Global'Class, and Global'Access are defined.
[End semi-fomal description. From here to the end is intended to be actual wording.]
Static Semantics
An annotation is defined by an Annotation_List.
[Editor's note: This is probably overly broad, but it was the meaning that I used throughout the wording, and this is the best way to fix that without rewriting all of the wording.]
A read or write of an object Obj is covered by an annotation in an Annotation_List if:
* Obj statically denotes a part of an object named in the Annotation_List;
* The annotation item OTHERS without a package name occurs in the list;
* The annotation item OTHERS with a package name P occurs in the list, and Obj denotes part of an object declared in P, or Obj denotes a part of an object produced by a dereference of an object of a pool-specific access type whose pool is declared in P;
* Obj denotes a part of an object produced by a dereference of an object with designated type T, and the type D given in an ACCESS D annotation item covers T; or
* Obj denotes a part of an object produced by a dereference of an object of a pool-specific access type named in the Annotation_List.
AARM Ramification: OTHERS by itself allows anything to be read or written.
AARM Discussion: ACCESS D represents reading/writing of any aliased or tagged object (including those allocated from pools) with a type covered by the type D.
"Statically denotes" does not include dereferences, so the first rule only applies to statically declared objects.
An annotation defined by an Annotation_List A1 is compatible with another such annotation A2 if:
* A1 contains NULL; or
* A2 contains the annotation item OTHERS without a package name; or
* All of the following are true: -- Each object_name in A1 is covered by an annotation item in A2 or is
an object that would not need to be included in A1 if it was explicitly referenced within the entity defining A1;
AARM Reason: The latter part means that local objects in a subprogram S do not need to be included its annotation when they are included in the annotation for a nested subprogram of S that S calls.
-- Each formal_parameter_name item in A1 is found in A2; -- Each access_subtype_mark item in A1 is found in A2 or, if the
the subtype_mark denotes a pool-specific access type, an OTHERS annotation item in A2 naming the package P in which the pool of the access type is declared; and
-- For each OTHERS annotation item with a package name P, there is
an OTHERS annotation item in A2 that statically denotes P.
AARM Ramification: This definition is not symmetrical; A2 may allow more object access than A1 allows (such as having an annotation of (others)).
A type T is compatible with an annotation A of an aspect if:
* T is a generic formal type, and A contains the *formal_parameter_*name of the formal type; or
* The annotation for the same aspect of T is compatible with A.
The result of a union of annotation A1 with annotation A2 is:
* if A1 contains NULL, A2;
* if A2 contains NULL, A1;
* if either A1 or A2 contains an OTHERS annotation without a package name, an annotation with a single item of OTHERS without a package name;
* Otherwise, an annotation with all of the Annotation_Items of A1 and A2 with any duplicates removed.
AARM Ramification: This definition is symmetrical; the order of the operands does not matter.
Unless otherwise specified (either explicitly or defined by this International Standard), the annotation for each defined aspect is (others).
AARM Ramification: (others) allows all global references, so it is completely compatible with earlier versions of Ada.
An inherited subprogram (see 3.4) inherits the annotations of the primitive subprogram of the parent or progenitor type. Redundant[The annotations can be changed on an overriding subprogram, with some restrictions.]
When determining the Global in annotations of entities declared in an instantiation of a generic G, each formal_parameter_name item F of every Global in annotation A of any entities declared in the instance that references a formal parameter of G is removed from A and:
* if F is a formal type, the result is the union of A and the Global in annotation of the actual type;
* if F is a formal subprogram, the result is the union of A and the Global in annotation of the actual subprogram;
* if F is a formal IN OUT parameter, the *object_*name of the actual parameter is added to A if that object_name would need to be included in a Global in annotation for the enclosing entity when it is read at the point of the instance, Redundant[and nothing is added otherwise].
Analogous rules apply to a Global out annotation (replacing "Global in" by "Global out" and "read" by "written" everywhere).
AARM Discussion: At the point of an instance, all of the references to the formal parameters are replaced by the annotations of the actual. This does not require re-analyzing the generic.
Legality Rules
An annotation_list can be given if and only if the aspect is Global, Global'Class, or Global'Access.
The aspect Global shall be given only on subprograms, generic subprograms, types, packages, and generic packages.
The aspect Global'Access shall be given only on access-to-subprogram types.
The aspect Global'Class shall be given only on primitive subprograms of a tagged type.
The Annotation_Item NULL shall appear alone in an Annotation_List.
An object_name given in an Annotation_List shall statically denote some object.
An access_subtype_mark given in an Annotation_List shall denote a pool-specific access type.
A formal_parameter_name given in an Annotation_List shall statically denote some generic formal parameter of an enclosing generic unit; the formal parameter shall be a formal type, a formal subprogram, or a formal IN OUT object.
If a subprogram or generic subprogram contains a Global in annotation, then:
* Every object that is read by the subprogram body shall either be accessible from the subprogram call, be a constant object of an elementary type, or be covered by the Global in annotation.
* The subprogram corresponding to each dispatching call in the subprogram body which has a dynamically tagged controlling operand shall have a compatible Global'Class in annotation; the access-to-subprogram type for each call of a dereference of an access value shall have a compatible Global'Access in annotation; the formal_parameter_name for each call of a formal subprogram is present in the annotation; and the subprogram corresponding to every other call in the subprogram body shall have a compatible Global in annotation.
* The type of every stand-alone object declared by the subprogram shall have a compatible Global in annotation.
* Every nested package and package instantiation declared by the subprogram shall have a compatible Global in annotation.
* The type of each assignment_statement in the subprogram body shall be compatible with the annotation. In addition, if the target of the assignment_statement is a dereference of some access type A, the Allocate and Deallocation routines associated with the storage pool of type A in the subprogram body shall have a compatible Global in annotation.
AARM Reason: Allocate and Deallocate can be called here if the implementation chooses; we have to assume the worst.
* The Allocate and Deallocate routines associated with the storage pool for the type of each allocator in the subprogram body shall have compatible Global in annotations, and the type of the allocated object shall have a compatible Global in annotation.
AARM Reason: Again, Deallocate can be called here if the implementation chooses; we have to assume the worst.
* For each attribute A'Storage_Size in the subprogram body where A is an access type, the Storage_Size routine associated with the storage pool of A shall have a compatible Global in annotation.
* If the subprogram contains a call on an instance of Unchecked_Conversion with a pool-specific access type A as the target type, the subprogram is illegal if the type A is named as an access_subtype_mark annotation item.
AARM Reason: We assume that objects of type A can only designate objects in the pool of A. The only way to violate this is to use Unchecked_Conversion from a general access type value; if such a conversion exists, we require the subprogram to be annotated as if A is a general access type.
AARM Ramification: Local objects, elementary constant objects (declared anywhere) and the parameters of the call do not need to appear in a Global in annotation. Note that this is referring to constant objects, not just constant views of an object.
A write of a dereference of an object P reads the object P (and writes the designated object).
The prefix of a protected function call is considered to be read; the prefix of a protected procedure or entry call is considered to be both read and written. The prefix of a task entry is considered to be read. These rules follow from the requirements in 9.5 on whether or not the prefix of a protected subprogram call or an entry call can be a constant; we don't want to be logically writing constants. End AARM Ramification.
AARM Discussion: We don't need a rule for Deallocate calls in Unchecked_Deallocation, as it is a call and does not have annotations defined. Thus the above rule will always fail and thus we don't care about the annotations on Deallocate. End AARM Discussion.
Analogous rules apply to a Global out annotation (replacing "in" by "out" and "read" by "written" everywhere).
[Editor's note: I don't want to duplicate the rules, they're complex enough as it is.]
For an attribute P'Access of access-to-subprogram type S that has a Global'Access in annotation, subprogram P shall have a compatible Global in annotation. Similarly, for a type S that has a Global'Access out annotation, subprogram P shall have a compatible Global out annotation.
[Editor's note: One could argue that this belongs in 3.10.2; I put it here to keep all of the relevant rules together.]
Redundant[Global'Class annotations provide annotations for dispatching calls.] The Global in annotation of a subprogram shall be compatible with the Global'Class in annotation of the subprogram; similarly Global out annotation of a subprogram shall be compatible with the Global'Class in annotation of the subprogram.
AARM Ramification: The Global'Class annotations have to allow the same or more than the Global annotations, as they apply to all overriding subprograms as well.
For each primitive subprogram P of a tagged type that overrides another primitive subprogram PP of the type:
* If PP has a Global'Class in annotation, the annotation shall be compatible with the Global'Class in annotation for P. The Global in annotation for P shall be compatible with the Global'Class in annotation for PP.
* If PP has a Global'Class out annotation, the annotation shall be compatible with the Global'Class out annotation for P. The Global out annotation for P shall be compatible with the Global'Class out annotation for PP.
If a type includes a Global in annotation:
* If the full type is composite, the type of each component shall be compatible with the annotation.
* If the full type is controlled, the associated Initialize and Finalize routines shall have compatible Global in annotations.
* If the full type is controlled and not limited, the associated Adjust routine shall have a compatible Global in annotation.
* If the full type is composite, for each default expression E for a component of the type:
* every object that is read by E shall be a constant object of an elementary type, or be covered by the Global in annotation; and
* the subprogram corresponding to each dispatching call in E which has a dynamically tagged controlling operand shall have a compatible Global'Class in annotation; the access-to-subprogram type for each call in E of a dereference of an access value shall have a compatible Global'Access in annotation; the formal_parameter_name for each call of a formal subprogram in E is present in the annotation; the subprogram corresponding to every other call in E shall have a compatible Global in annotation; and
* the Allocate routine associated with the storage pool for the type of each allocator in E shall have a compatible Global in annotation.
* The Allocate and Deallocate routines associated with the storage pool for the type of each allocator in E shall have compatible Global in annotations, and the type of the allocated object shall have a compatible Global in annotation.
* For each attribute A'Storage_Size in E where A is an access type, the Storage_Size routine associated with the storage pool of A shall have a compatible Global in annotation.
* If the full type is a task type, the rules for a subprogram body (given previously) shall be applied to the task body and the Global in annotation.
[We do not need to worry about assignment, stand-alone objects, and instances here, none of those are possible inside of types, other than task bodies, which we handle by requiring the rules of a subprogram body to be checked.]
AARM Note: Adjust really doesn't belong here, but it seems to be overkill to have a special kind of annotation just for it (and composition means that trying to define it directly would be a mess - composition happens automatically for the above rules). In practice, Adjust and Finalize are usually very similar in design, and are likely to depend on the same set of globals, so this isn't much of a limitation.
Analogous rules apply to a Global out annotation (replacing "in" by "out" and "read" by "written" everywhere).
If a package or generic package includes a Global in annotation:
* For each expression or call E in every declarative_item (but not including those in nested units) and the sequence of statements of the package body:
* every object that is read by E shall be declared in the package, a constant object of an elementary type, or be covered by the Global in annotation; and
* the subprogram corresponding to each dispatching call in E which has a dynamically tagged controlling operand shall have a compatible Global'Class in annotation; the access-to-subprogram type for each call in E of a dereference of an access value shall have a compatible Global'Access in annotation; the formal_parameter_name for each call of a formal subprogram is present in the annotation; the subprogram corresponding to every other call in E shall have a compatible Global in annotation; and
* the Allocate routine associated with the storage pool for the type of each allocator in E shall have a compatible Global in annotation.
* The Allocate and Deallocate routines associated with the storage pool for the type of each allocator in E shall have compatible Global in annotations, and the type of the allocated object shall have a compatible Global in annotation.
* For each attribute A'Storage_Size in E where A is an access type, the Storage_Size routine associated with the storage pool of A shall have a compatible Global in annotation.
* The type of every stand-alone object declared by the package shall have a compatible Global in annotation.
* Every nested package and package instantiation declared by the package shall have a compatible Global in annotation.
* The type of each assignment_statement in the sequence_of_statements of the package body shall be compatible with the annotation. In addition, if the target of the assignment_statement is a dereference of some access type A, the Allocate and Deallocation routines associated with the storage pool of type A in the subprogram body shall have a compatible Global in annotation.
Analogous rules apply to a Global out annotation (replacing "in" by "out" and "read" by "written" everywhere).
** Wording TBD:
I hate the duplication of rules here. I tried and tried to find some way to eliminate the duplication for expressions and calls (for which most of the rules apply). But I continually got stuck by the fact that there are essentially 3 parameters: the expression E; the accessibility/locality of objects to exclude (that is, the definition of what is local is different for subprograms [we need to include the parameters], packages [we need to exclude anything outside of the package, even though at the same accessibility level, as packages are invisible to accessibility], and types [locals only for tasks, and nothing special needed otherwise]; and the kind of annotation (either "in" or "out"). It's just too much to do in any understandable way. And I couldn't find a way to factor out the accessibility without getting overlapping rules. Maybe someone else has a better idea.
** End Wording TBD.
[Generic rules; these apply to the entire Legality Rules section]
In addition to the places where Legality Rules normally apply, these rules also apply in the private part of an instance of a generic unit.
For the purposes of enforcing these rules in a generic body, the Global annotations on the storage pool operations for formal access types are assumed to be (others). The Global annotations on generic formal elementary types are assumed to be (null).
[This last paragraph is not talking about inside of instances; rechecking is done there with the actual annotations. This is the assume-the-worst rule needed in generic bodies. We can assume the (null) for formal elementary types because no elementary type can have a "significant" default initialization; and the actual has to be known to be elementary. Note that an elementary type could have some other annotations that are explicitly specified; those might be ignored inside of the generic. Other annotations are always assumed to be (others); note that we provide another way to annotate formal entities and those are recommended in most cases.]
Implementation Permissions
An implementation is permitted to omit a call on a subprogram whose Global out annotation is (null) and the results are not needed after the call. In addition, the implementation may omit the call on such a subprogram and simply reuse the results produced by an earlier call on the same subprogram provided: * No globals that are indicated as read by the Global in annotation for the
subprogram are modified between the earlier call and the omitted call;
* None of the parameters are of a limited type; * The addresses and values of all by-reference actual parameters, the values
of all by-copy-in actual parameters, and the values of all object accessible via the values of any access parameters, are the same as they were at the earlier call.
Redunant[This permission applies even if the subprogram produces other side-effects when called.]
AARM Discussion: This is intended to be the same rules as applies to calls on subprograms defined in declared Pure packages (see 10.2.1). Note that we don't need to talk about access values embedded in the parameter objects (as we have to for Pure), or about objects accessed from parameters of named access types, as those have to be covered by the Global annotations.
AARM Ramification: The part about indicating that no globals read are modified via Global in annotations is trivially true for Global in => (null). This makes this rule easier to use than the corresponding Pure rule.
The part about side-effects is barely necessary. The only possible side effects from a call with Global out => (null) would be through machine code insertions modifying objects, imported subprograms with untruthful annotations, Address_to_Access_Conversions, and similar features. The compiler may omit a call to such a subprogram even if such side effects exist; it is allowed to presume the annotations are accurate, even though this cannot be 100% certain.
---
[Now define the default annotations. Above we said that all entities default to having an annotation of (others); here we're going to say otherwise for particular cases where we can do better without introducing compatibility problems.]
Add to 3.5:
Unless otherwise specified, elementary types that do not have a partial view have annotations (see 13.3.4) of Global in out => (null).
AARM Ramification: If the elementary type does have a partial view, the type has annotations of Global in => (others), Global out => (others)); this is the default for all entities and is necessary to avoid breaking privacy. Annotations are part of the contract of the type, and should be carefully thought out to avoid problems with future maintenance.
Add to 3.6:
Unless otherwise specified, array types that do not have a partial view have Global in and out annotations (see 13.3.4) that are copies of those of the component type.
AARM Ramification: If the array type does have a partial view, the type has annotations of Global in => (others), Global out => (others)); this is the default for all entities and is necessary to avoid breaking privacy. Annotations are part of the contract of the type, and should be carefully thought out to avoid problems with future maintenance.
AARM Discussion: Note that there is no such rule for record or other composite types. The annotations needed for them are complex in general, and leaving them out of the source code is not going to help the human reader. [Editor's note: It is also fairly rare that they would be generated; most record types in well-designed programs do have partial views, so it is not a big hardship to write them by hand in the rare case where that is not the case.]
Add to 4.5:
Unless otherwise specified, the predefined operators of the language that have all operands of an elementary type all have implied annotations (see 13.3.4) of Global in out => (null).
Add after 4.5.2:
The predefined equality and ordering operators for discrete array types have implied annotations (see 13.3.4) of Global in out => (null).
AARM Ramification: The global rule means that equality and ordering operators for elementary types also have such annotations. Composition of equality for composite types means that they cannot have implied null annotations; that would be seriously incompatible. User-defined equality operators can have annotations, of course.
[Editor's note: We could use a rule more like the one for array components, inheriting the annotations from the "=" for the component type, if there is no partial view for the type. I didn't do that as the dependence of a partial view is a bit weird. Trying to come up with a rule for record types would be annoying; it would have to include the union of the "=" for all of the component types. Dispatching "=" would still have to use (others) so that future extensions would not be restricted.]
Add after 4.5.3:
If C is an elementary type, the predefined concatenation operators have implied annotations (see 13.3.4) of Global in out => (null).
[We could go further, but it gets messy, as any controlled component may drag Adjustment into the equation.]
Add after A(2)
Static Semantics
Each subprogram that is declared pure or is declared in a language-defined package or generic package that is declared pure has implied annotations (see 13.3.4) of Global in out => (null) unless the subprogram has one or more parameters of an access type or the annotations are specified elsewhere in this International Standard.
AARM Compatibility Note: This could be incompatible if a composite object passed as a parameter to such a subprogram has an access component. This does not seem likely for the language defined Pure packages.
[Editor's note: I'm not sure the exception is actually needed, but I didn't check.
Here the list of declared Pure packages as of this writing; I don't intend to put the list into the AARM as it would require constant maintenance. I'm ignoring Wide_ and Wide_Wide_ versions of packages for this list, as well as bounded and unbounded string versions.
Ada Ada.Assertions Ada.Characters Ada.Characters.Handling Ada.Characters.Latin_1 Ada.Characters.Conversions Ada.Containers -- No subprograms Ada.Containers.Generic_Array_Sort Ada.Containers.Generic_Constrained_Array_Sort Ada.Containers.Generic_Sort Ada.Decimal Ada.Dispatching Ada.IO_Exceptions -- No subprograms Ada.Numerics Ada.Numerics.Generic_Complex_Types Ada.Numerics.Generic_Complex_Elementary_Functions Ada.Numerics.Generic_Elementary_Functions Ada.Numerics.Generic_Real_Arrays Ada.Numerics.Generic_Complex_Arrays Ada.Streams Ada.Strings Ada.Strings.Equal_Case_Insensitive Ada.Strings.Hash Ada.Strings.Hash_Case_Insensitive Ada.Strings.Less_Case_Insensitive Ada.Strings.Maps Ada.Strings.Maps.Constants Ada.Strings.UTF_encoding Ada.Unchecked_Conversion Interfaces Interfaces.C Interfaces.Fortran Standard -- covered by the rules for predefined operators. System System.Storage_Elements
Containers are discussed below; I'm assuming that they will end up with explicit annotations.
I suspect that we need to give explicit annotations for the generic sorts, as the annotations of element types or the formal subprograms come into play for these, and we don't want to restrict them.
We probably also want to exclude the generic real and complex array packages; adding these annotations would prevent sparse matrix representations. I don't think we want to go that far (although sparse matrixes would be hard to implement within the restrictions of Pure, so maybe it doesn't matter).
End really long Editor's note. Probably should move some of this to !discussion after we make decisions.]
Replace to G.1.1(3) with:
type Complex is record Re, Im : Real'Base; end record with Global in => (null), Global out => (null);
[Editor's note: This is the only visible record type in the standard that I know of. We may want some annotation for many of the private types as well; that needs to be done on a case-by-case basis.]
[Editor's note: Annotations on the containers were assigned to Bob Duff. I'm providing suggested annotations for part of Bounded_Vectors in order to test that the generic mechanisms work.
Notes: We have to use the others in Vectors on all of the cursor forms because of the dereference of an access-to-vector type defined in this package (cursors include a reference to their associated container).
The annotations on the unbounded form of Vectors would be the same except that OTHERS IN Vectors would be added to any that could allocate/deallocate elements in order to reflect the allocated memory (from a presumably private but library-level access type).]
A.18.17 Bounded Vectors
generic type Index_Type is range <>; type Element_Type is private; with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Bounded_Vectors is pragma Preelaborate(Bounded_Vectors); pragma Remote_Types(Bounded_Vectors);
subtype Extended_Index is Index_Type'Base range Index_Type'First-1 .. Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; No_Index : constant Extended_Index := Extended_Index'First;
type Vector (Capacity : Count_Type) is tagged private with Global in out => (generic Element_Type); pragma Preelaborable_Initialization(Vector); -- We're assuming an implementation something like: -- type Vector (Capacity : Count_Type) is tagged record -- Length : Count_Type; -- Data : array (1 .. Capacity) of Element_Type; -- end record;
type Cursor is private with Global in out => (generic Index_Type); pragma Preelaborable_Initialization(Cursor); -- We're assuming an implementation like: -- type Cursor is -- Vect : access Vector; -- Index : Extended_Index; -- end record;
Empty_Vector : constant Vector; No_Element : constant Cursor; function "=" (Left, Right : Vector) return Boolean with Global in out => (generic Element_Type, generic Ada.Containers.Bounded_Vectors."=");
function To_Vector (Length : Count_Type) return Vector with Global in out => (generic Element_Type); -- Every operation that needs to create a Vector object needs to -- include the annotations of the Vector object.
function To_Vector (New_Item : Element_Type; Length : Count_Type) return Vector with Global in out => (generic Element_Type);
function "&" (Left, Right : Vector) return Vector with Global in out => (generic Element_Type);
function "&" (Left : Vector; Right : Element_Type) return Vector with Global in out => (generic Element_Type);
function "&" (Left : Element_Type; Right : Vector) return Vector with Global in out => (generic Element_Type);
function "&" (Left, Right : Element_Type) return Vector with Global in out => (generic Element_Type);
function Capacity (Container : Vector) return Count_Type with Global in out => (null);
procedure Reserve_Capacity (Container : in out Vector; Capacity : in Count_Type) with Global in out => (null); -- This would be very different for other forms, where this does -- something.
function Length (Container : Vector) return Count_Type with Global in out => (null);
procedure Set_Length (Container : in out Vector; Length : in Count_Type) with Global in out => (generic Element_Type); -- We need to allow writing empty elements, if the implementation -- does something explicit for them. We have to allow Adjust, so -- we also need to include the reading portion.
function Is_Empty (Container : Vector) return Boolean with Global in out => (null);
procedure Clear (Container : in out Vector) with Global in out => (null); -- This just changes the length.
function To_Cursor (Container : Vector; Index : Extended_Index) return Cursor with Global in out => (null); -- No dereferences here.
function To_Index (Position : Cursor) return Extended_Index; Global in out => (null); -- No dereferences here.
function Element (Container : Vector; Index : Index_Type) return Element_Type with Global in out => (generic Element_Type); -- Creates an element.
function Element (Position : Cursor) return Element_Type with Global in => (access Vector, generic Element_Type), Global out => (generic Element_Type); -- The dereference of the container can touch any Vector object. -- This will prevent many optimizations. -- I knew I hated this implicit container semantics, I just -- couldn't explain why. Note that the previous routine has -- much stronger annotations. Apparently, tools will need to -- be container-aware to have any chance. Yuck.
procedure Replace_Element (Container : in out Vector; Index : in Index_Type; New_Item : in Element_Type) with Global in out => (generic Element_Type); -- Assigns an element; the type's Global annotations are also -- used for assignment.
procedure Replace_Element (Container : in out Vector; Position : in Cursor; New_item : in Element_Type) with Global in => (access Vector, generic Element_Type), Global out => (generic Element_Type); -- The access read is to access the cursor; it has to be -- the same as the Container item or we get an exception, -- but that is beyond the power of these annotations.
...
!discussion
The global in and global out annotations are intended to be descriptive. That is, the annotations describe the behavior of the subprogram body, initialization/finalization of a type, or elaboration of a package. As such, these annotations are checked. There is no benefit to be gained from lying about side-effects; such incorrect information could easily lead to incorrect code being generated (if the compiler uses the annotations). Moreover, if it is impractical to specify the correct annotations, it makes sense to specify none at all.
All of the global in and global out annotations proposed can be statically checked. It is possible to imagine annotations that cannot be statically checked, but these are assumptions as opposed to descriptive. Assumptions are a different set of annotations.
Note that it is possible to lie about the use of globals of subprograms and other entities that are imported. This is of course impossible to check, but thankfully is covered by B.1(38.1/2). Incorrect annotations on imported subprograms could cause a program to be erroneous.
---
The keywords in the syntax are necessary in order that the special syntax of this list can be recognized immediately. Otherwise, a massive amount of lookahead is needed to parse this (as the list would start the same way as the expression used for more typical aspects). We take advantage of the fact that Ada already has "in" and "out" keywords to make this syntax distinctive but still sensible.
---
It might make the most sense to define these in Annex H (High-Integrity Systems), rather than in Section 13. The most important thing is to define the syntax so that implementations can implement it and the checking (even if they are not doing semantic analysis now). The information is valuable to have in programs for future analysis when improved tools are available. The legality rules ensure that the information is accurate.
---
Annotations are defined in terms of "reading" and "writing" of objects. We use these terms in the same way as the rest of the standard; in particular, in the definitions of the semantics for Atomic objects and pragma Reviewable.
---
We have three kinds of global annotations, one for almost everything (Global), and two for special cases: Global'Access for calls through access-to-subprogram types, and Global'Class for dispatching calls.
Note that we need Global'Access to be a separate annotation as an access-to-subprogram type has both annotations (and we need to be able to talk about it for generics, as well as needed to support the unlikely possibility of it having a partial view).
Annotations are defined as aspects, and thus we are using the rules for aspects to simplify this description: there is only one per type (they are not view-specific) [although they can be given on private types, they then cannot be given on the full type];
Global annotations can be given on private types; if so, they are enforced on the full type as well.
---
The definition of preelaborable has legality rules depending on a runtime concept (elaboration). We tried to avoid that mistake with this set of rules.
That requires making composition of annotations explicit. The definition of the Global annotations for types requires this; the annotations of all of the components and all of the default expressions have to be compatible with the type's annotation. Once we have this, applying the rules just requires talking about the type of stand-alone objects and of assignment_statements; they include the annotations of any components by definition.
---
The rules are complicated by the need to include all implicit calls. That is done by folding Initialize/Finalize/Adjust into Global (along with default initialization), and explicitly talking about the operations of storage pools.
---
These annotations can be used by the compiler to guide code generation as well as for static analysis. The Implementation Permission provides rules similar to those for Pure subprograms -- it is OK to assume that the annotations are correct, but if the subprogram is called, then the compiler must use the actual side-effects, not any assumed because of annotations.
---
Annotations can explicitly include names of generic formal parameters; the annotations appropriate for the actual parameters are substituted when the generic is instantiated.
We originally tried to use an assume-the-worst rule for generic units, but that essentially requires any subprogram declaring in a generic that uses a formal parameter to be annotated with Global in => (others). That would totally prevent useful annotations on generic units, which is a complete nonstarter for obvious reasons.
Another option considered was to include the annotations as part of the generic contract. That would require some new matching rules, but otherwise is fairly simple. But it should be obvious that that does not work well for general-purpose generic units. For instance, consider the bounded Vector container. In order to be able to have the desired (null), (null) annotations on most routines, we would have to annotate the Element_Type with (null), (null) annotations. But that would prevent instantiating the container with many real types (any that include parts with Initialize/Adjusts that allocate memory, for instance). Not only is that incompatible, it also reduces the utility of the containers.
Luckily, annotations can be combined with the normal set operations. Thus, if we create a way to refer to the annotations of formal parameters without actually knowing what they are, we can then use the real annotations of the actual types when the generic is instantiated. This neatly solves the problem by making the annotations change as needed. For instance, when the bounded container is instantiated with Integer, all of the annotations will become (null), (null); but if the actual type has default annotations of (others), (others) all of the annotations will reflect that as well.
[I'm so smart to have figured this out myself. ;-) Just wish I had done so the first time. Editor.]
Note that we only provide generic annotations for formal entities that have interesting annotations. We don't provide annotations for in formal parameters, as they are copies of the actual made at the point of the instance. As such, they have no effect on the annotations of items declared in the generic (of course, the evaluation of the actuals could require them to be included in an annotation for a subprogram or package surrounding the instance).
Similarly, we don't provide annotations for formal packages, as the actuals for those are already elaborated instances. As such, their annotations will never be needed in the generic unit (they're only used at the point of the instance).
---
We allow specifying the name of a pool-specific access type as an Annotation_Item. This provides a convinient way to cover all possible target objects without discussing the pool. Note that conversions from other access types to a pool-specific type are not allowed (other than via Unchecked_Conversion, which we disallow explicitly). That means we can treat the pool as local to the package that declares the access type, even if the actual pool is allocated somewhere else. This allows using OTHERS IN <package_name> for types that are hidden from clients.
We do have to treat such a pool as a global object, even though in many cases objects allocated from such hidden access types are not shared and could be considered part of other objects. Since we are using static checked, properties that can only be verified dynamically effectively require "assume-the-worst" rules. See the example of February 1, 2010 found in the !appendix.
For all access types, we provide the ACCESS T annotation item. This item specifies any object that could be allocated for a general access type designating T: any aliased object of a type covered by T (including those allocated from any pool), and, if T is tagged, any object of a type covered by T. (Recall that 'Access can always be used on tagged type parameters, so they are effectively aliased for this purpose.)
Still, if the name of a designated type is not visible, the only annotation available is (OTHERS) (which covers everything).
An alternative approach that was considered would be to wrap up the entire set of items in Global in/out annotations for each access type (that would be disjoint with access-to-subprograms use for the same thing). That would include all of the Global annotations for the subprograms of the storage pool, an annotation for the storage pool object, and ACCESS designated_subtype_mark for general access objects. That doesn't seem to help anything for types that are hidden, thus we did not use that alternative.
!example
Following is a non-generic example that illustrates how these annotations work on a controlled type. There are some embedded comments that explain some details of the annotations.
with Ada.Finalization; package TestV02A is
type JSON_Data_Type is (JSON_NULL, JSON_BOOLEAN, JSON_NUMBER, JSON_STRING); -- As this is an elementary type, we don't need any annotations; -- they will default to Global in => null, Global out => null.
type Holder is tagged private with Global in => (TC_Count), Global out => (TC_Count, TC_Passed); -- Globals used by the default initialization/adjustment/finalization of -- the type.
Null_Holder : constant Holder;
Boolean_Holder : constant Holder;
String_Holder : constant Holder;
function Check_Holder (Container : in Holder; Kind : in JSON_Data_Type) return Boolean with Global in out => (null);
TC_Passed : Boolean := True;
TC_Final_Count : Natural := 0;
private
type Holder is new Ada.Finalization.Controlled with record Type_Kind : JSON_Data_Type := JSON_Null; end record; -- Since Global is an aspect and it was specified for the private type, -- we don't repeat it here. Aspects are the same for all views. subtype My_Holder is Holder;
procedure Initialize (Container : in out Holder) with Global in => (null), Global out => (TC_Passed);
procedure Adjust (Container : in out Holder) with Global in => (null), Global out => (TC_Passed);
procedure Finalize (Container : in out Holder) with Global in => (TC_Count), Global out => (TC_Count);
-- Neither Adjust nor Initialize should be called on the following: -- (Note: Program_Error probably will be raised here if the test fails.)
Null_Holder : constant Holder := (Ada.Finalization.Controlled with Type_Kind => JSON_NULL);
Boolean_Holder : constant Holder := Holder'(Ada.Finalization.Controlled with Type_Kind => JSON_BOOLEAN);
String_Holder : constant Holder := (My_Holder'(Ada.Finalization.Controlled with Type_Kind => JSON_STRING));
end TestV02A;
package body TestV02A is
function Check_Holder (Container : in Holder; Kind : in JSON_Data_Type) return Boolean is -- Only parameters are used, so the annotations are both (null). begin return Container.Type_Kind = Kind; end Check_Holder;
procedure Initialize (Container : in out Holder) is begin TC_Passed := False; end Initialize;
procedure Adjust (Container : in out Holder) is begin TC_Passed := False; end Adjust;
procedure Finalize (Container : in out Holder) is begin TC_Count := TC_Count + 1; end Finalize;
end TestV02A;
with TestV02A; package TestV02B is
function Generator return TestV02a.JSON_Data_Type with
Global in => (others in TestV02B), Global out => (others in TestV02B); -- We have to use others as the global object is not visible -- in the specification.
type Operand is record Kind : TestV02a.JSON_Data_Type := Generator; Obj : TestV02a.Holder; end record with Global in => (others in TestV02B, TestV02A.TC_Count), Global out => (others in TestV02B, TestV02A.TC_Passed, TestV02A.TC_Count); -- This annotation at least has to cover the annotations of the component -- types and anything used by the default expressions. But it can cover -- more: (others) could have been used, or (others in TestV02B, others in TestV02a).
procedure Do_It_Once (O : in Operand) with Global in => (others in TestV02B, TestV02A.TC_Count), Global out => (others in TestV02B, TestV02A.TC_Passed, TestV02A.TC_Count);
function OK return Boolean with Global in => (TestV02A.TC_Passed, TestV02A.TC_Count), Global out => (null);
end TestV02B;
package body TestV02B is
Seed : TestV02a.JSON_Data_Type := TestV02a.JSON_NULL;
function Generator return TestV02a.JSON_Data_Type is
use type TestV02a.JSON_Data_Type;
begin if Seed /= TestV02a.JSON_Data_Type'Last then Seed := TestV02a.JSON_Data_Type'Succ(Seed); else Seed := TestV02a.JSON_Data_Type'First; end if; return Seed; end Generator;
procedure Do_It_Once (O : in Operand) is Copy_of_O : Operand := O; -- The annotations of Operand are required to be covered -- because of this declaration. begin TestV02A.Check_Holder (Copy_of_O, TestV02a.JSON_NULL); end Do_It_Once;
function OK return Boolean is begin return TestV02A.TC_Passed and (TestV02A.TC_Count = 3); end OK;
end TestV02B;
---
Annotations of instances are substituted. For instance, for the following instantiation of Ada.Containers.Bounded_Vectors:
subtype Short_Int is Natural range 0 .. 1000; package Int_Vect is new Ada.Containers.Bounded_Vectors (Short_Int, Integer);
In this case, the annotations for the actual corresponding to "Generic Element_Type" would be "Global in out => (null)", as would the annotations for "=". That means that almost all of the annotations of the types and routines in the instance would become "Global in out => (null)", meaning that the permission to remove extra calls would be active.
On the other hand, if a type like Holder above was used as the element type:
package Holder_Vect is new Ada.Containers.Bounded_Vectors (Short_Int, TestV02a.Holder);
In this case, the annotations for the actual corresponding to "Generic Element_Type" would be "Global in => (TestV02A.TC_Count),
Global out => (TestV02A.TC_Passed, TestV02A.TC_Count)"
and the annotations for "=" would be "Global in out => (others)" (since they were not specified).
Thus the effective annotations for "=" in the Holder_Vect instance would be Global in out => (others), while those for Element (by index) would be Global in => (TestV02A.TC_Count), Global out => (TestV02A.TC_Passed, TestV02A.TC_Count), and those for function Length would still be Global in out => (null).
!ACATS test
!appendix

From: Randy Brukardt
Sent (privately): Wednesday, March 18, 2009  4:30 PM

As I understand it (mainly from an old message of John's about "exposing your
globals"), Global_In is a list of names of globals touched by the body of a
subprogram. It also ought to include two special names: "null" (for explicitly
stating that no globals are harmed by this subprogram :-); and "private" (for
globals that aren't visible at the point of the annotation). By default, all
subprograms have

    Global_In => private,

which says that they touch globals but we aren't going to say which ones.

Presumably, Global_Out are a similar list of globals written by a subprogram.

Do I have it so far?

Now, the problem with the SPARK definition is that it doesn't take into account
things like storage pools and tasks, which we'll have to do.

For the storage pool problem, I think that declaring any collections read would
be sufficient, and that could easily be done by mentioning the name of the
access type in the annotation. (Directly naming the pool has two problems: the
pool may not be visible while the access type is, and secondly, the default pool
does not have a name.)

I'm going to ignore tasks for now (not really relevant to my questions).

I do think that the compiler needs to check that this listing is correct. (And I
think that is fairly easy: any object whose accessibility is outside of that of
the subprogram call "shall be listed" in the Global_In annotation unless the
Global_In annotation includes "private". ["Subprogram call" allows
accessing/modifying the parameters.] That would of course include anything
listed in the Global_In annotation of any called routines. Language-defined
operators other than "=" for tagged types would be defined to have Global_In =>
null.) Having this information incorrect would lead to all kinds of bad
assumptions by the compiler and by the reader. And you can always use Global_In
=> private if you don't want to say - just don't lie.

I note that this gets the effect of the "strict" annotation that I was lobbying
for, but in a way which is much harder to argue with. ("Global_In => null" means
"I don't have a side effect other than as declared in the spec", and the
compiler and reader can depend on that.) We don't get the elaboration benefit (I
would have allowed early calls on strict functions, because so long as their
parameters are frozen, they are safe), but that is no big deal.


But I am wondering about accesses to sub-parts of parameters. My "strict"
definition would have banned that, because it would allow depending on
side-effects. The way I wrote the description above would also ban that, but I
worry that people would be annoyed. This problem comes from my recognition that
the Claw Is_Valid routine is not strict, even though it only depends on reading
its parameter. For example:

     type A_Window is private;

     function Is_Valid (A : A_Window) return Boolean
     when Global_In => ???;

  private

     type Data is record
        Valid : Boolean := False;
        Handle : HWnd := Null_HWnd;
        ...
     end record;
     type Data_Access is access all Data;

     type A_Window is record
         My_Data : Data_Access;
         ...
     end record;

The problem here is that the user of the GUI application can manually close a
window, at which point Valid gets set to False and the Handle gets set to
Null_HWnd (among other things, of course).

Is_Valid only reads its parameter, but the portion that is pointed at can be
modified asynchronously by another task. So it would be wrong for an analyzer to
depend on the value of Is_Valid not changing. (This is a huge challenge when
programming with Claw.)

So, does this mean that type Data_Access must be included in the Global_In list?
(In this particular case, since the type is defined in the private part, the
Global_In list would have to be "private").

****************************************************************

From: Tucker Taft
Sent (privately): Wednesday, March 18, 2009  5:31 PM

...
> Do I have it so far?

I hadn't thought about it too much in detail yet.  As you know SPARK has
something like this.

The notion of "private" doesn't sound too useful.  I would suggest allowing the
names of packages as well as objects, where the name of a package means some
presumably non-visible "state" in the package (spec or body).  I suspect we
would need to parenthesize the list if there is more than one item, to avoid
creating a syntactic mess, with "null" substituting for the syntactically
illegal "()".

>
> Now, the problem with the SPARK definition is that it doesn't take
> into account things like storage pools and tasks, which we'll have to do.
>
> For the storage pool problem, I think that declaring any collections
> read would be sufficient, and that could easily be done by mentioning
> the name of the access type in the annotation. (Directly naming the
> pool has two
> problems: the pool may not be visible while the access type is, and
> secondly, the default pool does not have a name.)

Yes, an access type would seem reasonable as a stand-in for the collection it
represents.  And a package name would cover any non-visible *pool-specific*
access types declared within it.

If you are going through a non-visible *general* access type, then I think we
would want some notation for that if the access type is private, but the
designated type is not.  E.g. "all aliased T" might be a legal entry in the
list, and perhaps simply "all aliased" if the type is itself non-visible.

Alternatively, it might be appropriate in some cases to identify the particular
pointed-to object referenced/updated, e.g. Global_In => (X.all, Y.T.all),
Global_Out => (X.A, Y.B.all); Saying an entire access collection is affected is
too imprecise for some kinds of analysis.  And if the access type is a general
access type, then you are effectively "killing" all aliased objects of the
designated type (or types covered by it).

> I'm going to ignore tasks for now (not really relevant to my questions).

I don't see tasks as a big special case.  A task has state just like other
objects.  The slightly weird thing is that you can change the state of a task
even though you have it as an "IN" parameter.  Probably one way to think about
it is that every task has its own "collection", and the stack of the task is
allocated out of that collection, and the task object is really just a pointer
to that.  A call on an entry of a task passes an implicit dereference of that
pointer to the accept statement.

> I do think that the compiler needs to check that this listing is correct.
> (And I think that is fairly easy: any object whose accessibility is
> outside of that of the subprogram call "shall be listed" in the
> Global_In annotation unless the Global_In annotation includes "private". ["Subprogram call"
> allows accessing/modifying the parameters.] That would of course
> include anything listed in the Global_In annotation of any called routines.
> Language-defined operators other than "=" for tagged types would be
> defined to have Global_In => null.) Having this information incorrect
> would lead to all kinds of bad assumptions by the compiler and by the
> reader. And you can always use Global_In => private if you don't want to say - just don't lie.

Yes, I would agree with all of this.  But I would also try to define the
semantics so that if you manage to lie (e.g. by referencing imported
subprograms), the world doesn't implode. Instead it is like pragma Pure, the
compiler is allowed to avoid calling a subprogram again if it concludes
everything it takes as input is unchanged, and use the prior results of the
call.  It isn't allowed to assume that if it actually *makes* the call, it will
always get the same answer.

Something similar would be said about Global_Out, which would permit reusing
cached values after a call rather than reloading them from memory if they
supposedly wouldn't be affected by the call, but if you actually go to the
trouble of *reloading* the value from memory, you shouldn't presume this newly
loaded value is identical to the old one, and use the newly reloaded value to,
say, index into an array without rechecking against the bounds.

> I note that this gets the effect of the "strict" annotation that I was
> lobbying for, but in a way which is much harder to argue with.
> ("Global_In => null" means "I don't have a side effect other than as
> declared in the spec", and the compiler and reader can depend on
> that.) We don't get the elaboration benefit (I would have allowed
> early calls on strict functions, because so long as their parameters
> are frozen, they are safe), but that is no big deal.
>
>
> But I am wondering about accesses to sub-parts of parameters. My "strict"
> definition would have banned that, because it would allow depending on
> side-effects.

I don't really understand this last sentence.  I'm not sure what is a "sub-part"
and I'm not sure what you mean about "depending on side-effects."  I think I
understand what you mean in your example below, but I don't understand this
introductory sentence.

> ... The way I wrote the description above would also ban that, but
> I worry that people would be annoyed. This problem comes from my
> recognition that the Claw Is_Valid routine is not strict, even though
> it only depends on reading its parameter. For example:
>
>      type A_Window is private;
>
>      function Is_Valid (A : A_Window) return Boolean
>      when Global_In => ???;
>
>   private
>
>      type Data is record
>         Valid : Boolean := False;
>         Handle : HWnd := Null_HWnd;
>         ...
>      end record;
>      type Data_Access is access all Data;
>
>      type A_Window is record
>          My_Data : Data_Access;
>          ...
>      end record;
>
> The problem here is that the user of the GUI application can manually
> close a window, at which point Valid gets set to False and the Handle
> gets set to Null_HWnd (among other things, of course).
>
> Is_Valid only reads its parameter, but the portion that is pointed at
> can be modified asynchronously by another task. So it would be wrong
> for an analyzer to depend on the value of Is_Valid not changing. (This
> is a huge challenge when programming with Claw.)
>
> So, does this mean that type Data_Access must be included in the
> Global_In list? (In this particular case, since the type is defined in
> the private part, the Global_In list would have to be "private").
>
> Thanks in advance for your answer.

If you read something you get through an access value, then you will need to
account for it somehow, as "blah.all", the name of an access type, the name of a
package, or something like "all aliased [T]".

I think you are also talking about issues that have to multi-threading here.  If
the asynchronous event can happen at "any" time, then I would say you should
really declare the "Valid" field as volatile, in which case we would probably
want some way of stating that the result of a function is volatile and hence
essentially unpredictable.

If the aynchronous update can only happen during to some kind of
potentially-blocking or signaling operation, then it should be handled the
normal way things are handled at potential task signaling/blocking points, where
some appropriate part of the universe might be affected by the actions of other
tasks.

****************************************************************

From: Randy Brukardt
Sent (privately): Wednesday, March 18, 2009  5:59 PM

...
> The notion of "private" doesn't sound too useful.  I would suggest
> allowing the names of packages as well as objects, where the name of a
> package means some presumably non-visible "state" in the package (spec
> or body).  I suspect we would need to parenthesize the list if there
> is more than one item, to avoid creating a syntactic mess, with "null"
> substituting for the syntactically illegal "()".

Well, it surely isn't useful for analysis, but it seems necessary to have a
default that says, yup, we have some side effects and we aren't going to say
which ones. Because we surely can't require this annotation on all subprograms,
but we do have to know what to do if such a subprogram is called from inside of
one that does have an annotation.

If there is a better way to express the default of "anything goes, assume the
worst", I'm happy to see it.

...
> > I do think that the compiler needs to check that this listing is correct.
> > (And I think that is fairly easy: any object whose accessibility is
> > outside of that of the subprogram call "shall be listed" in the
> > Global_In annotation unless the Global_In annotation includes "private".
> > ["Subprogram call" allows accessing/modifying the parameters.] That
> > would of course  include anything listed in the Global_In annotation
> > of any called routines.
> > Language-defined operators other than "=" for tagged types would be
> > defined to have Global_In => null.) Having this information
> > incorrect would lead to all kinds of bad assumptions by the compiler
> > and by the reader. And you can always use Global_In => private if
> > you don't want to say - just don't lie.
>
> Yes, I would agree with all of this.  But I would also try to define
> the semantics so that if you manage to lie (e.g. by referencing
> imported subprograms), the world doesn't implode.
> Instead it is like pragma Pure, the compiler is allowed to avoid
> calling a subprogram again if it concludes everything it takes as
> input is unchanged, and use the prior results of the call.  It isn't
> allowed to assume that if it actually
> *makes* the call, it will always get the same answer.

Well, for static analysis, either you have the truth or the world implodes. :-)
And that's also true for legality rules - if you depend on an incorrect
annotation when enforcing a legality rule (or more accurately not enforcing),
it's pretty much garbage in, garbage out. Probably would want to define that as
a bounded error if at all possible (either you get an error or the code works at
runtime).

But I agree that we pretty much have to leave the Duff door open: lying in
annotations on an imported subprogram can't be banned or detected.

I do agree that uses in optimizations and code selection should follow rules
like you give here.

> Something similar would be said about Global_Out, which would permit
> reusing cached values after a call rather than reloading them from
> memory if they supposedly wouldn't be affected by the call, but if you
> actually go to the trouble of *reloading* the value from memory, you
> shouldn't presume this newly loaded value is identical to the old one,
> and use the newly reloaded value to, say, index into an array without
> rechecking against the bounds.

Right. I'm not personally as interested in Global_Out, at least not right this
minute, but I can see how it would be useful.

...
> > But I am wondering about accesses to sub-parts of parameters. My "strict"
> > definition would have banned that, because it would allow depending
> > on side-effects.
>
> I don't really understand this last sentence.  I'm not sure what is a
> "sub-part" and I'm not sure what you mean about "depending on
> side-effects."  I think I understand what you mean in your example
> below, but I don't understand this introductory sentence.

I mean cases like the example below. In other words, ignore the above if it is
too confusing.

> > ... The way I wrote the description above would also ban that, but I
> > worry that people would be annoyed. This problem comes from my
> > recognition that the Claw Is_Valid routine is not strict, even
> > though it only depends on reading its parameter. For example:
> >
> >      type A_Window is private;
> >
> >      function Is_Valid (A : A_Window) return Boolean
> >      when Global_In => ???;
> >
> >   private
> >
> >      type Data is record
> >         Valid : Boolean := False;
> >         Handle : HWnd := Null_HWnd;
> >         ...
> >      end record;
> >      type Data_Access is access all Data;
> >
> >      type A_Window is record
> >          My_Data : Data_Access;
> >          ...
> >      end record;
> >
> > The problem here is that the user of the GUI application can
> > manually close a window, at which point Valid gets set to False and
> > the Handle gets set to Null_HWnd (among other things, of course).
> >
> > Is_Valid only reads its parameter, but the portion that is pointed
> > at can be modified asynchronously by another task. So it would be
> > wrong for an analyzer to depend on the value of Is_Valid not
> > changing. (This is a huge challenge when programming with Claw.)
> >
> > So, does this mean that type Data_Access must be included in the
> > Global_In list? (In this particular case, since the type is defined
> > in the private part, the Global_In list would have to be "private").
> >
> > Thanks in advance for your answer.
>
> If you read something you get through an access value, then you will
> need to account for it somehow, as "blah.all", the name of an access
> type, the name of a package, or something like "all aliased [T]".

Right. I suspect some people will not like that much (you have even argued wrt
to constants that such accessed parts are logically part of the passed object).
But in this case, they are *not* logically part of the passed object.

> I think you are also talking about issues that have to multi-threading
> here.  If the asynchronous event can happen at "any" time, then I
> would say you should really declare the "Valid" field as volatile, in
> which case we would probably want some way of stating that the result
> of a function is volatile and hence essentially unpredictable.
>
> If the aynchronous update can only happen during to some kind of
> potentially-blocking or signaling operation, then it should be handled
> the normal way things are handled at potential task signaling/blocking
> points, where some appropriate part of the universe might be affected
> by the actions of other tasks.

Claw uses locks so that the state can't change inside of a Claw-defined routine.
If a state change needs to happen, it is delayed until the lock is available,
meaning after the current routine is finished. But we don't lock things that
only read scalar components (and don't have dependencies), because those can't
be in an inconsistent state: the Valid component can only be True or False.

I suppose that they really ought to be declared volatile, but given the nasty
impact on code generation, and that we only care that Valid is not some value
other than True or False (which can't happen with any of the Ada compilers we've
used), we never did that.

In any case, the pool or object has to be identified somehow in Global_In. That
eliminates my concern.

It does seem that a real proposal would be valuable here. If I had it, I could
point to it rather than duplicating a lot of that in AI-144's discussion.

****************************************************************

(Partial) Minutes of the Amendment subcommittee of the ARG conference call of
December 10, 2009

Attendees: Bob Duff, Tucker Taft, Randy Brukardt, Steve Baird, Gary Dismukes, Ed Schonberg

AI05-0186-1/01

Bob says that this is essential if you ever want to do any analysis of programs
without all of the source code available.

Bob comments that the write up talks about function too much, it should say
subprogram more. Tucker notes that this is mainly an issue in !problem. Randy
notes that the motivating case has to do with functions, so it just talks about
that there.

Bob wonders if we should talk about variables rather than constants. He doesn't
want to annotate reads of global constants. Not all constants are really
constants, however. Calling an entry of tasks if side-effect, even if the task
is a constant. He is not sure what the right answer is (we could except
elementary constants from the rules without problems).

Elementary Operators would have null annotations. Randy notes that composition
of equality means that we have to exclude composite operators, as they might
contain user-defined parts (even array "=" has that problem).

Bob wonders about annotations of the existing predefined packages. In an ideal
world, they would all have them, but that is a heck of a lot of work. Bob notes
that most of the pure packages could use global in/out => null. But access
parameters could cause problems, global in => null is stronger than Pure.

We would want all of the pure packages (like Generic_Elementary_Functions) to
have annotations. We'd like that for the containers, too, but they are mostly
preelaborable.

Randy notes that we'll all have to pitch in on this AI if we want to get it done
on time. Bob will investigate how these annotations could be used on the
unbounded vectors packages.

Ed doesn't like the idea too much. He thinks it is going halfway. If you don't
do data flow it is too imperfect.

Others disagree. You have explicitly include side effects of anything that you
call. That is the same as SPARK. No one thinks SPARK is "too imperfect".

Ed suggests that we might want this on task bodies. That could be used to
prevent/declare unsynchronized access. That seems useful.

Randy notes that in'Class and out'Class would be useful for dispatching calls.
We also would like to have this on access-to-subprogram types.

Bob leaves the call at this point.

We start wondering about the elaboration of entities. Calls that occur in
initialization are definitely included.

Steve notes that you need to worry about default initialization. That's at least
in the spec. It's the body that is hidden that is a problem.

What about instantiating a generic? You would like annotations for things that
happen in the body elaboration there.

That means we have to put aspect specs on bodys. Tucker already had an action
item to do that from St. Pete. He doesn't remember that, and asks for the
minutes draft.

Aspect specs need to be somewhere around the "is" - putting them at the very end
makes no sense. Tucker thinks before the "is". Ed thinks after the "is" makes
more sense. The current end is the ';' the end being the "is" makes more sense.
Gary thinks that would read OK.

Initialize procedures also need their side effects included.

Steve wonders about user-defined storage pools, those too ought be included.

Lots more wording to add, especially for implicit calls.

Access_subtype_name really ought to be Access_subtype_mark. For general access,
it would mean everything aliased covered by the designated type, plus the
storage pool. For all access types, also include the side effects of any
allocate/deallocate routines. (What about function Storage_Size?)

Is this privacy-preserving? In that case, a private type would need an
annotation for default initialization and finalization. But you can't really
have one without the other. Well, you could if you don't use the default
initialization. Tucker says that you ought to be responsible for them anyway. So
only a single annotation is needed for a private type.

Steve would like this to preserve the separation of static and dynamic
semantics. That is the intent - he notes that Pure does not do that. That means
the wording shouldn't talk about what happens at elaboration.

****************************************************************

Example of access annotations, February 1, 2010, Randy Brukardt

It is often the case that access types hidden in package bodies allocate objects
that "belong" to particular parameter objects. Verifying this property is
not possible statically; thus access type annotations have to assume that
allocated objects are shared amongst top-level objects.

Following is an example of a type that would be problematic without the
requirement to annotate hidden access types.

private with Ada.Finalization;
package Clones is

    type Clonee is tagged private
       with Global in out => (others in Clones);

    procedure Create (Obj : in out Clonee; Cnt : Natural; Ave : Float) with
       Global in out => (others in Clones);

    function Cnt (Obj : in Clonee) return Natural with
       Global in => (others in Clones), Global out => (null);

    function Ave (Obj : in Clonee) return Natural with
       Global in => (others in Clones), Global out => (null);

    procedure Reset (Obj : in out Clonee; Cnt : Natural; Ave : Float) with
       Global in out => (others in Clones);

private

    type Data_Type is record
        Ref_Cnt : Natural := 0;
        Ave : Float;
        Cnt : Natural;
    end record;
    type Data_Access is access Data;

    type Clonee is new Ada.Finalization.Controlled with record
        Data : Data_Access;
    end record;

    overriding
    procedure Adjust (Obj : in out Clonee) with
       Global in out => (others in Clones);

    overriding
    procedure Finalize (Obj : in out Clonee)
       Global in out => (others in Clones);

end Clones;


package body Clones is

    procedure Create (Obj : in out Clonee; Cnt : Natural; Ave : Float) is
    begin
        Obj.Data := new Data_Type'(Ref_Cnt => 1, Ave => Ave, Cnt => Cnt);
    end Create;

    function Cnt (Obj : in Clonee) return Natural is
    begin
        return Obj.Data.Cnt;
    end Cnt;

    function Ave (Obj : in Clonee) return Natural is
    begin
        return Obj.Data.Ave;
    end Ave;

    procedure Reset (Obj : in out Clonee; Cnt : Natural; Ave : Float) is
    begin
        Obj.Data.Ave := Ave;
        Obj.Data.Cnt := Cnt;
    end Reset;

    procedure Adjust (Obj : in out Clonee) is
    begin
       Obj.Data.Ref_Cnt := Obj.Data.Ref_Cnt + 1;
    end Adjust;

    procedure Finalize (Obj : in out Clonee) is
    begin
       if Obj.Data /= null then
          Obj.Data.Ref_Cnt := Obj.Data.Ref_Cnt - 1;
          if Obj.Data.Ref_Cnt = 0 then
              Free (Obj.Data);
          end if;
       end if;
    end Finalize;

end Clones;

with Clones;
procedure Test is
    A, B : Clones.Clonee;
begin
    Clones.Create (A, 10, 1.5);
    B := A;
    if Clones.Cnt(B) = 10 then ... -- (1)
    Clones.Reset (A, 5, 2.5);
    if Clones.Cnt(B) = 10 then ... -- (2)
end Test;

Clones.Cnt(B) has the value 10 at (1), and 5 at (2). Since Clones.Cnt
has a Global out => (null), it is a candidate for the optimization of
removing the redundant call at (2), most so because the object B
is the same as before. However, it fails the check that the Global in
is not modified, so the optimization cannot be performed.

If we allowed the "hidden" access type to be ignored in the annotations,
this (incorrect) optimization would be allowed. That's no good.

Note that if the Reset operation would have been some call unrelated
to package Clones, the optimization would have been allowed, as the
value of B could not have changed (even though it contains "global" data).

****************************************************************

From: Bob Duff
Sent (privately): Tuesday, February 2, 2010  3:51 PM

> Implementation Permissions
>
> An implementation is permitted to omit a call on a subprogram whose =
> Global out annotation is (null) and the results are not needed after
> the call. In = addition,

Hmm.  I thought our philosophy was that assertions are either checked, or not,
depending on the mode, but do not otherwise affect the semantics.  An
implementation can have a mode where it optimizes based on the assumption that
assertions are true (and perhaps the assumption that they don't have
"interesting" side effects), but we don't define such modes in the language.

Seems to me globals annotations are similar, and we should take a similar
attitude.  That is, globals annotations are there to support assertions, not to
help the optimizer.  (But of course, an implementation can have a mode where
they help the optimizer.)

****************************************************************

From: Randy Brukardt
Sent (privately): Wednesday, February 3, 2010  6:24 PM

Steve Baird wrote:

> Your goal of explicitly defining the static semantics (as opposed to a
> 10.2.1(5)-style cheat) is laudable, but it seems like there are bound
> to be holes even though (or perhaps
> because) the proposed change seems enormous.
>
> Do we deal with the initialization side-effects of an uninitialized
> allocator? Streaming attributes? Finalization of aggregate temps?

Yes (in version /05). The model is that the type of any object that is
declared/created by the syntax of a subprogram body requires that it's
annotation is covered. If the wording is missing for some case, it needs to be
added.

Yes. Streaming attributes are subprograms, and as such have annotations of
Global in out => (others) [because we didn't define them to be something else].
And the normal call rules apply. One could imagine trying to do better, but as
you imply, that would be hard.

I don't know, because I don't know what you mean by an "aggregate temp". Last
night, I thought you meant the logical copy required by the canonical semantics,
and the answer to that is yes (since the annotation of the type of any
assignment has to be compatible, which covers the finalization of that type as
well as the Adjustment; similarly, the finalization of any component types of T
is covered by the annotation for the T, so any component aggregate temporaries
are necessarily covered), but that seems so obvious that perhaps you had
something else in mind (I know how deviously your mind works. :-)

> And an implementation permission such as
>
>     An implementation is permitted to omit a call on a subprogram
>     whose Global out annotation is (null) and the results are not
>     needed after the call.
>
> really raises the stakes here. This means that we can't, for example,
> punt on defining the rules for some constructs. We don't want to allow
> omitting a call to
>
>     procedure P with global out null is
>     begin
>        abort The_Runaway_Task;
>     end P;
> or
>     procedure Q with global out null is
>     begin
>         raise We_Are_Approaching_An_Iceberg;
>     end Q;

Why not? We allow exactly that for pragma Pure, and global out (null) is
*stronger* than pragma Pure. I believe that both of these are legal for a
subprogram in a pragma Pure package, and the rule for Pure packages allows both
of these calls (indeed, *any* procedure call that doesn't have a modifiable
parameter).

[Aside: The second case illustrates the need for exception contracts better than
anything I could ever say, but we've all agreed that those are too complex for
this go-around. They ought to exist and have similar rules to these global
annotations: a possible raise of an exception not handled and not covered by the
contract is illegal.]

> I understand that these annotations are different than Assert pragmas
> because they are statically checked. Nonetheless, I would feel more
> comfortable if these annotations had no language-defined effects on
> dynamic semantics.
>
> If a compiler wants to make use of annotations in performing
> optimizations and is able to perform whatever analysis is needed in
> order to conclude that some transformation is safe, then fine.
> If we do a good job of defining these annotations, the existing
> permissions should suffice and no new permissions should be needed.

I don't buy any of this; I think your world view of these annotations is wrong.

These are *facts* about a subprogram; they're part of the *contract* of the
subprogram. A subprogram which violates its global annotations is wrong, whether
or not the compiler detects it. The compiler detection is just an aid to help
ensure that the program meant what they said. In that sense, it is no different
than "aliased"; the compiler is allowed to assume that an untagged object
without that notation is not going to be designated by an access type, even
though there exist a number of ways to have that effect.

One possible approach to that would be to say that outright:

Erroneous Execution

If a subprogram evaluates, elaborates, or executes an operation or statement
that accesses an entity that is not covered by its Global in annotation, or
modifies an entity that is not covered by its Global out annotation, execution
is erroneous. In particular, execution of a subprogram with a Global out =>
(null) annotation that modifies any non-local entity other than its parameters
is erroneous.

Since an erroneous subprogram can do anything at all, doing nothing at all would
be a valid implementation.

I don't particularly want to go this way, because we already have a more
restricted permission than that in the Ada language, and it makes sense to copy
it. And wording this normatively is likely to engender more controversy than is
worthwhile. But the above is  how I think about Globals annotations (and pragma
Pure, for that matter).

---

It is my opinion that this feature (and by corollary, all of the contract
proposals) is not worthwhile unless the compiler is allowed to rely on the
contracts. The basic problem is, if a tool cannot rely on the contracts unless
it can verify their correctness, you are essentially requiring full-source
analysis only. If you are willing to require that, you don't need *any* language
feature; the entire point is to strengthen the contracts for analysis even
before the body exists. (And that surely includes analysis by the compiler - I
don't see why we should have a double standard for compilers and for other
tools.)

The problem here is that if the compiler isn't allowed to use the contracts,
there is no justification for including the feature in the language. To
oversimplify a bit, there are only 4 reasons to add a feature to Ada:

(1) To improve the readability/expressiveness of the language;
(2) To improve static error detection (legality rules);
(3) To provide additional runtime correctness checking;
(4) To improve the capabilities of the compiler to provide better code.

Analyzing this proposal against these 4 criteria:
(1) Readability is worse, in general, because there is more noise in the
    specifications. Expressiveness is improved, but it mainly matters in corner
    cases. This is a net loss. (This is true for all of the contract schemes,
    IMHO.)
(2) The only static error detection added here is internal to the new feature.
    There is nothing added to the existing language. (This is also true for all
    of the contract schemes.)
(3) There is no runtime checks proposed here. (The other contracts differ on
    this one.)
(4) Yes, the compiler can use the additional information. But that requires
    being able to assume it is accurate, or requires looking in the body. As
    noted above, the reason for this feature is to avoid looking in the body, so
    that is not worth considering. (The other contracts can only be used by the
    compiler if it can prove that there are no side-effects, so this one is a
    "no" unless the Global annotations are available.

The net effect of this analysis is that the only language value to this feature
is from the ability of compilers to use the contracts. If you take that away,
you are taking it away from other contracts as well (that is, the ability to
optimize preconditions is eliminated for all but ones consisting solely of
predefined elementary operators, which will be approximately 0% of real
preconditions on private types). At that point, the only remaining value is the
ability of the compiler to produce warnings - but we don't have language
features about warnings. And the value of the other contracts is also greatly
compromised; they now have no more benefit than just writing some code at the
top of the subprogram (which I've been doing for 30 years of Ada programming),
with the possible exception of full-program analysis tools [and those don't need
the help, they can figure out what they need to know from the source itself].

So my question is, are we doing *contracts* or *assertions*? If we're doing
*assertions*, we don't need this AI and I'm not at all interested in any of the
related AIs [other than the syntax for aspects; it's what Ada should have had in
the first place]. (The benefit isn't much over assertion pragmas to start with;
the problems Pascal ranted about cancel out any benefits). In that case, I
should not waste any of my time on any of those AIs (beyond the basic editorial
issues. If we're doing *contracts*, we need to get this right, and compilers
have to be able to take advantage of the information.

To be continued tomorrow. :-)

****************************************************************

From: Bob Duff
Sent (privately): Tuesday, February 2, 2010  3:51 PM

I'm having trouble understanding this AI, and some others, because AI05-0183-1
is still up in the air. Tuck, would you mind putting that one at the head of
your priority queue?

General comments.

I find it difficult to understand this AI (even ignoring the AI05-0183-1 issue).
I'm not blaming you, Randy -- I think it's just hard.

I think perhaps globals annotations should not apply to nested subprograms.  A
tool (or a human reader) can reasonably be expected to just figure it out.  All
the relevant code is just there.  Yes, in case of subunits, the tool needs to do
an inter-compilation-unit analysis, but I think that's reasonable.

I think it would be useful to have a way to say "The default annotation in this
scope is 'null' instead of the usual 'others'." Or maybe a general way to set
the default (e.g. to 'all variables in this package').

I don't buy the idea that tools that make potentially-false assumptions are
useless.  Suppose a tool assumes X, and proves all kinds of assertions true
based on that.  And suppose X might be false.  Well, we've still got useful info
-- we know that "X implies so-and-so" (or, for the imply-o-phobes, "if X then
so-and-so").  If X is usually true, and can be checked separately (perhaps by
hand), then it's OK.

One X I'm thinking of here is [De]allocate.  I hate to see all kinds of
pessimistic assumptions, that basically ruin any attempt to prove anything about
any subprogram that does 'new' or U_D.  Yeah, the storage pool can have side
effects, but they're usually at a totally different level from the code that
invokes them.

Note that pure-functional languages do not consider "new" to be a side effect.

I'm not sure how we intend to deal with low-level chap-13-ish stuff.
There's a mention of Unchecked_Conversion here, but that's in the same category
as machine-code inserts, address clauses, etc. Seems to me all these things need
to be treated the same, namely it's the programmer's responsibility to ....

> Annotations are provided to describe the use of global objects by
> subprograms.
>
> !problem
>
> We're considering adding many kinds of annotations to Ada (see
> AI05-0145-1 and AI05-0146-1) in order to increase the ability of a
> programmer to specify contracts for types and subprograms. These
> contracts are defined to be checked at runtime, but are intended to be
> potentially checked (at least in part) statically.
>
> However, without knowledge of side-effects of functions used in the

"functions" --> "subprograms".

> annotations, a tool has to assume the worst about any user-defined
> functions.

When I said this at the last phone meeting, Ed pointed out that there's an
alternative: whole-program analysis.  So I suggest adding "(or perform
whole-program analysis)" at the end of the above sentence.  No need to point out
the drawbacks of that.

>...That is, that the result of a function can change even when

"That is" --> "For example".

> called with the same operands. Other assumptions could cause incorrect
> programs to be accepted as correct, and if the assumptions were used
> to omit "proved" annotations, to erroneous execution.  Both of these

"erroneous" --> "incorrect".

> results are unacceptable for a feature intended to improve the
> correctness of programs.
>
> The worst-case  assumptions pretty much prevent any  analysis unless
> the bodies  of  any  user-defined  functions  used in  the
> annotations  are available.

OK, I see...

>... This is bad, as it  prevents analysis of programs as they are
> constructed.   If  the   body   is  not   available,   no  analysis   is
> possible. Moreover, analysis depending on a body require creating
>pseudo  body dependencies  (if the  body is changed,  any analysis
>depending on  that properties of that body would  have to be performed
>again); but the

"that properties" --> "the properties"

> language  does not  allow  these  to be  "real"  body dependencies
> (any recompilation needed has to occur automatically).
>
> Ideally, analysis at the initial compile-time of a unit would be
> possible, as it is important to detect errors as soon as possible.
> More information about function side-effects is needed in the
> specification of subprograms in order to accomplish that goal.
>
> !proposal
>
> Add global in and global out annotations to Ada, for subprograms,
> packages, and types. Add related annotations for dispatching
> subprograms and access-to-subprogram types.
>
> The global annotations for types cover default
> initialization/adjustment/finalization.  The global annotations for
> packages cover operations that occur as part of the elaboration for
> packages.

Hmm...  Are we really sure it's OK to lump all that together.
I can imagine being frustrated when I want to give different 'globals' for init
versus final, e.g.

> !wording
>
> Add a new section:
>
> 13.3.4 Global usage annotation
>
> Semi-formal description: [Editor's note: This part depends heavily on
> the unfinished AI05-0183-1; it's not worth trying to describe these
> rules until that AI is finished.]
>
> Add to the aspect syntax given in AI05-0183-1:
>
>     Aspect_Mark [in|out|in out] => Annotation_List
>
>     Annotation_List ::= ( Annotation_Item {, Annotation_Item} )
>
>     Annotation_Item ::= *object_*name | *access_*subtype_mark |
>                          NULL | ACCESS subtype_mark |
>                          OTHERS [IN *package*name] |
>                          GENERIC *formal_parameter_*name

A "generic formal parameter" is not a "formal parameter".

> The names in these items resolve with the same visibility as other
> aspect expressions (that usually is the end of the visible part). The
> names must resolve without context.
>
> [Editor's note: We need the keyword GENERIC here, so that we can tell
> the difference between references to the initialization and the
> referenced data for formal pool-specific access types in annotations.
> Both use the access type name. An alternative would be to add a
> keyword to the *access_*subtype_mark case instead, but nothing that
> isn't ambiguous seems appropriate. My best idea was
> *access_*subtype_mark.ALL .]
>
> Aspect_Mark in out => Annotation_List is semantically equivalent to
> Aspect_Mark in => Annotation_List, Aspect_Mark out => Annotation_List.
>
> AARM Discussion: All of the rules are defined in terms of "Aspect_Mark in"
> and "Aspect_Mark out". The rules are applied twice (once for "in" and
> once for "out") to "Aspect_Mark in out".
>
> Aspects Global, Global'Class, and Global'Access are defined.
>
> [End semi-fomal description. From here to the end is intended to be
> actual wording.]
>
> Static Semantics
>
> A read or write of an object O is *covered by an annotation* in an

Please, PLEASE don't use "O" as an object name!
"X" or "Obj" or ...

> Annotation_List if:
>     * O statically denotes a part of an object named in the
> Annotation_List;

I'm not sure "statically denotes" is right, here.
Don't you want to include a record component X.Y, for example?

>     * The annotation item OTHERS without a package name occurs in the list;
>     * The annotation item OTHERS with a package name P occurs in the list, and
>       O denotes part of an object declared in P, or O denotes a part of an object
>       produced by a dereference of an object of an pool-specific
> access type whose

"an" --> "a"

>       pool is declared in P;

Including children and nested packages?

>     * O denotes a part of an object produced by a dereference of an object with
>       designated type T, and the type D given in an ACCESS D
>       annotation item covers T; or
>     * O denotes a part of an object produced by a dereference of an object of
>       a pool-specific access type named in the Annotation_List.
>
> AARM Ramification: OTHERS by itself allows anything to be read or written.
>
> AARM Discussion: ACCESS D represents reading/writing of any aliased or
> tagged object (including those allocated from pools) with a type
> covered by the type D.
>
> "Statically denotes" does not include dereferences, so the first rule
> only applies to statically declared objects.

I don't think "statically declared" means anything.

> An annotation A1 is *compatible* with another annotation A2 if:

"An annotation"?  We're only talking about globals annotations...

>     * A1 contains NULL; or
>     * A2 contains the annotation item OTHERS without a package name; or
>     * All of the following must be true:

"must be" --> "are"

>       -- Each *object_*name in A1 is covered by an annotation item in A2 or is
>          an object that would not need to be included in A1 if it was explicitly
>          referenced within the entity defining A1;
>
>          AARM Reason: The latter part means that local objects in a subprogram S
>          do not need to be included its annotation when they are included in
>          the annotation for a nested subprogram of S that S calls.
>
>       -- Each *formal_parameter_*name item in A1 is found in A2;
>       -- Each *access_*subtype_mark item in A1 is found in A2 or, if the
>          the subtype_mark denotes a pool-specific access type,
>          an OTHERS annotation item in A2 naming the package P in which the
>          pool of the access type is declared; and
>       -- For each OTHERS annotation item with a package name P, there is
>          an OTHERS annotation item in A2 that statically denotes P.
>
> AARM Ramification: This definition is not symmetrical; A2 may allow
> more than
> A1 requires (such as having an annotation of (others)).

Heh?  I don't get the juxtaposition of "allow" and "requires".

> A type T is *compatible* with an annotation A of an aspect if:
>     * T is a generic formal type, and A contains the *formal_parameter_*name
>       of the formal type; or
>     * The annotation for the same aspect of T is compatible with A.

This seems to be talking about annotations/aspects in general, not just globals.
Is that intended?

> The result of a *union* of annotation A1 with annotation A2 is:
>     * if A1 contains NULL, A2;
>     * if A2 contains NULL, A1;
>     * if either A1 or A2 contains an OTHERS annotation
>       without a package name, an annotation with a single item of OTHERS without a package name;
>     * Otherwise, an annotation with all of the Annotation_Items of A1 and A2 with any duplicates
>       removed.
>
> AARM Ramification: This definition is symmetrical; the order of the
> operands does not matter.
>
>
> Unless otherwise specified (either explicitly or defined by this
> International Standard),

What does "(either..." mean?

> the annotation for each defined aspect is (others).
>
> AARM Ramification: (others) allows all global references, so it is
> completely compatible with earlier versions of Ada.
>
> An inherited subprogram (see 3.4) inherits the annotations of the
> primitive subprogram of the parent or progenitor type. Redundant[The
> annotations can be changed on an overriding subprogram, with some
> restrictions.]

Need to merge multiple parents?  Or is that handled below?

> When determining the Global in annotations of entities declared in an
> instantiation of a generic G, each *formal_parameter_*name item F of
> every Global in annotation A of any entities declared in the instance
> that references a formal parameter of G is removed from A and:
>    * if F is a formal type, the result is the union of A and the Global in annotation
>      of the actual type;
>
>    * if F is a formal subprogram, the result is the union of A and the Global in annotation
>      of the actual subprogram;
>
>    * if F is a formal IN OUT parameter, the *object_*name of the actual parameter is added
>      to A if that *object_*name would need to be included in a Global in annotation
>      for the enclosing entity when it is read at the point of the instance, Redundant[and
>      nothing is added otherwise].
>
> Analogous rules apply to a Global out annotation (replacing "in" by
> "out" and "read" by "written" everywhere).
>
> AARM Discussion: At the point of an instance, all of the references to
> the formal parameters are replaced by the annotations of the actual.
> This does not require re-analyzing the generic.
>
>
> Legality Rules
>
> An annotation_list can be given if and only if the aspect is Global,
> Global'Class, or Global'Access.
>
> The aspect Global shall be given only on subprograms, types, packages,
> and generic packages.

Not generic subprograms?  Entries?  Task bodies?

> The aspect Global'Access shall be given only on access-to-subprogram types.
>
> The aspect Global'Class shall be given only on primitive subprograms
> of a tagged type.
>
> The Annotation_Item NULL shall appear alone in an Annotation_List.

Same for "others" (without pkg name)?

> An *object*_name given in an Annotation_List shall statically denote
> some object.
>
> An *access*_subtype_mark given in an Annotation_List shall denote a
> pool-specific access type.

???Hmm...

> A *formal_parameter_*name given in an Annotation_List shall statically
> denote some generic formal parameter of an enclosing generic unit; the
> formal parameter shall be a formal type, a formal subprogram, or a formal IN OUT object.
>
> If a subprogram contains a Global in annotation, then:
>   * Every object that is read by the subprogram body shall either be accessible
>     from the function call, be a constant object of an elementary type, or be
>     covered by the Global in annotation.

Or be nested inside the subprogram, right?

What does "accessible from the function call" mean?
(And shouldn't it be "subp call"?)

It seems like a pain to mention constants.  Can we limit this to "nonlimited",
rather than "elementary"?

>   * The subprogram corresponding to each dispatching call in the subprogram body
>     which has a dynamically tagged controlling operand shall have a compatible
>     Global'Class in annotation; the access-to-subprogram type for each call of
>     a dereference of an access value shall have a compatible Global'Access in
>     annotation; the *formal_parameter_*name for each call of a formal subprogram
>     is present in the annotation; and the subprogram corresponding to every other
>     call in the subprogram body shall have a compatible Global in annotation.
>   * The type of every stand-alone object declared by the subprogram shall be
>     compatible with the annotation.

I don't get it.

>   * Every nested package and package instantiation declared by the subprogram
>     shall have a compatible Global in annotation.
>   * The type of each assignment_statement in the subprogram body shall be compatible
>     with the annotation. In addition, if the target of the
>     assignment_statement is a dereference of some access type A, the Allocate
>     and Deallocation routines associated with the storage pool of type A in
>     the subprogram body shall have a compatible Global in annotation.
>
>     AARM Reason: Allocate and Deallocate can be called here if the implementation
>     chooses; we have to assume the worst.

Heh?

>   * The Allocate and Deallocate routines associated with the storage pool for the
>     type of each allocator in the subprogram body shall have compatible Global in
>     annotations.
>
>     AARM Reason: Again, Deallocate can be called here if the implementation chooses;
>     we have to assume the worst.
>
>   * For each attribute A'Storage_Size in the subprogram body where A is an access
>     type, the Storage_Size routine associated with the storage pool of A shall
>     have a compatible Global in annotation.
>
>   * If the subprogram contains a call on an instance of Unchecked_Conversion with
>     a pool-specific access type A as the target type, the subprogram is
>     illegal if the type A is named as an *access*_subtype_mark annotation item.

This one seems like overkill.

>     AARM Reason: We assume that objects of type A can only designate objects in
>     the pool of A. The only way to violate this is to use Unchecked_Conversion
>     from a general access type value; if such a conversion exists, we require
>     the subprogram to be annotated as if A is a general access type.
>
> AARM Ramification: Local objects, elementary constant objects
> (declared anywhere) and the parameters of the call do not need to appear in a Global in annotation.

Shouldn't be allowed.

> Note that this is referring to constant objects, not just constant
> views of an object.
>
> A write of a dereference of an object P *reads* the object P (and
> writes the designated object).
>
> The prefix of a protected function call is considered to be read; the
> prefix of a protected procedure or entry call is considered to be both
> read and written. The prefix of a task entry is considered to be read.
> These rules follow from the requirements in 9.5 on whether or not the
> prefix of a protected subprogram call or an entry call can be a
> constant; we don't want to be logically writing constants.
> End AARM Ramification.
>
> AARM Discussion: We don't need a rule for Deallocate calls in
> Unchecked_Deallocation, as it is a call and does not have annotations
> defined. Thus the above rule will always fail and thus we don't care about the annotations on Deallocate.

So anything that calls U_D has to have "others"?

> End AARM Discussion.
>
> Analogous rules apply to a Global out annotation (replacing "in" by
> "out" and "read" by "written" everywhere).
>
> [Editor's note: I don't want to duplicate the rules, they're complex
> enough as it is.]

Agreed!

> For an attribute P'Access of access-to-subprogram type S that has a
> Global'Access in annotation, subprogram P shall have a compatible
> Global in annotation. Similarly, for a type S that has a Global'Access
> out annotation, subprogram P shall have a compatible Global out annotation.
>
> [Editor's note: One could argue that this belongs in 3.10.2; I put it
> here to keep all of the relevant rules together.]

I agree to keeping all these rules together.

================================================================

> (Partial) Minutes of the Amendment subcommittee of the ARG conference
> call of December 10, 2009
>
> Attendees: Bob Duff, Tucker Taft, Randy Brukardt, Steve Baird, Gary
> Dismukes, Ed Schonberg
>
> AI05-0186-1/01
>
> Bob says that this is essential if you ever want to do any analysis of
> programs without all of the source code available.
>
> Bob comments that the write up talks about function too much, it
> should say subprogram more. Tucker notes that this is mainly an issue
> in !problem. Randy notes that the motivating case has to do with
> functions, so it just talks about that there.

I don't get that.  I see no difference between a function and a procedure,
except for syntax.

> Bob wonders if we should talk about variables rather than constants.
> He doesn't want to annotate reads of global constants. Not all
> constants are really constants, however. Calling an entry of tasks if
> side-effect, even if the task is a constant. He is not sure what the
> right answer is (we could except elementary constants from the rules without problems).
>
> Elementary Operators would have null annotations. Randy notes that
> composition of equality means that we have to exclude composite
> operators, as they might contain user-defined parts (even array "=" has that problem).

But "and" on boolean arrays, for ex., doesn't mess with globals.

> Steve would like this to preserve the separation of static and dynamic
> semantics. That is the intent - he notes that Pure does not do that.
> That means the wording shouldn't talk about what happens at elaboration.

I don't understand Steve's point.

> ****************************************************************
>
> Example of access annotations, February 1, 2010, Randy Brukardt

>     type Clonee is tagged record
>         Data : Data_Access;
>     end record;

I think you wanted Clonee to be controlled, and say "overriding" on the
following.

>     procedure Adjust (Obj : in out Clonee) with
>        Global in out => (others in Clones);
>
>     procedure Finalize (Obj : in out Clonee)
>        Global in out => (others in Clones);

****************************************************************

From: Randy Brukardt
Sent (privately): Tuesday, February 2, 2010  7:03 PM & Thursday, February 4, 2010

> I'm having trouble understanding this AI, and some others, because
> AI05-0183-1 is still up in the air.
> Tuck, would you mind putting that one at the head of your priority
> queue?

I agree. I left out all of the resolution issues from this AI, as they ought to
be covered in AI05-0183-1. But they're not there yet.

> General comments.
>
> I find it difficult to understand this AI (even ignoring the
> AI05-0183-1 issue).  I'm not blaming you, Randy -- I think it's just
> hard.

Well, I do have a tendency to ramble; I often find others (especiall Tucker)
explaining something I was struggling to put into words much more clearly. So
I'm certain there is room for improvement.

One thing that is missing is an overview of the meaning of things. It just jumps
into wording, so you are missing a roadmap. Perhaps that would be a good
assignment for you to undertake (it would bring a fresh perspective as well).

> I think perhaps globals annotations should not apply to nested
> subprograms.  A tool (or a human reader) can reasonably be expected to
> just figure it out.  All the relevant code is just there.  Yes, in
> case of subunits, the tool needs to do an inter-compilation-unit
> analysis, but I think that's reasonable.

I am 100% against any sort of inter-compilation unit analysis. Janus/Ada has no
such capability and will get one over my dead body. (I believe body dependencies
are the root of all evil; we don't have any.)

Anything separately compiled needs proper contracts. Period.

As a lesser issue, doing that would greatly complicate the wording, because now
you'd have to include everything present (logically) in the body, not just
syntactically in the body. I designed the rules here to only require talking
about things in the syntax.

> I think it would be useful to have a way to say "The default
> annotation in this scope is 'null' instead of the usual 'others'."
> Or maybe a general way to set the default (e.g. to 'all variables in
> this package').

Maybe, but this is so complex already that I am dubious that making it more
complex is very helpful. And the experience with the containers shows that the
annotations vary from routine to routine (depending on proc vs. func, and reader
versus modifier).

> I don't buy the idea that tools that make potentially-false
> assumptions are useless.  Suppose a tool assumes X, and proves all
> kinds of assertions true based on that.  And suppose X might be false.
> Well, we've still got useful info
> -- we know that "X implies so-and-so" (or, for the imply-o-phobes, "if
> X then so-and-so").  If X is usually true, and can be checked
> separately (perhaps by hand), then it's OK.

Well, it is useless for a compiler to optimize based on such assumptions
(optimize here includes reducing/removing assertions/preconditions/etc.) That's
because doing so can introduce erroneousness into programs that don't have any.
That's beyond bad.

I make no claims about what stand-alone tools can or can't do. I don't believe
in them much; I believe more in the omnipitant compiler.

> One X I'm thinking of here is [De]allocate.  I hate to see all kinds
> of pessimistic assumptions, that basically ruin any attempt to prove
> anything about any subprogram that does 'new' or U_D.  Yeah, the
> storage pool can have side effects, but they're usually at a totally
> different level from the code that invokes them.

I'll address this particular issue later; it doesn't need to be assume-the-worst
in general. I just didn't address it to keep the size of the proposal from
getting out of hand.

> Note that pure-functional languages do not consider "new" to be a side
> effect.

They don't have pools and cross-links, though, and those are the problem case.
If we don't handle those properly, these annotations will be worse than useless,
they'll be actively misleading.

> I'm not sure how we intend to deal with low-level chap-13-ish stuff.
> There's a mention of Unchecked_Conversion here, but that's in the same
> category as machine-code inserts, address clauses, etc.
> Seems to me all these things need to be treated the same, namely it's
> the programmer's responsibility to ....

The Unchecked_Conversion rules is specifically to plug a hole related
conversions into pool-specific access types. That's a common thing to do in Ada
83 code, and I didn't think it was a good idea to ignore it for that reason.

In all other cases, we are talking about erroneous code (or code that ought to
be declared that way, I think the rule for machine code insertions is missing,
there ought to be one like the one for interfaces); and there never is a
requirement in Ada that erroneous code does anything sane. In addition, I don't
expect lying about Global annotation for Imported/Exported subprogram, broken
machine code insertions, or abuse of
Unchecked_Conversion/Address_to_Access_Conversions (there is only a problem if
the designated type is incorrect) to be common. (Unlike the Unchecked_Conversion
to pool-specific access types.)

> > Annotations are provided to describe the use of global objects by
> > subprograms.
> >
> > !problem
> >
> > We're considering adding many kinds of annotations to Ada (see
> > AI05-0145-1 and AI05-0146-1) in order to increase the ability of a
> > programmer to specify contracts for types and subprograms. These
> > contracts are defined to be checked at runtime, but are intended to
> > be potentially checked (at least in part) statically.
> >
> > However, without knowledge of side-effects of functions used in the
>
> "functions" --> "subprograms".
>
> > annotations, a tool has to assume the worst about any user-defined
> > functions.

You can't use any subprograms other than functions in
assertions/preconditions/etc. "Annotations" really is the wrong term here;
they're really "contract aspects".

> When I said this at the last phone meeting, Ed pointed out that
> there's an alternative: whole-program analysis.  So I suggest adding
> "(or perform whole-program analysis)" at the end of the above
> sentence.  No need to point out the drawbacks of that.

As you later note, the next paragraph covers that. Do I need to say something
here?

> >...That is, that the result of a function can change even when
>
> "That is" --> "For example".
>
> > called with the same operands. Other assumptions could
> cause incorrect
> > programs to be accepted as correct, and if the assumptions
> were used
> > to omit "proved" annotations, to erroneous execution.  Both of these
>
> "erroneous" --> "incorrect".

I really meant "erroneous". If checks that fail are suppressed, execution is
erroneous. That's what's happening here (the compiler suppressing checks that
need to be made).

> > results are unacceptable for a feature intended to improve the
> > correctness of programs.
> >
> > The worst-case  assumptions pretty much prevent any
> analysis unless
> > the bodies  of  any  user-defined  functions  used in  the
> > annotations  are available.
>
> OK, I see...
>
> >... This is bad, as it  prevents analysis of programs as they are
> > constructed.   If  the   body   is  not   available,   no
> analysis   is
> > possible. Moreover, analysis depending on a body require creating
> >pseudo  body dependencies  (if the  body is changed,  any analysis
> >depending on  that properties of that body would  have to be
> performed
> >again); but the
>
> "that properties" --> "the properties"
>
> > language  does not  allow  these  to be  "real"  body dependencies
> > (any recompilation needed has to occur automatically).
> >
> > Ideally, analysis at the initial compile-time of a unit would be
> > possible, as it is important to detect errors as soon as possible.
> > More information about function side-effects is needed in the
> > specification of subprograms in order to accomplish that goal.
> >
> > !proposal
> >
> > Add global in and global out annotations to Ada, for subprograms,
> > packages, and types. Add related annotations for dispatching
> > subprograms and access-to-subprogram types.
> >
> > The global annotations for types cover default
> > initialization/adjustment/finalization.  The global annotations for
> > packages cover operations that occur as part of the elaboration for
> > packages.
>
> Hmm...  Are we really sure it's OK to lump all that together.
> I can imagine being frustrated when I want to give different 'globals'
> for init versus final, e.g.

I don't know. We decided that during a phone call (the one before the previous
one). Not doing thing would make things three times more complex, and all of the
examples I've looked at show that there isn't any difference in practice except
for ACATS test counters and the like.

> > !wording
> >
> > Add a new section:
> >
> > 13.3.4 Global usage annotation
> >
> > Semi-formal description: [Editor's note: This part depends heavily
> > on the unfinished AI05-0183-1; it's not worth trying to describe
> > these rules until that AI is finished.]
> >
> > Add to the aspect syntax given in AI05-0183-1:
> >
> >     Aspect_Mark [in|out|in out] => Annotation_List
> >
> >     Annotation_List ::= ( Annotation_Item {, Annotation_Item} )
> >
> >     Annotation_Item ::= *object_*name | *access_*subtype_mark |
> >                          NULL | ACCESS subtype_mark |
> >                          OTHERS [IN *package*name] |
> >                          GENERIC *formal_parameter_*name
>
> A "generic formal parameter" is not a "formal parameter".

So what is it?

> > The names in these items resolve with the same visibility as other
> > aspect expressions (that usually is the end of the visible part).
> > The names must resolve without context.
> >
> > [Editor's note: We need the keyword GENERIC here, so that
> we can tell
> > the difference between references to the initialization and the
> > referenced data for formal pool-specific access types in
> annotations.
> > Both use the access type name. An alternative would be to add a
> > keyword to the *access_*subtype_mark case instead, but nothing that
> > isn't ambiguous seems appropriate. My best idea was
> > *access_*subtype_mark.ALL .]
> >
> > Aspect_Mark in out => Annotation_List is semantically equivalent to
> > Aspect_Mark in => Annotation_List, Aspect_Mark out =>
> Annotation_List.
> >
> > AARM Discussion: All of the rules are defined in terms of
> "Aspect_Mark in"
> > and "Aspect_Mark out". The rules are applied twice (once
> for "in" and
> > once for "out") to "Aspect_Mark in out".
> >
> > Aspects Global, Global'Class, and Global'Access are defined.
> >
> > [End semi-fomal description. From here to the end is intended to be
> > actual wording.]
> >
> > Static Semantics
> >
> > A read or write of an object O is *covered by an annotation* in an
>
> Please, PLEASE don't use "O" as an object name!
> "X" or "Obj" or ...

OK.

> > Annotation_List if:
> >     * O statically denotes a part of an object named in the
> > Annotation_List;
>
> I'm not sure "statically denotes" is right, here.
> Don't you want to include a record component X.Y, for example?

We definitely have to use "statically denotes" (or something similar), because
we don't want to include anything with dynamic parts:

    Obj : T renames Ptr.all;

Don't want Obj in an annotation, but it "denotes" an object - but it doesn't
"statically denote" an object.

I don't much care about record components; I was thinking mainly of top-level
objects. But I thought that "statically denotes" did apply to record components
so long as the prefix is something that can be "statically denoted". I'll have
to go back and read the definition again.


> >     * The annotation item OTHERS without a package name
> occurs in the list;
> >     * The annotation item OTHERS with a package name P
> occurs in the list, and
> >       O denotes part of an object declared in P, or O
> denotes a part of an object
> >       produced by a dereference of an object of an pool-specific
> > access type whose
>
> "an" --> "a"
>
> >       pool is declared in P;
>
> Including children and nested packages?

Good question. I would say nested yes, children no, but I don't know how to
enforce that. (Nested yes because they can be totally hidden in the private
part, and we don't want to have no possible annotation for them.)

> >     * O denotes a part of an object produced by a dereference of an object with
> >       designated type T, and the type D given in an ACCESS D
> >       annotation item covers T; or
> >     * O denotes a part of an object produced by a dereference of an object of
> >       a pool-specific access type named in the Annotation_List.
> >
> > AARM Ramification: OTHERS by itself allows anything to be
> read or written.
> >
> > AARM Discussion: ACCESS D represents reading/writing of any
> aliased or
> > tagged object (including those allocated from pools) with a type
> > covered by the type D.
> >
> > "Statically denotes" does not include dereferences, so the
> first rule
> > only applies to statically declared objects.
>
> I don't think "statically declared" means anything.

Well, what you you say instead? I'm talking about objects that are declared
(ultimately) by declarations that are known statically.

> > An annotation A1 is *compatible* with another annotation A2 if:
>
> "An annotation"?  We're only talking about globals annotations...

"annotation" throughout this wording is short for "Annotation_List", the syntax
here. This syntax is only used (currently) for the family of globals
annotations, but there are already three such aspects (and in and out versions
of each). I probably ought to look at this more carefully.

"An annotation defined by an Annotation_List is *compatible* with another such
annotation A2 if:

Or something like that.

> >     * A1 contains NULL; or
> >     * A2 contains the annotation item OTHERS without a
> package name; or
> >     * All of the following must be true:
>
> "must be" --> "are"

OK.

...
> > AARM Ramification: This definition is not symmetrical; A2 may allow
> > more than
> > A1 requires (such as having an annotation of (others)).
>
> Heh?  I don't get the juxtaposition of "allow" and "requires".

I probably meant "requires it to allow" or something like that, but I agree that doesn't make much sense.

"...allow more object accesses than A2 allows..."

> > A type T is *compatible* with an annotation A of an aspect if:
> >     * T is a generic formal type, and A contains the
> *formal_parameter_*name
> >       of the formal type; or
> >     * The annotation for the same aspect of T is compatible with A.
>
> This seems to be talking about annotations/aspects in general, not
> just globals.  Is that intended?

Again, there are three aspects in question (Global, Global'Class,
Global'Access), and I've thought in the past we needed more.

> > The result of a *union* of annotation A1 with annotation A2 is:
> >     * if A1 contains NULL, A2;
> >     * if A2 contains NULL, A1;
> >     * if either A1 or A2 contains an OTHERS annotation
> >       without a package name, an annotation with a single
> item of OTHERS without a package name;
> >     * Otherwise, an annotation with all of the
> Annotation_Items of A1 and A2 with any duplicates
> >       removed.
> >
> > AARM Ramification: This definition is symmetrical; the order of the
> > operands does not matter.
> >
> >
> > Unless otherwise specified (either explicitly or defined by this
> > International Standard),
>
> What does "(either..." mean?

either specified explicitly by the programmer (in the source code), or specified
by the Standard (as for scalar operators, etc.)

> > the annotation for each defined aspect is (others).
> >
> > AARM Ramification: (others) allows all global references, so it is
> > completely compatible with earlier versions of Ada.
> >
> > An inherited subprogram (see 3.4) inherits the annotations of the
> > primitive subprogram of the parent or progenitor type.
> Redundant[The
> > annotations can be changed on an overriding subprogram, with some
> > restrictions.]
>
> Need to merge multiple parents?  Or is that handled below?

I wasn't expecting abstract or null subprograms to have annotations, but perhaps
they ought to. Otherwise, though, you'd only inherit from a concrete parent, and
there can only be one of those. Probably needs more wording.

...
> > The aspect Global shall be given only on subprograms,
> types, packages,
> > and generic packages.
>
> Not generic subprograms?  Entries?  Task bodies?

Blah. Forgot the first. The last isn't necessary; the annotation can (and
should) be given on the type. But I suppose we need a whole set of rules for
checking a task body. Barf. We need to find a way to share the rules: I couldn't
do it.

Entries is problematic because task entries don't have "bodies" per se, so I
don't know how to define what to check.

> > The aspect Global'Access shall be given only on
> access-to-subprogram types.
> >
> > The aspect Global'Class shall be given only on primitive
> subprograms
> > of a tagged type.
> >
> > The Annotation_Item NULL shall appear alone in an Annotation_List.
>
> Same for "others" (without pkg name)?

We could do that, I though it was better to be able to say:

    Global in => (Global_Counter, Wishing_Well, others)

which means that you access the two named items and unspecified other stuff.

But it isn't a big deal (you can't prove much additional with the above).

> > An *object*_name given in an Annotation_List shall statically denote
> > some object.
> >
> > An *access*_subtype_mark given in an Annotation_List shall denote a
> > pool-specific access type.
>
> ???Hmm...

I thought it was very confusing to have both with very different semantics.
Tucker is now suggesting turning this whole model upside down. If we do that,
then this annotation has to go away anyway (it would conflict with other
meanings).

> > A *formal_parameter_*name given in an Annotation_List shall
> > statically denote some generic formal parameter of an enclosing
> > generic unit; the formal parameter shall be a formal type, a formal
> subprogram, or a formal IN OUT object.
> >
> > If a subprogram contains a Global in annotation, then:
> >   * Every object that is read by the subprogram body shall
> either be accessible
> >     from the function call, be a constant object of an
> elementary type, or be
> >     covered by the Global in annotation.
>
> Or be nested inside the subprogram, right?
>
> What does "accessible from the function call" mean?
> (And shouldn't it be "subp call"?)

Perhaps if you put this this question together with the previous paragraphs
question, you'd see that one is the answer to the other. "Accessible from the
function call" (which is a dynamic concept checked statically) includes the
locals and the parameters: it's the accessibility from AI-142-4.

> It seems like a pain to mention constants.

We don't *have* to mention them, but then you'd have to annotate them. You said
you didn't want that.

>  Can we limit this
> to "nonlimited", rather than "elementary"?

No. Go back and read AI05-0054-2 again. We could say "types that cannot have
parts of immutably limited or controlled types", but that is pretty much the
same as "elementary" statically. You can't include any parts of private types,
any classwide types, etc. That leaves String and Complex and not much else. The
rule would take a whole paragraph by itself to define, and that would make this
thing much more complex.

> >   * The subprogram corresponding to each dispatching call
> in the subprogram body
> >     which has a dynamically tagged controlling operand
> shall have a compatible
> >     Global'Class in annotation; the access-to-subprogram
> type for each call of
> >     a dereference of an access value shall have a
> compatible Global'Access in
> >     annotation; the *formal_parameter_*name for each call
> of a formal subprogram
> >     is present in the annotation; and the subprogram
> corresponding to every other
> >     call in the subprogram body shall have a compatible
> Global in annotation.
> >   * The type of every stand-alone object declared by the
> subprogram shall be
> >     compatible with the annotation.
>
> I don't get it.

Words missing. And the intended wording is too complex anyway. "shall have a
compatible annotation" is better.

> >   * Every nested package and package instantiation declared
> by the subprogram
> >     shall have a compatible Global in annotation.
> >   * The type of each assignment_statement in the subprogram
> body shall be compatible
> >     with the annotation. In addition, if the target of the
> >     assignment_statement is a dereference of some access
> type A, the Allocate
> >     and Deallocation routines associated with the storage
> pool of type A in
> >     the subprogram body shall have a compatible Global in
> annotation.
> >
> >     AARM Reason: Allocate and Deallocate can be called here
> if the implementation
> >     chooses; we have to assume the worst.
>
> Heh?

Go read AI05-0107-1 again.

...
> >   * If the subprogram contains a call on an instance of
> Unchecked_Conversion with
> >     a pool-specific access type A as the target type, the
> subprogram is
> >     illegal if the type A is named as an
> *access*_subtype_mark annotation item.
>
> This one seems like overkill.

As I mentioned yesterday, this is so common in Ada 83 code that I thought it
ought to be included. It completely destroys the model of pool-specific access
types, and most importantly, it is *not* erroneous for it to do that.

> >     AARM Reason: We assume that objects of type A can only
> designate objects in
> >     the pool of A. The only way to violate this is to use
> Unchecked_Conversion
> >     from a general access type value; if such a conversion
> exists, we require
> >     the subprogram to be annotated as if A is a general access type.
> >
> > AARM Ramification: Local objects, elementary constant objects
> > (declared anywhere) and the parameters of the call do not
> need to appear in a Global in annotation.
>
> Shouldn't be allowed.

Locals or parameter can't be because of visiblity. I see no reason to disallow
giving constants (especially for reading purposes), it just isn't going to have
much effect.

...
> > AARM Discussion: We don't need a rule for Deallocate calls in
> > Unchecked_Deallocation, as it is a call and does not have
> annotations
> > defined. Thus the above rule will always fail and thus we
> don't care about the annotations on Deallocate.
>
> So anything that calls U_D has to have "others"?

That's the current model, because at some point we have to stop. Each new thing
we try to annotate is more work and possible errors.

It wouldn't be that hard to annotate U_D, because it could use the annotation of
the pool's Deallocate routine. I'm not certain that is enough, however.

...
> > Bob comments that the write up talks about function too much, it
> > should say subprogram more. Tucker notes that this is
> mainly an issue
> > in !problem. Randy notes that the motivating case has to do with
> > functions, so it just talks about that there.
>
> I don't get that.  I see no difference between a function and a
> procedure, except for syntax.

The motivating case is in precondition expressions. If you can explicitly call a
procedure there, you aren't using Ada. Talking about something you can't do in
the context of discussion isn't helpful.

The actual rules are on subprograms, of course.

You made the same mistake in the AI-147 problem; it's a problem statement, not a
general statement of usefulness. It's not a laundry list!

...
> > Elementary Operators would have null annotations. Randy notes that
> > composition of equality means that we have to exclude composite
> > operators, as they might contain user-defined parts (even
> array "=" has that problem).
>
> But "and" on boolean arrays, for ex., doesn't mess with globals.

The actual rules go further; I'm not sure why you are reading these !appendix
minutes rather than the actual proposal.

> > Steve would like this to preserve the separation of static
> and dynamic
> > semantics. That is the intent - he notes that Pure does not
> do that.
> > That means the wording shouldn't talk about what happens at
> elaboration.
>
> I don't understand Steve's point.

Legality Rules should not depend on Dynamic Semantics rules. Elaboration is a
dynamic semantics rule. Steve can expand if I oversimplified.

****************************************************************

From: Bob Duff
Sent (privately): Tuesday, February 2, 2010  8:31 PM

> > Note that pure-functional languages do not consider "new" to be a
> > side effect.
>
> They don't have pools and cross-links, though, and those are the
> problem case. If we don't handle those properly, these annotations
> will be worse than useless, they'll be actively misleading.

What do you mean by "cross links"?

Yes, pure-functional languages typically don't have pools.
But if they did, I don't think it would change things in this regard.  Of
course, the real issue is that such languages don't have pointer equality (e.g.
Lisp's 'eq').

****************************************************************

From: Randy Brukardt
Sent (privately): Thursday, February 4, 2010  12:55 AM

> What do you mean by "cross links"?

I mean when objects share other objects, as in the example I put in the
!appendix.

> Yes, pure-functional languages typically don't have pools.
> But if they did, I don't think it would change things in this regard.
> Of course, the real issue is that such languages don't have pointer
> equality (e.g. Lisp's 'eq').

Pure functional languages never share objects, do they? Everything is by-copy,
at least logically. So this is a very different problem.

****************************************************************

From: Tucker Taft
Sent (privately): Thursday, February 4, 2010  11:51 PM

One thing I see emerging in these global annotations which I find intriguing is
that we are beginning to give mechanisms whereby a global annotation can
effectively say: my global side-effects include those of <blah>.  This is as
opposed to going over to <blah>, copying all of its global side-effects into the
global annotations for this routine that presumably calls <blah>.

From a maintenance point of view, it may be better to simply announce that there
is an internal call on <blah> inside somewhere, rather than copying the global
side effects from <blah>. Clearly the global annotations on <blah> might change,
and if that is true, we might have to go and change the global annotations on
everything that calls <blah>.  Which would be <blech>!

This seems like a choice that it is nice to be able to provide: for each call
inside a routine, you can either incorporate the global effects of that call
into the global effects for the caller, or you can simply include the fact that
you made such a call in the global annotation.  I would think the name of the
subprogram would be an appropriate way to indicate that in the global "object"
list.

For type-related annotations, you would have the same choice.  And as suggested
in my earlier response, I might suggest:

   global in out => (new <type_name>)

as a way to indicate that global effects of creating/adjusting/finalizing an
object of the given type should be assumed for the routine with the given global
annotation.

It becomes interesting when you call a formal subprogram, or you create an
object of a formal type.  In those cases you clearly can't incorporate the
global effects of these operations directly, but instead you can only admit the
fact that you are doing these things.  Similarly, for a call through an
access-to-subprogram value, you can't easily incorporate the global effects, but
you can admit that you are making such a call. Here I would expect something
like:

   global in out => (acc_to_subp_param.all)

as a way of indicating that a call is made through the given acc_to_subp_param,
and whatever side effects that implies should be assumed. If you don't or can't
indicate the particular acc-to-subp value through which you are calling, could
use the type name instead:

   global in out => (acc_to_subp_type.all)

Presuming I understand the intent, it seems important to distinguish the forms
of Annotation_Item which are specifying some "direct" global side-effect, versus
when we are essentially specifying a global side-effect *indirectly* in terms of
some other subprogram being called or some specified type being
created/adjusted/finalized.

****************************************************************

From: Randy Brukardt
Sent (privately): Thursday, February 4, 2010  12:13 AM

> One thing I see emerging in these global annotations which I find
> intriguing is that we are beginning to give mechanisms whereby a
> global annotation can effectively
> say: my global side-effects include those of <blah>.  This is as
> opposed to going over to <blah>, copying all of its global
> side-effects into the global annotations for this routine that
> presumably calls <blah>.

Right. I found that without some way to do that for generics, all was lost.

On the other hand, I decided it was necessary to move away from it for access
types, because it doesn't model what really happens in the body.

>  From a maintenance point of view, it may be better to simply announce
> that there is an internal call on <blah> inside somewhere, rather than
> copying the global side effects from <blah>.
> Clearly the global annotations on <blah> might change, and if that is
> true, we might have to go and change the global annotations on
> everything that calls <blah>.  Which would be <blech>!

That might make sense for visible routines, although it seems to be exposing a
lot about the body: that could be bad of maintainance removes the call to
<blah>. Maybe the least of two evils.

> This seems like a choice that it is nice to be able to
> provide: for each call inside a routine, you can either incorporate
> the global effects of that call into the global effects for the
> caller, or you can simply include the fact that you made such a call
> in the global annotation.  I would think the name of the subprogram
> would be an appropriate way to indicate that in the global "object"
> list.

Resolution of the list is going to be a nightmare. There is also the problem of
overloading (which I was planning to talk about tomorrow if we got past the
"big" issues): just giving the name of a subprogram isn't enough -- different
overloaded versions have different annotations. Just look at the vectors example
in the AI:

   function Element (Container : Vector;
                     Index     : Index_Type)
      return Element_Type with
      Global in out => (generic Element_Type);
      -- Creates an element.

   function Element (Position : Cursor) return Element_Type with
      Global in  => (access Vector, generic Element_Type),
      Global out => (generic Element_Type);

If you say "Ada.Containers.Bounded_Vector.Element" in an annotation, which of
these annotations do you get? And I can easily imagine that the annotations
could be more different than these.

> For type-related annotations, you would have the same choice.
>  And as suggested in my earlier response, I might suggest:
>
>    global in out => (new <type_name>)
>
> as a way to indicate that global effects of
> creating/adjusting/finalizing an object of the given type should be
> assumed for the routine with the given global annotation.

That looks too much like an allocator to me.

> It becomes interesting when you call a formal subprogram, or you
> create an object of a formal type.  In those cases you clearly can't
> incorporate the global effects of these operations directly, but
> instead you can only admit the fact that you are doing these things.
> Similarly, for a call through an access-to-subprogram value, you can't
> easily incorporate the global effects, but you can admit that you are
> making such a call.
> Here I would expect something like:
>
>    global in out => (acc_to_subp_param.all)
>
> as a way of indicating that a call is made through the given
> acc_to_subp_param, and whatever side effects that implies should be
> assumed.

This makes no sense at all. You have to declare those side effects somewhere,
there is no possible way to assume them. And once you have them, the rules
follow from the call.

I really don't like the ".all" syntax, because it is ambiguous with
<object_name>, so there can be no syntax marker as to what is expected. Meaning
resolution is a nightmare (resolving for subprogram names, subtype names, and
object names all at the same time is something you never do in any other context
-- you could almost do it if you feed back the legality rules to control the
resolution, but Ada doesn't allow that. Example: if T is a subtype name, T(A) is
an object, T.all is an object; but you want to interpret it as a subtype name
and magic syntax. How do you do that??

> If you don't or can't indicate the particular acc-to-subp value
> through which you are calling, could use the type name instead:
>
>    global in out => (acc_to_subp_type.all)
>
> Presuming I understand the intent, it seems important to distinguish
> the forms of Annotation_Item which are specifying some "direct" global
> side-effect, versus when we are essentially specifying a global
> side-effect *indirectly* in terms of some other subprogram being
> called or some specified type being created/adjusted/finalized.

This I agree with, but you aren't doing that (at least with viable syntax).

****************************************************************

From: Steve Baird
Sent (privately): Thursday, February 4, 2010  2:53 PM

>>> Do we deal with ... finalization of aggregate temps?

> I don't know, because I don't know what you mean by an "aggregate temp".

I was wondering about the annotations for a subprogram Foo that contains, for
example, the following construct:

    if Some_Controlled_Type'(<aggregate>) in Some_Subtype then
     ...
    end if;

The Finalize routine for Some_Controlled_Type will be invoked.
What rule in the AI requires that this be reflected in the annotations of Foo?

****************************************************************

From: Randy Brukardt
Sent (privately): Thursday, February 4, 2010  3:05 PM

Ah. Luckily, this is Bob's problem now. ;-)

A more realistic example would be:

      Count := Fancy_Operation (Some_Controlled_Type'(<aggregate));

And note of course that you can't necessarily know that the object is
controlled. So we would need a rule like:

* The type of every aggregate given in the subprogram shall have a compatible
  Global in annotation.

Note that "given in the subprogram" here means syntactically, as do all of these
other rules; things that happen in other callable entities are necessarily
included in their annotations, and their annotations already have to be
compatible. (Not sure if there is better wording for that, I'm sure Bob will
figure it out.)

****************************************************************

From: Steve Baird
Sent (privately): Thursday, February 4, 2010  5:06 PM

The word "syntactically" is a bit of hyperbole, but I know what you mean.

In particular, I'm thinking about defaulted parameters, e.g.
     Some_Controlled_Type'(<aggregate>) in Some_Subtype as a default parameter
     value.

****************************************************************

From: Randy Brukardt
Sent (privately): Thursday, February 4, 2010  5:11 PM

Right, default expressions are considered to directly appear at the point of the
call. That has to be true for simple object reads and writes, not to mention
more complex stuff like allocators and aggregates. So you are right that the
rules aren't quite purely syntactic. I just don't like "given in" much, as it is
so vague. Not sure what the best phrasing is.

****************************************************************

From: Tucker Taft
Sent: Thursday, February 4, 2010  4:35 PM

Bob Duff asked that I send out a paragraph or two summarizing my "high-level"
view of this AI.  So here goes...

A Global in/out annotation specifies the global side-effects of a subprogram
call, the creation (adjustment/finalization) of an object, the elaboration of a
package, etc.  Each item in the list of items given in a Global annotation can
be viewed as specifying a set of objects, and it is the union of those sets that
are the objects that can be read (for an "in") or written (for an "out") by the
given operation.

Initially we had considered the Global annotation items to simply be object
names.  But as the AI has evolved, we have come up with additional syntax to be
able to specify other sets of objects:

   <object_name> -- the named object, and all of its
                    subcomponents
   null          -- the empty set
   others        -- the universal set
   others in <pkg> -- all objects declared in <pkg>,
                    and all objects designated by
                    pool-specific access types declared in <pkg>
   access <type> -- all objects of the given type
                    that might be designated by an
                    access value
   <access_type> -- all objects that might be
                    designated by an access value
                    of the given pool-specific access type
   generic <formal_type> -- all objects specified in the
                    corresponding Global annotation
                    on the actual type corresponding
                    to the given formal type, representing
                    the global side-effects of the creation,
                    adjustment, or finalization of objects
                    of the given type.

For what its worth, Tuck has suggested the following specifications as possible
additions and/or replacements:

   new <type>    -- all (global) objects that might be side-affected
                    by the creation, adjustment, or finalization
                    of objects of the given type.  [This replaces and
                    generalizes "generic" so that it works
                    with any <type>, not just a generic formal
                    one.]

   <subprogram_name> -- all objects that might be affected
                    by calling the given subprogram.  This
                    may be of the form "acc-to-subp-param.all".
                    The subp name must not be overloaded [or
                    we union across all overloadings?].

   aliased <type> -- all objects of the given type that might
                    be designated by an access value.
                    [This would replace "access <type>".]

   <acc_type>.all -- all objects that might be designated
                    by an access value of the given pool-specific
                    access type.  [This would replace "<acc_type>".]

****************************************************************

From: Randy Brukardt
Sent: Thursday, February 4, 2010  9:00 PM

...
> Initially we had considered the Global annotation items to simply be
> object names.  But as the AI has evolved, we have come up with
> additional syntax to be able to specify other sets of objects:

Note that the AI evolved through writing examples.

>    generic <formal_type> -- all objects specified in the
>                     corresponding Global annotation
>                     on the actual type corresponding
>                     to the given formal type, representing
>                     the global side-effects of the creation,
>                     adjustment, or finalization of objects
>                     of the given type.

This also allows <formal_subprograms> and <formal_in_out_objects>. The need to
cover formal subprograms should be obvious (assume-the-worst on "=" passed in is
not good!). Formal in out objects are like renames, and thus they can reference
global objects. Interestingly, formal in objects (which are always copies) are
effectively local to the generic (from the perspective of inside the generic) as
they always are declared at the point of the instantiation. So they don't need
to be covered in an annotation.

> For what its worth, Tuck has suggested the following specifications as
> possible additions and/or replacements:
>
>    new <type>    -- all (global) objects that might be side-affected
>                     by the creation, adjustment, or finalization
>                     of objects of the given type.  [This replaces and
>                     generalizes "generic" so that it works
>                     with any <type>, not just a generic formal
>                     one.]

This only covers the <formal_type> use; you'll also need to cover the other two
uses.

>    <subprogram_name> -- all objects that might be affected
>                     by calling the given subprogram.  This
>                     may be of the form "acc-to-subp-param.all".
>                     The subp name must not be overloaded [or
>                     we union across all overloadings?].

I suppose you could cover formal subprograms here. Not overloaded will never
fly, the first thing I tried to write in a generic was "=". I concluded that no
solution I could think of would work - the union idea will often lead to using
(others): predefined "=" is usually (others) for private types. (I used full dot
notation in the example, but even that is ambiguous with the "=" for type
Vector.) I'm glad I've passed the torch on this AI to Bob...

>    aliased <type> -- all objects of the given type that might
>                     be designated by an access value.
>                     [This would replace "access <type>".]
>
>    <acc_type>.all -- all objects that might be designated
>                     by an access value of the given pool-specific
>                     access type.  [This would replace "<acc_type>".]

I don't like this syntax as it is ambiguous with object_name. That will
complicate resolution given that there is no key whether you are resolving for
"object of any type" or "subtype" (and these are very different). Since I've
raised this before and essentially been told that I don't know what I'm talking
about, I won't say any more. (But I'll swear like a sailor when I have to
implement it...)

Humm, actually, I do have to say more. Adding <subprogram_name> alone is even
worse: you'll have overlap between <object_name> and <subprogram_name> since a
parameterless <function_call> and a <function_name> are indistinguishable. I
suppose you could have some goofy preference rule to deal with that overlap
(<function_call> never being legal in this context), but that seems way over the
top to me.

Now I'll go away...

****************************************************************

From: Bob Duff
Sent: Wednesday, February 24, 2010  3:55 PM

> Bob volunteers to take this over.

Well, I don't have time to deal with the whole AI.

But one thing I was supposed to do is:

> Bob would like to be able to specify the that some subsystem has a
> default of Global in out => (null).
>
> That does seem useful. He asks whether it should allow any arbitrary
> annotation. Randy notes that the containers packages have many
> identical annotations; a way to avoid having to put them in every spec
> would be welcome. Bob will study this.

I'm ready to at least discuss this.

Seems like it should be an aspect of a (generic) package, and applies to all
subprograms therein.  What's the syntax for aspects of packages?

Something like this:

    with P;
    package Q is
        with Default_Global in => (P, Q),
             Default_Global out => (null);

        ...

    end Q;

Or:

    with P;
    package Q is

        ...

    end Q
        with Default_Global in => (P, Q),
             Default_Global out => (null);

****************************************************************

From: Randy Brukardt
Sent: Thursday, April 22, 2010  10:56 PM

After the discussion in Burlington on AI05-0186-1, I was tasked with looking at
simplifications for the model in order to retain the critical parts. Thinking
about this did not quickly lead to a clear solution, so I decided to write up my
thoughts in the form of a paper. I was hoping that would help crystallize my
ideas, and it did.

I've posted the finished paper in the grab bag of the Ada-Auth.org site:
http://www.ada-auth.org/ai-files/grab_bag/Expr-Cont.pdf
It's 10 pages long, but I don't think it is particularly difficult reading (it's
nothing like accessibility).

I entitled the paper "Preconditions, abstraction, and compile-time analysis",
but I could probably have used a number of different titles. "Preconditions"
really is a stand-in for all contracts in the form of an expression;
"compile-time analysis" is really a stand in for optimization and static
checking and even proof to some extent.

Anyway, we'll discuss the options at our subcommittee phone call next week;
hopefully at least subcommittee members will read it by then.

Comments and discussion are welcome of course. (I put a version number on the
paper so I can fix the inevitable errors.)

****************************************************************

From: Yannick Moy
Sent: Monday, April 26, 2010  1:04 AM

Thank you Randy for this very good explanation of the solutions and trade-offs.
I have understood a lot by reading it, and I'd like to share with you a
different view of the possible interaction between expression functions on one
side and global annotations on the other side.

You say the goal of contracts is to be able to decide if "the result of the
function is known to be the same for a given pair of calls", like the calls to
Some_Pre in the code below, both in precondition and in the body of
Do_Something.

procedure Do_Something (X : T) with Pre => Some_Pre (X);

procedure Do_Something (X : T) is
begin
  Do_Some_Preliminary_Things (X);
  if not Some_Pre (X) then
    raise Constraint_Error;
  end if;
  ...
end;

Not talking yet of concurrent accesses, there are two subprograms which control
here the answer to your question: the function Some_Pre which is called in a
contract, and the procedure Do_Some_Preliminary_Things which may invalidate this
contract. Thus, the compiler (or static analyzer) needs to know enough about the
behavior of each in order to answer your question. I think the same solution
does not necessarily apply to both.

I think that your proposed solution with expression functions deserves more than
to be "a reasonable fall-back option should no agreement be found on other
options". It could well be the best option to implement functions that are
called in contracts, like Some_Pre. Let's compare the benefits and drawbacks:

In the benefits column:
1) Straightforward to use. It is the most natural abstraction of the expressions
   that one would like to put in contracts.
2) Compile-time checked purity. Here, I'm using "purity" as in purely functional
   languages, as a synonym for no (writing) side-effects. It may still read any
   accessible piece of data, but ...
3) Compile-time known body. The compiler (or static analyzer) has access to the
   implementation of this expression function. Hence it can perform a host of
   analyzes that would not be possible otherwise, with great precision and no
   additional cost to the user in terms of annotations. This is related to ...
4) Part of specifications. Contracts should be part of specifications. They do
   not tell the "how" but the "what" to compute. They allow separate
   verification of code, which would not be possible if contracts depend on
   functions implemented in the body of packages.
5) Correspond to 99% of useful contracts. With the addition of if-expressions,
   case-expressions and quantified-expressions, all contracts on the library of
   containers in GNAT (which are presently implemented as assertions) could be
   expressed as expression functions.

In the drawbacks column:
1) Restricted to expressions. You cannot call a procedure or a function that is
   not an expression function. For example, the following precondition is not
   expressible: the sum of elements of array parameter A is less than integer
   parameter Max. (It could be expressed with lambda-expressions like in
   functional languages.) One should note here that such contracts are not very
   useful for analysis, as they are usually too complex to allow proving
   anything automatically. (Even the sum example above fits in this category!)
2) Not readily usable with existing functions. As you noted, this requires that
   some functions are rewritten as expression functions. This seems like a small
   price to pay when switching to contracts and contract-based analysis.

So what about procedure Do_Some_Preliminary_Things? Here, the annotations for
writing global objects are the best possible solution. They should make it
possible to know if the expression designated by "Some_Pre (X)" is modified by
calling Do_Some_Preliminary_Things.

If you agree with this separation of concerns, then probably the focus of global
annotations should change. In particular, this would not be true to say that
"the current primary purpose of the annotations is to support precondition
contracts".

Some benefit of this separation is that the expression functions are readily
understood and usable by Ada programmers, while global annotations provide an
additional benefit for those who will take the time to understand them.

Although I'm in favor of a way to express the "frame condition" of a subprogram,
I'll leave this discussion for now, to separate concerns. :)

****************************************************************

Questions? Ask the ACAA Technical Agent