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

Differences between 1.9 and version 1.10
Log of other versions for file ai12s/ai12-0112-1.txt

--- ai12s/ai12-0112-1.txt	2018/12/14 08:31:30	1.9
+++ ai12s/ai12-0112-1.txt	2019/01/04 05:00:31	1.10
@@ -1,4 +1,7 @@
-!standard A.18.2(99/3)                                18-07-27    AI12-0112-1/04
+!standard A.18.2(99/3)                                18-01-03    AI12-0112-1/06
+!standard 11.5(23)
+!standard 11.5(26)
+!standard A(4)
 !class Amendment 14-05-15
 !status Amendment 1-2012 18-12-10
 !status ARG Approved 9-0-2  18-12-10
@@ -69,11 +72,11 @@
 Suppress). This sort of stomps on GNAT's existing implementation, although
 they should be pretty close in functionality (exceptions not raised through
 preconditions are not included in this Ada definition). Is this a problem?
-Is there an alternative name? (See !discussion.)
+Is there an alternative name? (See !discussion.) [This is fine.]
 
 (2) Should the preconditions be repeated in the semantics section or just
 shown in the package specification? I have them repeated for now, but that's
-relatively easy to change. 
+relatively easy to change. [Repeated.]
 
 (3) I used Pre and Post rather than Pre'Class and Post'Class, since these
 mostly belong to the specific routine rather than any routine matching the
@@ -84,14 +87,15 @@
 seem unusual, and using multiple versions of a single container simultaenously
 more so). By using Pre, an implementation can generate the precondition as
 part of the subprogram body if it wishes (or it can generate it at the call
-site to support optimization and suppressibility). Objections?
+site to support optimization and suppressibility). Objections? [This is OK.]
 
 (4) I've overridden the usual Nonblocking and Global status for the various
 predicate routines, to essentially mark these as Pure. If Nonblocking => True
 is used, this would prevent calling the formal subprograms in the associated
 routines. But that shouldn't be necessary to implement these (they usually
 are direct queries on the container state). Can anyone think of a reason NOT
-to require these routines to be pure (in general or specifically)?
+to require these routines to be pure (in general or specifically)? [This is
+also OK.]
 
 (5) The global setting "Access subtype_mark" says that it applies to all of
 the "(aliased)" objects of subtype_mark. For a tagged type (like Vector), it
@@ -106,7 +110,7 @@
 of these be written in prefixed notation for consistency? (We decided the
 reverse the previous time, I think.) I suppose I could have used an expanded
 name instead (Vectors.Length (Container)) - but that's just longer for no
-obvious reason.
+obvious reason. [Using prefix is OK, but only use it when necessary.]
 
 (7) I intend to check that this specification is compilable, and would prefer
 to check it against GNAT's existing implementation (meaning compiling the spec
@@ -114,6 +118,7 @@
 I'll need some help from someone at AdaCore, as I don't have access to the
 AdaCore test suite and would need help finding the source code and recompiling
 part of the runtime with GNAT (never having done that). Is there a volunteer??
+[Both Bob and Tucker at various times have offered to help.]
 
 (8) It would be best if we had a way to specify a precondition for anonymous
 access-to-subprogram types in order to properly handle
@@ -130,7 +135,7 @@
 Neither of these are critical, in the sense that the specification will work
 without them. It just means that tools and compilers cannot detect failing
 tampering checks (and optimize away unnecessary checks) based on these
-properties alone.
+properties alone. [Don't worry about this.]
 
 ]
 
@@ -157,14 +162,12 @@
         Nonblocking => Equal_Element'Nonblocking,
         Global => Equal_Element'Global &
                   Element_Type'Global &
-                  in out synchronized Ada.Containers.Vectors &
-                  in out synchronized <<some impl-defed helper packages>> is
+                  in out synchronized Ada.Containers.Vectors is
 
 [These are the default Nonblocking and Global settings; they're used unless
-otherwise  specified. Note that these depend on the formal parameters of the
-package. <<some impl-defed helper packages>> is a placeholder for however we
-decide to deal with helper packages. Note that in the Bounded version, Global
-is just Equal_Element'Global & Element_Type'Global.]
+otherwise specified. Note that these depend on the formal parameters of the
+package. Note that in the Bounded version, Global is just Equal_Element'Global
+& Element_Type'Global.]
 
    subtype Extended_Index is
       Index_Type'Base range
