CVS difference for ai12s/ai12-0079-1.txt

Differences between 1.5 and version 1.6
Log of other versions for file ai12s/ai12-0079-1.txt

--- ai12s/ai12-0079-1.txt	2014/11/13 04:00:55	1.5
+++ ai12s/ai12-0079-1.txt	2015/06/18 05:51:34	1.6
@@ -1,4 +1,4 @@
-!standard 7.3.2(3/3)                                13-10-13    AI12-0079-1/01
+!standard 6.1.2(0)                                  15-06-17    AI12-0079-1/02
 !class Amendment 13-06-28
 !status work item 13-06-28
 !status received 13-06-14
@@ -19,9 +19,9 @@
 
 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.
+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.
 
@@ -55,41 +55,41 @@
 
   with Global => (Input => ...,
                   In_Out => ..., Output => ...)
-                 
-where “...” is either a single name, or a parenthesized list of names, and
+
+where "..." is either a single name, or a parenthesized list of names, and
 Input, In_Out, and Output identify the variables global to the
 subprogram that are accessed by this subprogram, in read-only,
 read-write, or write-only mode, respectively. If there are no variables
 global to the subprogram accessed with a particular parameter mode, then
 that mode is omitted from the specification. If there are only global
 inputs, and no outputs or in-outs, then this syntax can be further
-simplified to: 
+simplified to:
 
-  with Global => ...
+   with Global => ...
 
 where again "..." is a single name, or a parenthesized list of names.
 
 Finally, if there are no global inputs, in-outs, nor outputs, then:
+
+   with Global => null
 
-  with Global => null
-  
 is used.
 
 We need to refine the notion of SPARK's Global aspect, because SPARK
 does not support access types, and because SPARK relies on an elaborate
-mechanism for handling the abstract “state” of packages.  The
+mechanism for handling the abstract "state" of packages.  The
 refinements we are proposing are the following:
 
 1.	Allow the name of an access type A (including "access T") to
-stand-in for the set of objects described roughly by: 
+stand-in for the set of objects described roughly by:
 
-   (for all X convertible to A => X.all)
-   
+    (for all X convertible to A => X.all)
+
 2.	Allow the name of a package P to stand-in for the set of objects
-described roughly by: 
+described roughly by:
+
+    (for all variables X declared in P => X)
 
-   (for all variables X declared in P => X)
-   
 3.	Allow the word *synchronized* to be used to represent the set of
 global variables that are tasks, protected objects, or atomic objects.
 
@@ -117,8 +117,114 @@
 
 !wording
 
-** TBD.
+Add the following section:
+
+6.1.2 The Global and Global'Class Aspects
 
