!standard 6.1.2(12/5) 19-05-09 AI12-0303-1/03 !standard 6.1.2(32/5) !standard 6.1.2(46/5) !class Amendment 19-01-10 !status work item 19-01-10 !status received 19-01-10 !priority Medium !difficulty Easy !subject Some constants must be covered by Global aspects; extensibility !summary Constants that have parts of types that might be inherently mutable (see 3.3) have to be included in the Global aspects for entities as if they were variables. We permit extension of the Global aspect to accommodate more advanced formal methods (such as SPARK). !problem AI12-0079-1 only requires reads and updates of global variables to be reported in the Global aspect for a subprogram. However, Ada declares certain constants "inherently mutable" because it is possible to squirrel away access-to-variable values when they are created. Later, the constant can be modified via copies of the squirrelled access-to-variable; such routines may not appear to modify the constant (for instance, it is not necessary to pass the constant as a parameter to trigger such uses). Such constants have to be included the Global for subprograms that read them, lest routines that depend on them appear to avoid dependence on state when in fact their results depend on more than their parameters. For example: with Ada.Finalization; package ADT is type Object_Type (<>) is tagged limited private with Global => in out access Object_Type; -- all would be OK, too. function Get_Data (Obj : in Object_Type) return Natural with Global => null; function New_Object (Start : in Natural) return Object_Type with Global => Object_Type'Global; procedure Bump_Em_All with Global => Object_Type'Global; private type Object_Access is access all Object_Type; type Object_Type is new Ada.Finalization.Limited_Controlled is record Next_Sibling : Object_Access; Data : Natural; end record; overriding procedure Initialize (Obj : in out Object_Type) with Global => Object_Type'Global; overriding procedure Finalize (Obj : in out Object_Type) with Global => Object_Type'Global; end ADT; package body ADT is All_Object_Root : Object_Access := null; function Get_Data (Obj : in Object_Type) return Natural with Global => null is begin return Obj.Data; end Get_Data; -- Global => null has to be OK here (and I believe it is), we're -- reading a by-copy component of the parameter without any -- dereference. There's no possible side effects here. function New_Object (Start : in Natural) return Object_Type is -- This function has to be built-in-place. begin return Result : Object_Type do -- Calls Initialize. Result.Data := Start; end return; end New_Object; procedure Bump_Em_All is Walker : Object_Type := All_Object_Root; begin while Walker /= null loop Walker.Data := @ + 1; Walker := Walker.Next_Sibling; end loop; end Bump_Em_All; procedure Initialize (Obj : in out Object_Type) is begin Obj.Data := Start; Obj.Next_Sibling := All_Object_Root; All_Object_Root := Obj'Unchecked_Access; end Initialize; procedure Finalize (Obj : in out Object_Type) is begin -- Remove Obj from the list rooted by All_Object_Root; -- left for an exercise for the reader. end Finalize; end ADT; This ADT keeps a list of all of the objects of the type, so it can do some global operations on them as needed. with ADT; package Trouble is Fooey : constant ADT.Object_Type := ADT.New_Object (4); function Evil (A : Natural) return Natural with Global => null; end Trouble; package body Trouble is function Evil (A : Natural) return Natural is begin return Fooey.Get_Data + A; -- OK by AI12-0079-1, will be -- illegal by this AI. end Evil; -- Global => null is OK here, as both "+" and Get_Data are Global => null. end Trouble; with ADT, Trouble; procedure Main is V1, V2 : Natural; begin V1 := Evil (12); -- V1 = 16. ADT.Bump_Em_All; V2 := Evil (12); -- V2 = 17. end Main; Evil is a function with no global references and that isn't erroneous, and still manages to get a different result for the same parameters. As a further concern, the SPARK 2014 language includes the Global aspect, but has additional kinds of entities (such as, abstract state) which are relevant. The SPARK Global aspect also worries about constants whose initial value depends on variables. !proposal Require inclusion of constants with inherently mutable parts in Global contracts. In order to avoid breaking privacy, we have to assume that any private type or private extension might have such a part. We also allow any constant to be given in a Global contract; this can help with maintenance (future changes won't change the needed contract) and also helps compatibility with SPARK (which requires constants in Global contracts in some, different from Ada, circumstances). Finally, we provide an implementation permission to extend the syntax of the Global aspect more generally, to accommodate SPARK and future experimentation with more advanced formal methods. !wording [Editor's note: The paragraph numbers here are from draft 19 of the RM.] Replace the following wording from RM 6.1.2(12/5): The Global aspect identifies the set of variables (which, for the purposes of this clause includes all task objects) 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 program unit. If not specified for a library unit, the aspect defaults to "Global => null" for a nongeneric library unit that is declared Pure, and to "Global => in out all" otherwise. with: The Global aspect identifies the set of variables (which, for the purposes of this clause includes all constants with some part being immutably limited, or of a controlled type, private type, or private extension) global to a callable entity that are potentially read or updated as part of the execution of a call on the entity. Constants of any type may also be mentioned in a Global aspect. If not specified, the aspect defaults to the Global aspect for the nearest enclosing program unit. If not specified for a library unit, the aspect defaults to "Global => null" for a nongeneric library unit that is declared Pure, and to "Global => in out all" otherwise. Modify the following bullet from 6.1.2(32/5): * /object_/name identifies the specified global variable (or [nonpreelaborable] constant) [Editor's note: So this doesn't conflict with the "may be mentioned" rule.] Add after 6.1.2(46/5) the additional permission: Implementations may extend the syntax or semantics of the Global aspect in an implementation-defined manner. !discussion We attempted to find a restriction on private types covered by this rule based on the Global contract of the private. Usually, the Global contract of Initialize has to include some global in which to do the squirreling. This contract has to be included in the Global contract of the private type, so this cannot be hidden. However, if Initialize squirrels the access into the object itself, no Global contract would be required. That would also be the case for the self-pointers that can be constructed in an immutably limited type. Thus, in order to avoid privacy breaking, we have to include all private types in this requirement. Even with this rule, objects that can never be a problem (like a scalar constant) do not need to be mentioned in a Global aspect. To support SPARK 2014 and other more advanced formal methods tools, we allow any constant to be mentioned in a Global aspect, and we go further to allow any sort of implementation-defined extension to the syntax. This is consistent with the general permission to allow implementation-defined syntax for aspect specifications (see 13.1.1(38/3)). We don't want to lose that flexibility just because we decide to standardize some Global aspect capabilities. !corrigendum 6.1.2(0) @dinsc Just enough to force a conflict; the real text is found in the conflict file. !ASIS No ASIS effect from these changes (the original changes should cover this). !ACATS test ACATS B- and C-Tests are needed to check that the newly required items are covered by Global specifications. !appendix From: Tucker Taft Sent: Wednesday, January 9, 2019 2:30 PM I suggest we indicate on this early use of the term "variable" the following: The Global aspect identifies the set of variables (which for the purposes of this clause includes all inherently mutable objects -- see 3.3) global to a callable entity that are potentially read or updated as part of the execution of a call on the entity. Randy, does that solve the problem? **************************************************************** From: Randy Brukardt Sent: Wednesday, January 9, 2019 2:55 PM > Randy, does that solve the problem? Sort of. The remaining problem is that determining whether an object is "inherently mutable" requires breaking privacy (sometimes). I had suggested that we treat all limited private types and all non-limited private types with non-null Globals as "inherently mutable", as that seems to avoid the need to break privacy to see whether there are any controlled or immutably limited parts. For the nonlimited private case, if the type has a null Global, then any Initialize/Adjust/Finalize routines cannot squirrel any access values to the object (as that would have to be reflected in their Globals, and thus the Global of the type), and thus there cannot be any back-channel modifications, even if controlled types are involved. This does assume that the Global of a type has to include the Globals of all of the types of its components, but I don't see how it could work otherwise. The main problem with this is that most types will (initially, at least) default to Global => all, so most user-defined constants would have to be included. I know we discussed other options for this, but I don't recall any others that worked. I know we don't want to make all private constants be mentioned this way. **************************************************************** From: Tucker Taft Sent: Wednesday, January 9, 2019 3:26 PM Perhaps we should take a different route. The question is whether there is a visible operation on the type which takes an IN parameter of the type, and nevertheless can update the state "associated with" the parameter. With the notion of ownership, that state might be part of the object itself (by using the Rosen trick), or it might be pointed-to. If we don't have ownership, then the only way to have a side-effect is via an access value, in which case you would have to report "access T" in the Global aspect (even if you used the Rosen trick), which avoids the problem. So this problem is really only important once we have ownership, which will allow the programmer to *not* report a side-effect via "access T." If we use ownership with random number Generators and File_Types, then we will want to be able to write, for example, "Global => in out My_File" even though My_File is a global constant. And anyone using the Rosen trick will need to use ownership to avoid having to use "access T," and have an operation that somehow communicates the update being performed on the "owned" state, even when the parameter is an IN parameter. That brings back up the "Modifies" aspect that we have been discussing privately, or the ability to pervert the Global aspect a bit to report an update to state owned by an IN parameter. If we presume we will eventually have ownership, then I think we can use the notion mentioned above, namely that "a variable includes any object of a type with of a visible operation that takes an IN parameter of the type, and nevertheless can update the state owned by the parameter." Perhaps that change ought to be part of the forthcoming Nth version of the ownership AI, rather than trying to fix it here. Without ownership, I don't see a problem, due to the requirement to specify "access T" to capture Rosen-trick side-effects. **************************************************************** From: Randy Brukardt Sent: Wednesday, January 9, 2019 3:50 PM The problem is that the "access T" is on Initialize and potentially some other operations, and not on those that are merely reading the inherently mutable constant. This lets a pure function (that is, Global => null) depend on variable state. I wrote up a complete example (complete with a mistake) in private mail last month. It doesn't use any ownership, and definitely has a problem. --------------- (From private mail of December 10th). Consider the following packages, based on the Claw design (disclaimer, I didn't try to compile this, so it is probably full of syntax errors :-): with Ada.Finalization; package ADT is type Object_Type (<>) is tagged limited private with Global => in out access Object_Type; -- all would be OK, too. function Get_Data (Obj : in Object_Type) return Natural with Global => null; function New_Object (Start : in Natural) return Object_Type with Global => Object_Type'Global; procedure Bump_Em_All with Global => Object_Type'Global; private type Object_Access is access all Object_Type; type Object_Type is new Ada.Finalization.Limited_Controlled is record Next_Sibling : Object_Access; Data : Natural; end record; overriding procedure Initialize (Obj : in out Object_Type) with Global => Object_Type'Global; overriding procedure Finalize (Obj : in out Object_Type) with Global => Object_Type'Global; end ADT; package body ADT is All_Object_Root : Object_Access := null; function Get_Data (Obj : in Object_Type) return Natural with Global => null is begin return Obj.Data; end Get_Data; -- Global => null has to be OK here (and I believe it is), we're -- reading a by-copy component of the parameter without any -- dereference. There's no possible side effects here. function New_Object (Start : in Natural) return Object_Type is -- This function has to be built-in-place. begin return Result : Object_Type do -- Calls Initialize. Result.Data := Start; end return; end New_Object; procedure Bump_Em_All is Walker : Object_Type := All_Object_Root; begin while Walker /= null loop Walker.Data := @ + 1; Walker := Walker.Next_Sibling; end loop; end Bump_Em_All; procedure Initialize (Obj : in out Object_Type) is begin Obj.Data := Start; Obj.Next_Sibling := All_Object_Root; All_Object_Root := Obj'Unchecked_Access; end Initialize; procedure Finalize (Obj : in out Object_Type) is begin -- Remove Obj from the list rooted by All_Object_Root; -- left for an exercise for the reader. end Finalize; end ADT; Essentially, this ADT keeps a list of all of the objects of the type, so it can do some global operations on them as needed. This is how Claw works (it avoids this problem by not providing a creation functions [they didn't work on Ada 95], and the creation procedures all take in out parameters, so a stand-alone constant can never represent anything except an invalid object). with ADT; package Trouble is Fooey : constant ADT.Object_Type := ADT.New_Object (4); function Evil (A : Natural) return Natural with Global => null; end Trouble; package body Trouble is function Evil (A : Natural) return Natural is begin return Fooey.Get_Data + A; end Evil; -- Global => null is OK here, as both "+" and Get_Data are Global => null. end Trouble; with ADT, Trouble; procedure Main is V1, V2 : Natural; begin V1 := Evil (12); -- V1 = 16. ADT.Bump_Em_All; V2 := Evil (12); -- V2 = 17. end Main; So Evil is a function with no global references and that isn't erroneous, and still manages to get a different result for the same parameters. Which blows up the pure permission (it shouldn't be done in this sort of case). It could make trouble for parallel block checks (imagine a block where one branch calls Evil and the other branch calls Bump_Em_All). And so on. ----- (End example of December 10th.) The problem here is that Get_Data doesn't need to mention the access component in its Global contract because it doesn't use it. (And that seems fundamental to the model of Global). But some other routine can use the access component to modify the components that Get_Data *does* use. Thus the Fooey "constant" needs to be represented in the Global aspect for Fooey. The key here seems to be that the private type's Global is not null and cannot be null, in which case there is a possibility that is squirrels access objects (as this example does). In that case, we have to assume-the-worst are require the constant to be covered by Global. Unless you can figure out some better rule. **************************************************************** From: Tucker Taft Sent: Wednesday, January 9, 2019 5:36 PM > The problem is that the "access T" is on Initialize and potentially > some other operations, and not on those that are merely reading the > inherently mutable constant. This lets a pure function (that is, > Global => null) depend on variable state. > I wrote up a complete example (complete with a mistake) in private > mail last month. It doesn't use any ownership, and definitely has a > problem. ... Clearly the Global aspect of Bump_Em_All has to imply that it is changing Fooey, even though Fooey is a declared constant. Clearly Evil is reading Fooey. So the question is, what makes us have to report reads of Fooey? I was claiming the presence of a visible operation that takes an IN parameter and nevertheless updates the state associated with the object. But here the problem is that we have a global access-to-variable pointer, pointing (indirectly) to the constant object, with this pointer being created during Initialization. So without taking Fooey as any sort of parameter, Bump_Em_All can update it. Clearly Bump_Em_All needs to report "Global => in out access Object_Type" (it doesn't do so in your example, which seems like a bug). Now the question is why we need to have Evil report it is reading Fooey, and how we know Fooey can be designated by an access value. The Initialize operation works on constants, so that makes it like an operation that has an IN parameter but updates the associated state. But it also sticks an access-to-variable pointer to the object into a global place. That is what needs to be captured somehow, which will trigger a requirement to treat constants of the type like (aliased) variables. And of course the Initialize operation need not be visible, so a Global aspect on the Initialize operation doesn't prove much. So it seems we need something on the type, and your suggestion of a non-null Global on the type seems as good as any. The Rosen trick (sorry JP to keep calling it that) doesn't immediately create a problem, because to use it you would need to dereference the pointer. However, suppose you call an operation later that merely copies the pointer generated during Initialize into a global place. Or for that matter, without doing anything during Initialize, what prevents a procedure from squirreling away a pointer to an in-out parameter of a tagged type using 'Unchecked_Access at any time? That would only work on a variable, but we somehow need to know that the variable can now be designated by an access value. That property itself isn't always visible. I guess we have to assume the worst for private types, as far as the possibility that they can be designated by an access value. Clearly an update via a pointer of a general access type will destroy much of the known universe, for the purposes of Global. We might as well accept that. This makes some kind of ownership all the more important, and encourages the use of pool-specific access types. I think we should probably go for an assume-the-worst, and say that any global constant or variable of a private type must be assumed to be alterable by an assignment through a pointer of a general access type (i.e. "in out access T" in the Global aspect), given the possibility of a Rosen trick applied during Initialize, and then a later copying of the access-to-variable value into a global. So.... The wording should now be: I suggest we indicate on this early use of the term "variable" the following: The Global aspect identifies the set of variables (which for the purposes of this clause includes all constants with at least some part being of a private type or private extension) global to a callable entity that are potentially read or updated as part of the execution of a call on the entity. I think we might want to also add: {Constants of any type may also be mentioned in a Global aspect.} There seems no harm, and that way the programmer doesn't have to worry about maintenance issues when a type suddenly has a private component added or removed. Also, SPARK requires certain constants-initialized-by-variables to be mentioned, so this would allow them to do so without violating the Ada rules. **************************************************************** From: Randy Brukardt Sent: Wednesday, January 9, 2019 6:14 PM ... > Clearly Bump_Em_All needs to report "Global => in out access > Object_Type" (it doesn't do so in your example, which seems like a > bug). Bump_Em_All has a Global of "Object_Type'Global", and the Global of Object_Type is "in out access Object_Type". So I don't see any bug here. > Now the question is why we need to have Evil report it is reading > Fooey, and how we know Fooey can be designated by an access value. > > The Initialize operation works on constants, so that makes it like an > operation that has an IN parameter but updates the associated state. > But it also sticks an access-to-variable pointer to the object into a > global place. That is what needs to be captured somehow, It *is* captured, in the Global of the type Object_Type. That has to cover any Globals of Initialize/Finalize/Adjust. > ... which will trigger a > requirement to treat constants of the type like (aliased) variables. > And of course the Initialize operation need not be visible, so a > Global aspect on the Initialize operation doesn't prove much. So it > seems we need something on the type, and your suggestion of a non-null > Global on the type seems as good as any. > > The Rosen trick (sorry JP to keep calling it that) doesn't immediately > create a problem, because to use it you would need to dereference the > pointer. However, suppose you call an operation later that merely > copies the pointer generated during Initialize into a global place. > Or for that matter, without doing anything during Initialize, what > prevents a procedure from squirreling away a pointer to an in-out > parameter of a tagged type using 'Unchecked_Access at any time? That > would only work on a variable, but we somehow need to know that the > variable can now be designated by an access value. That property > itself isn't always visible. I guess we have to assume the worst for > private types, as far as the possibility that they can be designated > by an access value. The ability to be designated by an access is a property of an object ("aliased") not of a type, other than parameters of a tagged type. So I'm not sure there is much to be gained here by worrying about that -- I would tend to say any type can be designated by an access type. The only way to disprove that is to determine that there are no such types dereferenced anywhere (which you can see, sort of, but that of course assumes no one uses "all" or package names in Global). The problem comes when you can get access-to-variable for a constant, so I've mainly be worrying about those cases. > Clearly an update via a pointer of a general access type will destroy > much of the known universe, for the purposes of Global. We might as > well accept that. This makes some kind of ownership all the more > important, and encourages the use of pool-specific access types. Yes. In a parallel universe, I've been struggling with some problems caused by that assumption in our optimizer. The optimizer has to be conservative, so there isn't really any other choice. (In my case, the question is whether to delay the compiler release that's already months late to try to get additional info into the optimizer so it can make better decisions about local objects at least. As it stands, every indirect reference looks like every other, so assume-the-worst is the only choice, which leads nowhere.) > I think we should probably go for an assume-the-worst, and say that > any global constant or variable of a private type must be assumed to > be alterable by an assignment through a pointer of a general access > type (i.e. "in out access T" in the Global aspect), given the > possibility of a Rosen trick applied during Initialize, and then a > later copying of the access-to-variable value into a global. I don't see the problem in the case of constants unless it's possible for an access-to-variable to be created. If only an access-to-constant can be created, it's hard to alter the object. :-) And we assume implicitly that all variables can be modified (and at all times, I think; a Modified aspect would help bound that at a bit, but the default has to be that they can be modified through a parameter of any mode), so I don't quite see what the fact that they can be designated by access-to-variable matters. > So.... > > The wording should now be: > > I suggest we indicate on this early use of the term "variable" the > following: > > The Global aspect identifies the set of variables > (which for the purposes of this clause includes all constants > with at least some part being of a private type or private extension) > global to a callable > entity that are potentially read or updated as part of the execution > of a call on the entity. It seems to be going too far, since it essentially implies that everything except visible elementary types has to be covered (and trivial composite types). (But it *surely* fixes the problem.) Can you show an example of how my slightly stricter rule (that is, that constants of types with Global /= null be required) could be defeated? That is, declare a private type with a Global => null (meaning no squirreling controlled parts) and still manage to mutate a constant. > I think we might want to also add: > > {Constants of any type may also be mentioned in a Global aspect.} > > There seems no harm, and that way the programmer doesn't have to worry > about maintenance issues when a type suddenly has a private component > added or removed. Also, SPARK requires certain > constants-initialized-by-variables to be mentioned, so this would > allow them to do so without violating the Ada rules. Yes, that makes sense. **************************************************************** From: Tucker Taft Sent: Wednesday, January 9, 2019 6:51 PM >It seems to be going too far, since it essentially implies that everything >except visible elementary types has to be covered (and trivial composite >types). (But it *surely* fixes the problem.) > >Can you show an example of how my slightly stricter rule (that is, that >constants of types with Global /= null be required) could be defeated? That >is, declare a private type with a Global => null (meaning no squirreling >controlled parts) and still manage to mutate a constant. type T is tagged private; private type T is new Controlled with record AI : aliased Integer := 22; P : access Integer; end record; procedure Initialize (X : in out T) is -- Doesn't have any global effects. Only change is to X itself. begin X.P := X.AI'Unchecked_access; end Initialize; Global_P : access Integer; procedure Copy_To_Global (X : in T) is -- This can be called anytime to cause a constant to be -- designated by an access-to-variable Global begin Global_P := X.P.all'Unchecked_Access; end Copy_To_Global; Z : constant T := ...; procedure Kill_Z with Global => access Integer; procedure Kill_Z is -- Calling this updates part of Z, but I can't imagine how we would know that! begin Global_P.all := 37; end Kill_Z; **************************************************************** From: Randy Brukardt Sent: Thursday, January 10, 2019 5:25 PM >>> The wording should now be: >>> >>> I suggest we indicate on this early use of the term >>> "variable" the following: >>> >>> The Global aspect identifies the set of variables >>> (which for the purposes of this clause includes all constants >>> with at least some part being of a private type or private >>> extension) >>> global to a callable >>> entity that are potentially read or updated as part of the execution >>> of a call on the entity. I failed to catch this yesterday, but this wording needs to include all constants with some part being a visible immutably limited type (maybe better to state as "some part being immutably limited or controlled"). Otherwise, you can have the problem with a visible type, which would be silly. :-) And why does your wording include "at least"? Isn't "some part" enough? So the new wording could be (which for the purposes of this clause includes all constants with some part being immutably limited, or of a private type, private extension, or controlled type) Maybe there's a better order for this. But also see below. ... > Global_P : access Integer; > > procedure Copy_To_Global (X : in T) is A Global is needed here to somehow mention Global_P. Since it's private, it would have to be "private package <>". But I don't think this changes your conclusion any. > -- This can be called anytime to cause a constant to be > -- designated by an access-to-variable Global > begin > Global_P := X.P.all'Unchecked_Access; > end Copy_To_Global; > > Z : constant T := ...; > > procedure Kill_Z with Global => access Integer; > procedure Kill_Z is > -- Calling this updates part of Z, but I can't imagine how we would > -- know that! > begin > Global_P.all := 37; > end Kill_Z; I see. I was thinking for a while that there would always have to be a parameter, and that if you assumed "in" parameters of composite types are always modified, this would be not a problem, but that's not enough for Kill_Z. But I think I was right about having to assume that any composite type that is inherently mutable or has a part of some access type (which would necessarily have to include all private types) modifies "in" parameters. You can't assume otherwise for existing Ada code (the Rosen trick and varieties like my Claw code are common), and that certainly seems to carry over into new Ada code. So I'd suggest that your Modifies (or was it Modified??) aspect allow "null" as an option; if given, that implies all "in" parameters don't modify their argument. And perhaps allowing a default to be inherited from a package, much as we do with Nonblocking and Global. (But that's probably for Corrigendum 1 for Ada 2020.) >>> I think we might want to also add: >>> >>> {Constants of any type may also be mentioned in a Global aspect.} >>> >>> There seems no harm, and that way the programmer doesn't have >>> to worry about maintenance issues when a type suddenly has a >>> private component added or removed. Also, SPARK requires >>> certain constants-initialized-by-variables to be mentioned, >>> so this would allow them to do so without violating the Ada rules. >>Yes, that makes sense. Sounds like we're agreed. Do you want me to write up a fix AI to make these two changes to AI12-0079-1?? **************************************************************** From: Randy Brukardt Sent: Friday, January 11, 2019 2:55 PM > And why does your wording include "at least"? Is "some part" enough? > > So the new wording could be > (which for the purposes of this clause includes all constants > with some part being immutably limited, or of a private > type, private extension, or controlled type) Looking at the existing AI12-0079-1, I had another idea as to how we could prevent dragging the universe in here. What if we used Preelaborable initialization (PI) here (combined with immutably limited)? A type with a non-trivial Initialize never has Preelaborable initialization. So if we said (which for the purposes of this clause includes all constants with some part being immutably limited, controlled, or of a private type or private extension that does not have preelaborable initialization) We'd catch any private types that have a non-trivial Initialize (which means that anything allowed could not squirrel). And PI extends to subcomponents, so those are covered for free. Ugh, "immutably limited" doesn't catch private types completed by regular composite types with an immutably limited subcomponent. Those types have to be limited, though. So the rule would have to be: (which for the purposes of this clause includes all constants with some part being immutably limited, controlled, or of a nonlimited private type or private extension that does not have preelaborable initialization) This would at least give people a way to declare ADTs that wouldn't be caught by the rule (although they couldn't be controlled). For instance, type Imaginary in the complex package wouldn't be caught (for some reason, Complex itself isn't private, so it doesn't need help). Similarly for the Bounded_Bignum (except, of course, that we're probably not doing that. :-) Also Exception_Id, and many others. Humm. I suppose one could squirrel via Adjust. Seems useless, but that wouldn't be covered by PI. So I guess this wouldn't work, either. Darn. **************************************************************** From: Tucker Taft Sent: Thursday, April 18, 2019 10:47 AM SPARK has the notion of "abstract state" which appears in Global aspects. We should permit such implementation-defined extensions. I would suggest adding after 6.1.2(46/5) the additional permission: Implementations may extend the syntax for global_aspect_definition, as well as any of the syntactic categories that comprise it, in an implementation-defined manner. The key point is that they may *extend* it, but must still support the forms that are part of the standard. *************************************************************** From: John Barnes Sent: Thursday, April 18, 2019 10:59 AM That seems vital *************************************************************** From: Randy Brukardt Sent: Thursday, April 18, 2019 1:43 PM Seems reasonable. I suggest that you write up an AI to that effect, or perhaps add it to the still open AI12-0303-1. *************************************************************** From: Tucker Taft Sent: Thursday, April 18, 2019 2:16 PM OK, below is an update to AI12-0303-1. [This is version /02 of the AI - Editor.] *************************************************************** From: Randy Brukardt Sent: Thursday, April 18, 2019 7:33 PM > OK, below is an update to AI12-0303-1. Looks good. But... ... > Replace the following wording from RM 6.2.1(12/5): There's no 6.2.1 in the draft RM. You mean 6.1.2. I fixed that throughout. As well as a couple of spacing and punctuation fixes. And I replaced "e.g." with "such as" (we try to avoid that as it is often misused and no one is quite sure what the definition is). I also added a note to mention that these paragraph numbers are from Draft 19. I don't want to try to figure out why the paragraph numbers don't make sense when reading this AI in 2027. :-) *************************************************************** From: Tucker Taft Sent: Thursday, April 18, 2019 10:22 PM > ... >> Replace the following wording from RM 6.2.1(12/5): > > There's no 6.2.1 in the draft RM. You mean 6.1.2. I fixed that throughout. > As well as a couple of spacing and punctuation fixes. And I replaced "e.g." > with "such as" (we try to avoid that as it is often misused and no one > is quite sure what the definition is). Thanks. > > I also added a note to mention that these paragraph numbers are from > Draft 19. I don't want to try to figure out why the paragraph numbers > don't make sense when reading this AI in 2027. :-) Good point. ***************************************************************