@@ -195,7 +198,7 @@
       renames "=";
 
 [Note: We need this renames of the formal parameter in order to be able to
-write the Nonblocking and Global aspects.]
+write the Nonblocking and Global aspects. "="'Global is ambigious.]
 
 [The rest of the package is as described in the detailed wording below. The
 specs would match.]
@@ -258,7 +261,7 @@
 function To_Vector (Length : Count_Type) return Vector
    with Post => To_Vector'Result.Length = Length and then
                 not Tampering_With_Elements_Prohibited (To_Vector'Result) and then
-                not Tampering_With_Cursors (To_Vector'Result) and then
+                not Tampering_With_Cursors_Prohibited (To_Vector'Result) and then
                 To_Vector'Result.Capacity >= Length;
 101/2
 Returns a vector with a length of Length, filled with empty elements.
@@ -269,7 +272,7 @@
    Length   : Count_Type) return Vector
    with Post => Length (To_Vector'Result) = Length and then
                 not Tampering_With_Elements_Prohibited (To_Vector'Result) and then
-                not Tampering_With_Cursors (To_Vector'Result) and then
+                not Tampering_With_Cursors_Prohibited (To_Vector'Result) and then
                 To_Vector'Result.Capacity >= Length;
 103/2
 Returns a vector with a length of Length, filled with elements initialized to
@@ -279,7 +282,7 @@
 function "&" (Left, Right : Vector) return Vector
    with Post => Length (Vectors."&"'Result) = Length (Left) + Length (Right),
                 not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
-                not Tampering_With_Cursors (Vectors."&"'Result) and then
+                not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then
                 Vectors."&"'Result.Capacity >= Length (Left) + Length (Right);
 105/2
 Returns a vector comprising the elements of Left followed by the elements of
@@ -290,7 +293,7 @@
               Right : Element_Type) return Vector
    with Post => Vectors."&"'Result.Length = Length (Left) + 1 and then
                 not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
-                not Tampering_With_Cursors (Vectors."&"'Result) and then
+                not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then
                 Vectors."&"'Result.Capacity >= Length (Left) + 1;
 107/2
 Returns a vector comprising the elements of Left followed by the element Right.
@@ -300,7 +303,7 @@
               Right : Vector) return Vector
    with Post => Length (Vectors."&"'Result) = Length (Right) + 1 and then
                 not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
-                not Tampering_With_Cursors (Vectors."&"'Result),
+                not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then
                 Vectors."&"'Result.Capacity >= Length (Right) + 1;
 109/2
 Returns a vector comprising the element Left followed by the elements of Right.
@@ -309,7 +312,7 @@
 function "&" (Left, Right  : Element_Type) return Vector
    with Post => Length ("&"'Result) = 2 and then
                 not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
-                not Tampering_With_Cursors (Vectors."&"'Result) and
+                not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then
                 Vectors."&"'Result.Capacity >= 2;
 
 111/2
@@ -667,6 +670,8 @@
    with Pre => (if Capacity /= 0 and then Capacity < Length (Source)
                 then raise Capacity_Error),
         Post => Length (Copy'Result) = Length (Source) and then
+                not Tampering_With_Elements_Prohibited (Copy'Result) and then
+                not Tampering_With_Cursors_Prohibited (Copy'Result) and then
                 Copy'Result.Capacity >= (if Capacity = 0 then
                    Length (Source) else Capacity);
 147.22/3+
@@ -1590,8 +1595,8 @@
 or in an instance of a generic unit declared in a child unit of
 Ada.Containers.
 
-AARM Reason: One could use the Assertion_Policy to eliminate such checks, but
-that would require recompiling the Ada.Containers packages (the assertion
+AARM Reason: One could use @b<pragma> Assertion_Policy to eliminate such checks,
+but that would require recompiling the Ada.Containers packages (the assertion
 policy that determines whether the checks are made is that used to compile the
 unit). In addition, we do not want to specify the behavior of the
 Ada.Containers operations if the precondition fails; that is different than
@@ -1605,13 +1610,52 @@
 occurs, the execution of the program is erroneous. {Similarly, if a
 precondition check has been suppressed and the evaluation of the precondition
 would have raised an exception, execution is erroneous.}
-
-AARM Reason: It's unclear that a precondition expression that includes
-/raise/ Program_Error is an "error situation"; the precondition never actually
-evaluates to False in that case. Thus, we spell out that case. We only allow
-suppressing preconditions associated with language-defined units; other
-preconditions follow the rules of the appropriate Assertion_Policy.
 
+AARM Reason: It's unclear that a precondition expression that executes 
+/raise/ *some_exception* is an "error situation"; the precondition 
+never actually evaluates to False in that case. Thus, we spell out that case.
+We only allow suppressing preconditions associated with language-defined 
+units; other preconditions follow the rules of the appropriate 
+Assertion_Policy.
+
+
+Add after Annex A(4): [Implementation Permissions]
+
+The implementation may add specifications of synchronized entities of
+implementation-defined packages to the global specification (see 6.1.2) for
+any language-defined entity that is not declare pured or has a global 
+specification of \null\.
+
+AARM Reason: Ada runtime libraries often use implementation-defined helper
+packages to implement the language-defined units. For instance, it is common
+to use a common low-level package to implement I/O; if that package includes
+support for Current Input and Current Output, then it is likely to have state
+that needs to be reflected in the packages that use it such as Ada.Text_IO.
+
+We want to allow such packages, so we have defined this permission to allow 
+them to include state if necessary. We require that any such state is 
+synchronized to ensure that appropriate use (as defined above) is allowed in 
+parallel operations.
+
+We exclude units that are declared pure from this permission since this is
+a declaration that the unit doesn't have any global state, so specifying 
+otherwise would defeat the purpose. Similarly, entities that explicitly 
+specify Global as \null\ are supposed to have no side-effects, and we don't 
+want implementations to add any.
+End AARM Reason.
+
+AARM Ramification: Implementations are of course allowed to make other changes
+to the specifications of language-defined units, so long as those changes are 
+semantically neutral (that is, no program could change legality or effect
+because of the changes). In particular, an implementation would need to
+add implementation-defined units to the context clause in order to use the
+previous permission; this is allowed and does not need a separate permission.
+
+Similarly, an implementation can add postconditions to
+language-defined subprograms, so long as those postconditions
+always evaluate to True. This is useful if the
+implementation can use those postconditions for optimization.
+End AARM Ramification.
 
 !discussion
 
@@ -1694,6 +1738,45 @@
 hopefully the new aspect will trigger implementers to inspect their 
 implementations for issues.
 
+!corrigendum 11.5(23)
+
+@dinsa
+@xhang<@xterm<Storage_Check>
+Check that evaluation of an @fa<allocator> does not require more space than 
+is available for a storage pool. Check that the space available for a task 
+or subprogram has not been exceeded.>
+@dinss
+@xbullet<The following check corresponds to situations in which the exception
+Assertion_Error is raised upon failure.>
+@xhang<@xterm<Container_Check>
+Check the precondition of a routine declared in a child unit of Ada.Containers
+or in an instance of a generic unit declared in a child unit of
+Ada.Containers.>
+
+!corrigendum 11.5(26)
+
+@drepl
+If a given check has been suppressed, and the corresponding error situation
+occurs, the execution of the program is erroneous.
+@dby
+If a given check has been suppressed, and the corresponding error situation
+occurs, the execution of the program is erroneous. Similarly, if a
+precondition check has been suppressed and the evaluation of the precondition
+would have raised an exception, execution is erroneous.
+
+!corrigendum A(4)
+
+@dinsa
+The implementation may restrict the replacement of language-defined 
+compilation units. The implementation may restrict children of 
+language-defined library units (other than Standard). 
+@dinst
+The implementation may add specifications of synchronized entities of
+implementation-defined packages to the global specification (see 6.1.2) for 
+any language-defined entity that is not declared pure or has a global 
+specification of @b<null>.
+
+
 !ASIS
 
 No ASIS impact.
@@ -1809,8 +1892,8 @@
 parameters. [The next three parameter "<" that I see will be the first. ;-)]
 That would allow applications that care about Global or want to uniformly use
 prefixed notation or to do a derivation to work usefully, and won't (I think)
-equire any other code to change. [It would be only incompatible with anyone
-hat decided to add these themselves somewhere; that might make some calls
+require any other code to change. [It would be only incompatible with anyone
+that decided to add these themselves somewhere; that might make some calls
 ambiguous. That's the normal problem from added new routines.]
 
 I'm thinking that adding these routines might be a good idea, especially for
@@ -2036,4 +2119,205 @@
 off on it.
 
 ****************************************************************
+
+From: Randy Brukardt
+Sent: Friday, December 14, 2018  9:15 PM
+
+We've talked on several occasions about having a global permission for 
+implementation-defined packages to appear in the Global specification of 
+language-defined entities. This is needed, for instance, to support an 
+implementation-defined helper package that implements all of the low-level IO 
+operations. If that package has state, it needs to appear in the global 
+contracts of packages that use it. Forcing implementations to move all of the 
+state seems like a nightmare for implementers and adverse to good Ada design 
+practice (share as much as possible of the implementation).
+
+At the recent meeting we talked about putting this into the start of Annex A. 
+We also talked about allowing additional postconditions, which we agreed was 
+possible without any permission.
+
+Here is suggested wording for this permission and some associated AARM notes. 
+Improvements welcome.
+
+=============
+
+Add after Annex A(4): [Implementation Permissions]
+
+The implementation may add specifications of synchronized entities of 
+implementation-defined packages to the global specification for any 
+language-defined entity that is not declare pure or has a global specification 
+of \null\.
+
+AARM Reason: Ada runtime libraries often use implementation-defined helper 
+packages to implement the language-defined units. For instance, it is common
+to use a common low-level package to implement I/O; if that package includes
+support for Current Input and Current Output, then it is likely to have state
+that needs to be reflected in the packages that use it such as Ada.Text_IO.
+
+We want to allow such packages, so we have defined this permission to allow 
+them to include state if necessary. We require that any such state is 
+synchronized to ensure that appropriate use (as defined above) is allowed in
+parallel operations.
+
+We exclude units that are declared pure from this permission since this is a
+declaration that the unit doesn't have any global state, so specifying 
+otherwise would defeat the purpose. Similarly, entities that explicitly 
+specify Global as \null\ are supposed to have no side-effects, and we don't 
+want implementations to add any.
+End AARM Reason.
+
+AARM Ramification: Implementations are allowed to make other changes to the 
+specifications of language-defined units, so long as those changes are 
+semantically neutral (that is, no program could change legality or effect 
+because of the changes). In particular, an implementation would need to add
+implementation-defined units to the context clause in order to use the 
+previous permission; this is allowed and does not need a separate permission.
+
+Similarly, an implementation can add/enhance postconditions to 
+language-defined subprograms, so long as those postconditions reflect the 
+definition of the subprogram. This might be useful, for instance, if the 
+implementation can use those postconditions to eliminate following code 
+(perhaps by proving that a following precondition must be true based on the 
+postcondition).
+End AARM Ramification.
+
+****************************************************************
+
+From: Bob Duff
+Sent: Saturday, December 15, 2018  10:50 AM
+
+> Here is suggested wording for this permission and some associated AARM 
+> notes.
+> ...
+
+Looks good to me.
+
+By the way, how would one express the fact that Text_IO is messing around 
+with the state on the disk? Is that even possible?
+
+> AARM Ramification: Implementations are allowed to make other changes 
+> to the specifications of language-defined units, so long as those 
+> changes are semantically neutral (that is, no program could change 
+> legality or effect because of the changes). In particular, an 
+> implementation would need to add implementation-defined units to the 
+> context clause in order to use the previous permission; this is 
+> allowed and does not need a separate permission.
+
+That's so obvious, I'm tempted to add "of course":
+"Implementations are allowed..."
+
+And maybe remove the parenthetical remark -- anybody reading the AARM 
+should know what "semantically neutral" means.
+
+> Similarly, an implementation can add/enhance postconditions to 
+> language-defined subprograms, so long as those postconditions reflect 
+> the definition of the subprogram. This might be useful, for instance, 
+> if the implementation can use those postconditions to eliminate 
+> following code (perhaps by proving that a following precondition must 
+> be true based on the postcondition).
+
+I suggest shortening that a bit:
+
+    Similarly, an implementation can add postconditions to
+    language-defined subprograms, so long as those postconditions
+    are True. This is useful if the
+    implementation can use those postconditions for optimization.
+
+***************************************************************
+
+From: Bob Duff
+Sent: Saturday, December 15, 2018  10:58 AM
+
+> That's so obvious, I'm tempted to add "of course":
+> "Implementations are allowed..."
+
+Ooops, I meant to write:
+
+    That's so obvious, I'm tempted to add "of course":
+    "Implementations are of course allowed..."
+                         ^^^^^^^^^
+
+Of COURSE that's what I meant!  ;-)
+
+***************************************************************
+
+From: Randy Brukardt
+Sent: Sunday, December 16, 2018  12:09 AM
+
+> > Here is suggested wording for this permission and some associated 
+> > AARM notes.
+> > ...
+> 
+> Looks good to me.
+
+Thanks for the comments.
+
+> By the way, how would one express the fact that Text_IO is messing 
+> around with the state on the disk?
+> Is that even possible?
+
+Not sure. I've always imagined it as the "state" of one of the helper 
+packages, but I don't know if that is really the right model.
+ 
+...
+> And maybe remove the parenthetical remark -- anybody reading the AARM 
+> should know what "semantically neutral" means.
+
+I've heard several times from people on comp.lang.ada that they found the AARM
+interesting reading. That is, not everyone reading it is an implementer or 
+language lawyer. (I probably would have found it interesting had it existed
+when I was at the University of Wisconsin.) So I don't want to assume too much 
+about the reader's knowledge. Besides, it really easy to assume that such 
+things are obvious when you've been talking about such things for decades. So 
+I think the parenthetical remark is helpful to some readers, and reinforcing 
+to others (including me!).
+
+> > Similarly, an implementation can add/enhance postconditions to 
+> > language-defined subprograms, so long as those postconditions 
+> > reflect the definition of the subprogram. This might be useful, for 
+> > instance, if the implementation can use those postconditions to 
+> > eliminate following code (perhaps by proving that a following 
+> > precondition must be true based on the postcondition).
+> 
+> I suggest shortening that a bit:
+> 
+>     Similarly, an implementation can add postconditions to
+>     language-defined subprograms, so long as those postconditions
+>     are True. This is useful if the
+>     implementation can use those postconditions for optimization.
+
+Seems a bit too short to me, it seems to say that you can only add "True" as 
+postconditions. (Obviously, no one would write a note to say that, so it's 
+nonsense, but it takes some thought to figure that out.) How about:
+
+     Similarly, an implementation can add postconditions to
+     language-defined subprograms, so long as those postconditions
+     always evaluate to True. This is useful if the
+     implementation can use those postconditions for optimization.
+
+or maybe "always would evaluate to True" (since they won't actually be 
+evaluated in most circumstances).
+
+***************************************************************
+
+From: Bob Duff
+Sent: Sunday, December 16, 2018  1:50 PM
+
+> Seems a bit too short to me, it seems to say that you can only add 
+> "True" as postconditions.
+
+Good point.
+>      Similarly, an implementation can add postconditions to
+>      language-defined subprograms, so long as those postconditions
+>      always evaluate to True. This is useful if the
+>      implementation can use those postconditions for optimization.
+
+Yes, that's better.
+
+> or maybe "always would evaluate to True" (since they won't actually be 
+> evaluated in most circumstances).
+
+I slightly prefer leaving out the "would".
+
+***************************************************************
 

Questions? Ask the ACAA Technical Agent