+For a noninstance subprogram, a generic subprogram, an entry, a package,
+or a generic package, the following language-defined aspect may be
+specified with an aspect_specification (see 13.1.1):
+
+Global
+
+   The syntax for the aspect_definition used to define a Global aspect
+   is as follows:
+
+    global_aspect_definition ::=
+      global_set |
+      (global_mode => global_set {, global_mode => global_set})
+
+    global_mode ::= Input | In_Out | Output
+
+    global_set ::= global_name |
+       (global_name, global_name{, global_name}) | ALL | SYNCHRONIZED | NULL
+
+    global_name ::= variable_name | package_name | access_subtype_mark
+
+   This aspect specifies the set of variables global to a callable entity
+   that are potentially read or updated as part of the execution of a
+   call on the entity. If not specified, the aspect defaults to the
+   Global aspect for the nearest enclosing package or generic package.
+   If not specified for a library package or generic package, the aspect
+   defaults to "Global => null" for a library package or generic package
+   that is declared Pure, and to "Global => (In_Out => all)" otherwise.
+
+For a dispatching subprogram, a package, or a generic package, the
+following language-defined aspect may be specified with an
+aspect_specification (see 13.1.1):
+
+Global'Class
+
+   The syntax for the aspect_definition used to define a Global'Class
+   aspect is the same as that defined above for global_aspect_definition.
+   This aspect specifies an upper bound on the set of variables global to a
+   dispatching operation that can be read or updated as a result of a
+   dispatching call on the operation. If not specified, the aspect
+   defaults to the Global'Class aspect for the nearest enclosing package
+   or generic package.  If not specified for a library package or generic
+   package, the aspect defaults to "Global'Class => null" for a library
+   package or generic package that is declared Pure, and to "Global'Class
+   => (In_Out => all)" otherwise.
+
+    Name Resolution Rules
+
+A global_name shall statically denote a variable, a package, or an
+access-to-variable subtype that is visible at the point of the aspect
+specification.
+
+    Static Semantics
+
+A global_aspect_definition defines the set of global variables that can
+be read or written by a callable entity. The form of
+global_aspect_definition comprising only "global_set" is equivalent to
+"(Input => global_set)".  If a given global_mode does not appear in a
+given global_aspect_definition, it is as though the aspect definition
+included "global_mode => null".  The Input and In_Out global_modes
+together identify the set of global variables than can be read by the
+callable entity.  The In_Out and Output global_modes together identify
+the set of global variables that can be updated by the callable entity.
+
+A global_set identifies a *global variable set* as follows:
+
+   * "null" identifies the empty set of global variables;
+   * "all" identifies the set of all global variables;
+   * "synchronized" identifies the set of all global variables that are
+     either of a protected type, a task type, an atomic type, or a record
+     or array all of whose components are "synchronized" in this sense;
+   * (global_name, global_name{, global_name}) identifies the union of the
+     sets of variables identified by the individual global_name's.
+   * for the three forms of global_name:
+
+     * variable_name identifies the specified global variable;
+     * package_name identifies the set of all variables declared within
+       the package of the same accessibility level as the package;
+     * access_subtype_mark identifies the set of objects that can be designated
+       by values of the given access-to-variable type;
+
+    Legality Rules
+
+Within a global_aspect_definition, a given global_mode shall be
+specified at most once. Similarly, within a global_aspect_definition, a
+given entity shall be named at most once by a global_name, and the
+reserved words ALL and SYNCHRONIZED shall appear at most once.
+
+If a callable entity has a Global aspect other than (In_Out => all),
+then it shall read only those variables global to the entity that are
+within the *global variable set* identified by either the Input or
+In_Out global_modes, and it shall update only those variables global to
+the entity that are within the *global variable set* identified by
+either the In_Out or Output global_modes. This includes any calls within
+the body of the callable entity, presuming those calls read and update
+all global variables permitted by their Global aspect (or Global'Class
+aspect, if a dispatching call).
+
+For a subprogram that is a dispatching operation of a tagged type T, the
+Input and In_Out modes of its Global aspect shall identify a subset of
+the variables identified by the Input and In_Out modes of the
+Global'Class aspect of a corresponding dispatching subprogram of any
+ancestor of T. Similarly, the In_Out and Output modes of its Global
+aspect shall identify a subset of the variables identified by the In_Out
+and Output modes of such Global'Class aspects.
 
 !discussion
 
@@ -153,15 +259,15 @@
 
 !example
 
-  package Random is
-    procedure Set_Seed(Seed : Float);
-       with Global => (Out => Random);
-         --  Initialize state of Random package
-         
-    function Next_Random return Float
-       with Global => (In_Out => Random);
-         --  Update state of Random package
-  end Random;
+   package Random is
+     procedure Set_Seed(Seed : Float);
+        with Global => (Out => Random);
+          --  Initialize state of Random package
+
+     function Next_Random return Float
+        with Global => (In_Out => Random);
+          --  Update state of Random package
+   end Random;
 
 !ASIS
 
@@ -328,7 +434,7 @@
 From: Bob Duff
 Sent: Tuesday, October 14, 2014  5:20 PM
 
-> Here is an AI on the Global aspect, based on SPARK and on the HILT 
+> Here is an AI on the Global aspect, based on SPARK and on the HILT
 > 2014 paper on parallel language extensions for Ada.
 
 Looks good.  You make it look so simple.  So why didn't we already do this?
@@ -337,42 +443,42 @@
 See below for editorial comments and some questions.
 
 > !summary
-> 
+>
 > Annotations are provided to describe the use of global objects by subprograms.
                                                          ^^^^^^^
 
 variables
 
 > !problem
-> 
-> Ada 2012 added many kinds of assertions to Ada 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 
+>
+> Ada 2012 added many kinds of assertions to Ada 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 
+>
+> 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
                                                         ^^^^^^^^^ subprograms
 
-> the result of a function can change even when called with the same 
-> operands. Other assumptions could cause incorrect programs to be 
+> 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.
                            ^^^^          ^^^^^^^
 
 I think you mean "suppress...checks".  If not, please explain.
 
-> Both of these results are unacceptable for a feature intended to 
+> 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 
+>
+> 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).
 
