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

Differences between 1.1 and version 1.2
Log of other versions for file ai12s/ai12-0339-1.txt

--- ai12s/ai12-0339-1.txt	2019/07/17 02:26:41	1.1
+++ ai12s/ai12-0339-1.txt	2019/07/17 03:28:49	1.2
@@ -1,5 +1,33 @@
-!standard A.18.2(8/5)                                  19-06-16  AI12-0339-1/01
+!standard A.18.2(8/5)                                  19-07-16  AI12-0339-1/02
+!standard A.18.2(13/5)
+!standard A.18.2(78.2/5)
+!standard A.18.2(99/5)
+!standard A.18.3(6/5)
+!standard A.18.3(9.1/5)
+!standard A.18.3(50.2/5)
+!standard A.18.5(3/5)
+!standard A.18.5(6.1/5)
+!standard A.18.5(37.3/5)
+!standard A.18.5(47/5)
+!standard A.18.6(4/5)
+!standard A.18.6(7.1/5)
+!standard A.18.6(51.4/5)
+!standard A.18.8(3/5)
+!standard A.18.8(6.1/5)
+!standard A.18.8(59.2/5)
+!standard A.18.8(69/5)
+!standard A.18.9(4/5)
+!standard A.18.9(7.1/5)
+!standard A.18.9(74.2/5)
+!standard A.18.10(11.1/5)
+!standard A.18.18(7.1/5)
+!standard A.18.20(7/5)
+!standard A.18.22(7/5)
+!standard A.18.24(7/5)
+!standard A.18.25(8/3)
 !class Amendment 19-06-16
+!status Amendment 1-2012 19-07-16
+!status ARG Approved 10-0-0  19-06-16
 !status work item 19-06-16
 !status received 19-06-12
 !priority Low
@@ -9,9 +37,9 @@
 
 Define appropriate Empty functions for all the containers. For containers
 types that have an associated Capacity, the corresponding Empty function accepts a
-Capacity parameter to specify this value. The Capacity parameter will have a
-system defined default value. For other container types that do not have the
-notion of capacity, the Empty function will be parameterless.
+Capacity parameter to specify this value. The Capacity parameter will have an
+implementation-defined default value. For other container types that do not 
+have the notion of capacity, the Empty function is parameterless.
 
 !problem
 
@@ -46,7 +74,7 @@
 
 !wording
 
-Modify A.18.2 (8/5)
+Modify A.18.2(8/5):
 
 type Vector is tagged private
       with Constant_Indexing => Constant_Reference,
@@ -66,19 +94,19 @@
               (not Tampering_With_Cursors_Prohibited (Vector)) and then
               (not Tampering_With_Elements_Prohibited (Vector));
 
-Insert before A.18.2 (13/5)
+Insert before A.18.2(13/5):
 
 function Empty
-     (Capacity   : Count_Type := Implementation Defined) return Vector
+     (Capacity   : Count_Type := /implementation-defined/) return Vector
       with Pre  => (if Capacity > Maximum_Length then raise Constraint_Error),
            Post =>