@@ -382,8 +488,8 @@
 (i.e. specs).  If you prove something about package body X, you want that proof
 to be valid in the presence of arbitrary changes to bodies called by X.
 
-> We need to refine the notion of SPARK's Global aspect, because SPARK 
-> does not support access types, and because SPARK relies on an 
+> We need to refine the notion of SPARK's Global aspect, because SPARK
+> does not support access types, and because SPARK relies on an
 > elaborate mechanism for handling the abstract “state” of packages.
 
 What's your opinion about that elaborate mechanism?  I've never understood why
@@ -392,9 +498,9 @@
 
 >...The
 > refinements we are proposing are the following:
-> 
+>
 > 1.	Allow the name of an access type A (including "access T") to
-> stand-in for the set of objects described roughly by: 
+> stand-in for the set of objects described roughly by:
 
 "stand in" (no dash)
 
@@ -403,44 +509,44 @@
 That's the same thing as the collection of A, right?
 
 > 2.	Allow the name of a package P to stand-in for the set of objects
-> described roughly by: 
-> 
+> described roughly by:
+>
 >    (for all variables X declared in P => X)
 
 Does that include children of P?
 
 > !wording
-> 
+>
 > ** TBD.
 
 ;-)  ;-)
 
 > !discussion
-> 
-> Global annotations are critical to being able to perform any sort of 
+>
+> Global annotations are critical to being able to perform any sort of
 > modular static analysis.
 
 Yeah, that's what I meant by my "software engineering" comment above.
 
-> All of the global in, in-out, and out annotations proposed can be 
+> All of the global in, in-out, and out annotations proposed can be
 > statically checked.
-> 
-> 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). 
+>
+> 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.
-> 
-> SPARK does not currently support identifying particular components of 
+>
+> SPARK does not currently support identifying particular components of
 > a global variable in the Global aspect, but for Ada we plan to allow that.
-> This is somewhat inconsistent with what can be specified for 
-> parameters, since there is no easy way to identify which components of 
-> an in-out parameter are actually updated. It is possible to specify in 
-> a postcondition that X.C = X.C'Old and X.D = X.D'Old and ... but that 
-> can be a maintenance issue as the names and numbers of subcomponents 
+> This is somewhat inconsistent with what can be specified for
+> parameters, since there is no easy way to identify which components of
+> an in-out parameter are actually updated. It is possible to specify in
+> a postcondition that X.C = X.C'Old and X.D = X.D'Old and ... but that
+> can be a maintenance issue as the names and numbers of subcomponents
 > changes, and only works for types that have an appropriate "=" operator.
-> It might be useful to have another aspect that indicated which 
-> components of an in-out parameter might be updated, with all others 
+> It might be useful to have another aspect that indicated which
+> components of an in-out parameter might be updated, with all others
 > presumably being preserved (e.g. Updated => (X.A, X.B)).
 
 Yes, I'm a fan of limited types, and I'd like to be able to say things like
@@ -452,14 +558,14 @@
 Sent: Tuesday, October 14, 2014  9:37 PM
 
 ...
->> However, without knowledge of side-effects of functions used in the 
->> aspects, a tool has to assume the worst about any user-defined 
+>> 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
->                                                          ^^^^^^^^^ 
+>                                                          ^^^^^^^^^
 > subprograms
 >
->> the result of a function can change even when called with the same 
->> operands. Other assumptions could cause incorrect programs to be 
+>> 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.
 >                             ^^^^          ^^^^^^^
 >
@@ -468,37 +574,37 @@
 I didn't actually write the "problem" statement.  I think it might be Randy's original wording.
 
 
->> Both of these results are unacceptable for a feature intended to 
+>> 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 
+>> 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).
 >
-> I agree, having to look at bodies is "bad", but those don't seem like 
-> the main reasons why.  To me, the main reason is the usual software 
-> engineering one: you want well-defined interfaces, and you want to 
-> depend ONLY on those interfaces (i.e. specs).  If you prove something 
-> about package body X, you want that proof to be valid in the presence 
+> I agree, having to look at bodies is "bad", but those don't seem like
+> the main reasons why.  To me, the main reason is the usual software
+> engineering one: you want well-defined interfaces, and you want to
+> depend ONLY on those interfaces (i.e. specs).  If you prove something
+> about package body X, you want that proof to be valid in the presence
 > of arbitrary changes to bodies called by X.
 
 Agreed.  Again, this problem statement was from an earlier version of the AI.
 It seemed adequate to capture the problem, but it could perhaps use some
 wordsmithing.
 