-              Empty'Result.Capacity = Capacity and then
+              Capacity (Empty'Result) >= Capacity and then
               not Tampering_With_Elements_Prohibited (Empty'Result) and then
               not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Length = 0;
+              Length (Empty'Result) = 0;
 
 
-Modify A.18.2 (78.2/5)
+Modify A.18.2(78.2/5):
 
 type Vector (Base : not null access Vectors.Vector) is
          tagged limited private
@@ -94,32 +122,61 @@
               Global => (in Vector.Base.all, synchronized out Vector.Base.all),
               Default_Initial_Condition => Length (Vector) = 0;
       pragma Preelaborable_Initialization(Vector);
-
 
-Insert before A.18.2 (99/5)
+Insert before A.18.2(99/5):
 
-function Empty (Capacity : Count_Type := Implementation Defined) return Vector
+function Empty (Capacity : Count_Type := /implementation-defined/) return Vector
    with Pre  => (if Capacity > Maximum_Length then raise Constraint_Error),
         Post =>
-           Empty'Result.Capacity = Capacity and then
+           Capacity (Empty'Result) = Capacity and then
            not Tampering_With_Elements_Prohibited (Empty'Result) and then
            not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-           Empty'Result.Length = 0;
- Returns a vector with a length of 0 that has additional storage allocated to
- ensure that the length of the resulting vector can become at least the value
- Capacity without requiring an additional call to Reserve_Capacity.
+           Length (Empty'Result) = 0;
+ Returns an empty vector.
 
+Modify A.18.3(6/5):
+
+type List is tagged private
+      with Constant_Indexing => Constant_Reference,
+           Variable_Indexing => Reference,
+           Default_Iterator  => Iterate,
+           Iterator_Element  => Element_Type,
+           Iterator_View     => Stable.List,
+           Aggregate         => (Empty       => Empty[_List],
+                                 Add_Unnamed => Append),
+           Stable_Properties => (Length,
+                                 Tampering_With_Cursors_Prohibited,
+                                 Tampering_With_Elements_Prohibited),
+           Default_Initial_Condition =>
+              Length (List) = 0 and then
+              (not Tampering_With_Cursors_Prohibited (List)) and then
+              (not Tampering_With_Elements_Prohibited (List));
 
-Insert before A.18.3 (9.1/5)
+Insert before A.18.3(9.1/5):
 
 function Empty return List
-      with Post =>
-              not Tampering_With_Elements_Prohibited (Empty'Result) and then
-              not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Length = 0 is (Empty_List);
+   is (Empty_List)
+   with Post =>
+           not Tampering_With_Elements_Prohibited (Empty'Result) and then
+           not Tampering_With_Cursors_Prohibited (Empty'Result) and then
+           Length (Empty'Result) = 0;
+
+Modify A.18.3(50.2/5):
 
+   type List (Base : not null access Doubly_Linked_Lists.List) is
+         tagged limited private
+         with Constant_Indexing => Constant_Reference,
+              Variable_Indexing => Reference,
+              Default_Iterator  => Iterate,
+              Iterator_Element  => Element_Type,
+              Aggregate         => (Empty          => Empty_List,
+                                    Add_Unnamed    => Append),
+              Stable_Properties => (Length),
+              Global => (in List.Base.all, synchronized out List.Base.all),
+              Default_Initial_Condition => Length (List) = 0;
+      pragma Preelaborable_Initialization(List);
 
-Modify A.18.5 (3/5)
+Modify A.18.5(3/5):
 
 type Map is tagged private
       with Constant_Indexing => Constant_Reference,
@@ -138,18 +195,17 @@
               (not Tampering_With_Elements_Prohibited (Map));
    pragma Preelaborable_Initialization(Map);
 
+Insert before A.18.5(6.1/5):
 
-Insert before A.18.5 (6.1/5)
-
 function Empty
-     (Capacity   : Count_Type := Implementation Defined) return Map
+     (Capacity   : Count_Type := /implementation-defined/) return Map
       with Post =>
-              Empty'Result.Capacity = Capacity and then
+              Capacity (Empty'Result) >= Capacity and then
               not Tampering_With_Elements_Prohibited (Empty'Result) and then
               not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Length = 0;
+              Length (Empty'Result) = 0;
 
-Modify A.18.5 (37.3/5)
+Modify A.18.5(37.3/5):
 
 type Map (Base : not null access Hashed_Maps.Map) is
          tagged limited private
@@ -164,27 +220,59 @@
               Default_Initial_Condition => Length (Map) = 0;
       pragma Preelaborable_Initialization(Map);
 
-Insert before A.18.5 (47/5)
+Insert before A.18.5(47/5):
 
-function Empty (Capacity : Count_Type := Implementation Defined) return Map
+function Empty (Capacity : Count_Type := /implementation-defined/) return Map
    with Post =>
-           Empty'Result.Capacity = Capacity and then
+           Capacity (Empty'Result) >= Capacity and then
            not Tampering_With_Elements_Prohibited (Empty'Result) and then
            not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-           Empty'Result.Length = 0;
- Returns a map with a length of 0 that has additional storage allocated to ensure
- that the length of the resulting map can become at least the value Capacity
- without requiring an additional call to Reserve_Capacity.
+           Length (Empty'Result) = 0;
+ Returns an empty map.
 
-Insert before A.18.6 (7.1/5)
+Modify A.18.6(4/5):
 
+type Map is tagged private
+      with Constant_Indexing => Constant_Reference,
+           Variable_Indexing => Reference,
+           Default_Iterator  => Iterate,
+           Iterator_Element  => Element_Type,
+           Iterator_View     => Stable.Map,
+           Aggregate         => (Empty     => Empty[_Map],
+                                 Add_Named => Insert),
+           Stable_Properties => (Length,
+                                 Tampering_With_Cursors_Prohibited,
+                                 Tampering_With_Elements_Prohibited),
+           Default_Initial_Condition =>
+              Length (Map) = 0 and then
+              (not Tampering_With_Cursors_Prohibited (Map)) and then
+              (not Tampering_With_Elements_Prohibited (Map));
+
+Insert before A.18.6(7.1/5):
+
 function Empty return Map
-      with Post =>
-              not Tampering_With_Elements_Prohibited (Empty'Result) and then
-              not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Length = 0 is (Empty_Map);
+   is (Empty_Map)
+   with Post =>
+           not Tampering_With_Elements_Prohibited (Empty'Result) and then
+           not Tampering_With_Cursors_Prohibited (Empty'Result) and then
+           Length (Empty'Result) = 0;
+
+Modify A.18.6(51.4/5):
+
+type Map (Base : not null access Ordered_Maps.Map) is
+         tagged limited private
+         with Constant_Indexing => Constant_Reference,
+              Variable_Indexing => Reference,
+              Default_Iterator  => Iterate,
+              Iterator_Element  => Element_Type,
+              Aggregate         => (Empty      => Empty_Map,
+                                    Add_Named  => Insert),
+              Stable_Properties => (Length),
+              Global => (in Map.Base.all, synchronized out Map.Base.all),
+              Default_Initial_Condition => Length (Map) = 0;
+      pragma Preelaborable_Initialization(Map);
 
-Modify A.18.8 (3/5)
+Modify A.18.8(3/5):
 
 type Set is tagged private
       with Constant_Indexing => Constant_Reference,
@@ -200,17 +288,18 @@
               (not Tampering_With_Cursors_Prohibited (Set));
    pragma Preelaborable_Initialization(Set);
 
-Insert before A.18.8 (6.1/5)
+Insert before A.18.8(6.1/5):
 
 function Empty
-     (Capacity   : Count_Type := Implementation Defined) return Map
+     (Capacity   : Count_Type := /implementation-defined/) return Map
       with Post =>
-              Empty'Result.Capacity = Capacity and then
+              Capacity (Empty'Result) = Capacity and then
               not Tampering_With_Elements_Prohibited (Empty'Result) and then
               not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Length = 0;
+              Length (Empty'Result) = 0;
+
+Modify A.18.8(59.2/5):
 
-Modify A.18.8 (59.2/5)
 type Set (Base : not null access Hashed_Sets.Set) is
          tagged limited private
          with Constant_Indexing => Constant_Reference,
@@ -223,97 +312,128 @@
               Default_Initial_Condition => Length (Set) = 0;
       pragma Preelaborable_Initialization(Set);
 
-Insert before A.18.8 (69/5)
+Insert before A.18.8(69/5):
 
-function Empty (Capacity : Count_Type := Implementation Defined) return Set
+function Empty (Capacity : Count_Type := /implementation-defined/) return Set
    with Post =>
-           Empty'Result.Capacity = Capacity and then
+           Capacity (Empty'Result) >= Capacity and then
            not Tampering_With_Elements_Prohibited (Empty'Result) and then
            not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-           Empty'Result.Length = 0;
- Returns a set with a length of 0 that has additional storage allocated to ensure
- that the length of the resulting set can become at least the value Capacity
- without requiring an additional call to Reserve_Capacity.
+           Length (Empty'Result) = 0;
+ Returns an empty set.
+
+Modify A.18.9(4/5):
+
+type Set is tagged private
+      with Constant_Indexing => Constant_Reference,
+           Default_Iterator  => Iterate,
+           Iterator_Element  => Element_Type,
+           Iterator_View     => Stable.Set,
+           Aggregate         => (Empty       => Empty_Set,
+                                 Add_Unnamed => Include),
+           Stable_Properties => (Length,
+                                 Tampering_With_Cursors_Prohibited),
+           Default_Initial_Condition =>
+              Length (Set) = 0 and then
+              (not Tampering_With_Cursors_Prohibited (Set));
+   pragma Preelaborable_Initialization(Set);
 
-Insert before A.18.9 (7.1/5)
+Insert before A.18.9(7.1/5):
 
 function Empty return Set
-      with Post =>
-              not Tampering_With_Elements_Prohibited (Empty'Result) and then
-              not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Length = 0 is (Empty_Set);
+   is (Empty_Set)
+   with Post =>
+           not Tampering_With_Elements_Prohibited (Empty'Result) and then
+           not Tampering_With_Cursors_Prohibited (Empty'Result) and then
+           Length (Empty'Result) = 0;
+
+Modify A.18.9(74.2/5):
+
+   type Set (Base : not null access Hashed_Sets.Set) is
+         tagged limited private
+         with Constant_Indexing => Constant_Reference,
+              Default_Iterator  => Iterate,
+              Iterator_Element  => Element_Type,
+              Aggregate         => (Empty       => Empty[_Set],
+                                    Add_Unnamed => Include),
+              Stable_Properties => (Length),
+              Global => (in Set.Base.all, synchronized out Set.Base.all),
+              Default_Initial_Condition => Length (Set) = 0;
+      pragma Preelaborable_Initialization(Set);
 
-Insert before A.18.10 (11.1/5)
+Insert before A.18.10(11.1/5):
 
 function Empty return Tree
-      with Post =>
-              not Tampering_With_Elements_Prohibited (Empty'Result) and then
-              not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty.Result.Is_Empty is (Empty_Tree);
+   is (Empty_Tree)
+   with Post =>
+           not Tampering_With_Elements_Prohibited (Empty'Result) and then
+           not Tampering_With_Cursors_Prohibited (Empty'Result) and then
+           Node_Count (Empty'Result) = 1;
 
-Insert before A.18.18 (7.1/5)
+Insert before A.18.18(7.1/5):
 
 function Empty return Holder
-      with Post =>
-              not Tampering_With_Elements_Prohibited (Empty'Result) and then
-              not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Is_Empty is (Empty_Holder);
+   is (Empty_Holder)
+   with Post =>
+           not Tampering_With_Elements_Prohibited (Empty'Result) and then
+           not Tampering_With_Cursors_Prohibited (Empty'Result) and then
+           Is_Empty (Empty'Result);
 
-Insert before A.18.20 (7/5)
+Insert before A.18.20(7/5):
 
 The function Empty is replaced by:
 
 function Empty
-     (Capacity   : Count_Type := Implementation Defined) return List
+     (Capacity   : Count_Type := /implementation-defined/) return List
       with Post =>
               Empty'Result.Capacity = Capacity and then
               not Tampering_With_Elements_Prohibited (Empty'Result) and then
               not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Length = 0;
+              Length (Empty'Result) = 0;
 
- Returns a List with a length of 0 and a capacity of Capacity.
+ Returns an empty list.
 
-Insert before A.18.22 (7/5)
+Insert before A.18.22(7/5):
 
 The function Empty is replaced by:
 
 function Empty
-     (Capacity   : Count_Type := Implementation Defined) return Map
+     (Capacity   : Count_Type := /implementation-defined/) return Map
       with Post =>
               Empty'Result.Capacity = Capacity and then
               not Tampering_With_Elements_Prohibited (Empty'Result) and then
               not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Length = 0;
+              Length (Empty'Result) = 0;
 
- Returns a Map with a length of 0 and a capacity of Capacity.
+ Returns an empty map.
 
-Insert before A.18.24 (7/5)
+Insert before A.18.24(7/5):
 
 The function Empty is replaced by:
 
 function Empty
-     (Capacity   : Count_Type := Implementation Defined) return Set
+     (Capacity   : Count_Type := /implementation-defined/) return Set
       with Post =>
               Empty'Result.Capacity = Capacity and then
               not Tampering_With_Elements_Prohibited (Empty'Result) and then
               not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Length = 0;
+              Length (Empty'Result) = 0;
 
- Returns a Set with a length of 0 and a capacity of Capacity.
+ Returns an empty set.
 
-Insert before A.18.25 (8/3)
+Insert before A.18.25(8/3):
 
 The function Empty is replaced by:
 
 function Empty
-     (Capacity   : Count_Type := Implementation Defined) return Tree
+     (Capacity   : Count_Type := /implementation-defined/) return Tree
       with Post =>
               Empty'Result.Capacity = Capacity and then
               not Tampering_With_Elements_Prohibited (Empty'Result) and then
               not Tampering_With_Cursors_Prohibited (Empty'Result) and then
-              Empty'Result.Is_Empty;
+              Node_Count (Empty'Result) = 1;
 
- Returns an Tree with a capacity of Capacity and for which Is_Empty returns True.
+ Returns an empty tree.
 
 !discussion
 
@@ -361,7 +481,7 @@
 ****************************************************************
 
 From: Brad Moore
-Sent: Sunday, June 16, 2019 1:29 AM
+Sent: Sunday, June 16, 2019  1:29 AM
 
 Here is a new AI that we talked about yesterday (AI12-0338?) that defines an 
 Empty function for most of the Ada containers. [This is version /01 of the AI - 
@@ -369,4 +489,52 @@
 
 ****************************************************************
 
+From: Randy Brukardt
+Sent: Tuesday, July 16, 2019  10:25 PM
+
+> Here is a new AI that we talked about yesterday (AI12-0338?) that 
+> defines an Empty function for most of the Ada containers.
+
+Some for the record remarks beyond what was in the meeting notes:
+
+(1) The default parameter for these functions should be "implementation-defined" 
+in italics, to match the usage in 13.7 and A.18.1. (We had talked about the 
+!summary in Warsaw, but not the parameters. Or at least I'm interpreting my 
+notes that way, 'cause what was said in Warsaw is wrong for the parameters.)
+
+(2) The notes say that the postconditions "shouldn't use prefix notation", but 
+note that is necessary in the bounded containers since "Capacity" is a 
+discriminant in those containers.
+
+(3) Brad didn't change the Aggregate definition in those (unbounded) 
+containers that don't have capacities, but that would then mean the Empty 
+function wouldn't be used in aggregates in the bounded forms of those 
+containers. We have to change *all* of the Aggregate aspects to use this 
+function, even the ones that don't have a capacity.
+
+(4) For the unbounded forms with capacities, the requirement is always that 
+the actual capacity is as specified or greater. Empty should be no different.
+Capacity (Empty'Result) >= Capacity should be part of the postcondition.
 
+(5) The description of most of these routines reads something like:
+
+   Returns a List with length = 0 and Capacity as specified.
+
+which is a direct copy of the postcondition. We don't want to repeat the 
+postcondition in English (any one can read it, and it's more formal than 
+English anyway). For this routine, we don't need any formal description at all
+(the postcondition describes the complete contents and properties of the 
+result) - so we can be really vague. I used:
+
+   Returns an empty list.
+
+for every container (changing "list" appropriately, of course). I did this for 
+most of the existing routines (removed duplication with the pre or post 
+conditions), but I didn't bother for a handful where completely new text was 
+needed. But that was more not wanting to make additional work for myself than 
+something to copy.
+
+(6) Fixed all of the dates (it's not 2016!), the missing !standards, and the 
+mis-formatted Modify and Insert After descriptions.
+
+****************************************************************

Questions? Ask the ACAA Technical Agent