->> We need to refine the notion of SPARK's Global aspect, because SPARK 
->> does not support access types, and because SPARK relies on an 
+>> We need to refine the notion of SPARK's Global aspect, because SPARK
+>> does not support access types, and because SPARK relies on an
 >> elaborate mechanism for handling the abstract “state” of packages.
 >
-> What's your opinion about that elaborate mechanism?  I've never 
-> understood why it's needed, but I'm told by SPARK folks that it's 
-> super-useful.  I'd like to understand why, and whether we ought to add 
+> What's your opinion about that elaborate mechanism?  I've never
+> understood why it's needed, but I'm told by SPARK folks that it's
+> super-useful.  I'd like to understand why, and whether we ought to add
 > such stuff to Ada.
 
 The elaborate mechanism is needed if you make heavy use of global variables.
@@ -542,11 +648,11 @@
 public children, as you could name them separately.
 
 >> ...
->> It might be useful to have another aspect that indicated which 
->> components of an in-out parameter might be updated, with all others 
+>> It might be useful to have another aspect that indicated which
+>> components of an in-out parameter might be updated, with all others
 >> presumably being preserved (e.g. Updated => (X.A, X.B)).
 >
-> Yes, I'm a fan of limited types, and I'd like to be able to say things 
+> Yes, I'm a fan of limited types, and I'd like to be able to say things
 > like that.
 
 If we adopt something like "Updated" then it might make sense to keep Global
@@ -560,8 +666,8 @@
 
 > > Here is an AI on the Global aspect, based on SPARK and on the HILT
 > > 2014 paper on parallel language extensions for Ada.
-> 
-> Looks good.  You make it look so simple.  So why didn't we already do 
+>
+> Looks good.  You make it look so simple.  So why didn't we already do
 > this?  I guess the Devil's in the "!wording".
 
 Mostly FUD, really. You and I spent a lot of hours creating AI05-0186-1,
@@ -575,5 +681,66 @@
 Unfortunately, most of the work will have to be redone; hopefully Tucker et.
 al. will be able to use some of the wording created for AI05-0186-1 so the
 effort won't totally go to waste.
+
+****************************************************************
+
+From: Tucker Taft
+Sent: Wednesday, June 17, 2015  8:39 AM
+
+Here is a first attempt at wording for the Global/Global'Class aspects.
+[This is version /02 of the AI - Editor.]
+
+****************************************************************
+
+From: Randy Brukardt
+Sent: Thursday, June 18, 2015 12:47 AM
+
+> Here is a first attempt at wording for the Global/Global'Class
+> aspects.
+...
+> If a callable entity has a Global aspect other than (In_Out => all),
+> then it shall read only those variables global to the entity that are
+> within the *global variable set* identified by either the Input or
+> In_Out global_modes, and it shall update only those variables global
+> to the entity that are within the *global variable set* identified by
+> either the In_Out or Output global_modes. This includes any calls
+> within the body of the callable entity, presuming those calls read and
+> update all global variables permitted by their Global aspect (or
+> Global'Class aspect, if a dispatching call).
+
+I find this rather simplistic, since it seems to require the reader and the
+compiler to look through a near-infinite set of possible global variables
+(especially in the call case). Perhaps there is a better way to describe this
+without requiring that (perhaps some type of matching).
+
+I had thought that the term "global" was undefined in Ada, but it actually is
+defined in 8.1. Who knew? (I've been using it in an English sense forever.)
+
+---
+
+As with nonbounded, there doesn't seem anything for formal subprograms. I don't
+think there is any way to write a container package with these annotations
+unless there is some way to control the actual subprograms and/or export the
+same annotations on the routines that call the formal subprograms. The
+annotations are next to useless if you can't write a generic container using
+them (and preferably, they'll work with the existing containers).
+
+---
+
+There clearly has to be some rules for predefined operations. Most of them
+should have global => null, but beware of record equality, which can incorporate
+user-defined "=". I never figured out a good way to handle that (requiring
+global => null on those as well would have been great, but it's at least 35
+years too late for that).
+
+---
+
+The entire predefined library needs to be decorated. In the old AI, I proposed
+doing that by having some defaults for pure library units (which shouldn't have
+any global state), but we'd still want to manually do it for the containers and
+possibly other useful packages (probably not for the I/O packages). Perhaps that
+should be a separate AI or AIs due to the size.
+
+Enough comments for tonight.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent