!standard A.18.2(8/5) 19-07-19 AI12-0339-1/03 !standard A.18.2(12.3/5) !standard A.18.2(78.2/5) !standard A.18.2(98.6/5) !standard A.18.3(6/5) !standard A.18.3(10.2/5) !standard A.18.3(50.2/5) !standard A.18.5(3/5) !standard A.18.5(7.2/5) !standard A.18.5(37.3/5) !standard A.18.5(46/2) !standard A.18.6(4/5) !standard A.18.6(8.2/5) !standard A.18.6(51.4/5) !standard A.18.8(3/5) !standard A.18.8(8.1/5) !standard A.18.8(59.2/5) !standard A.18.8(68/2) !standard A.18.9(4/5) !standard A.18.9(9.1/5) !standard A.18.9(74.2/5) !standard A.18.10(15.2/5) !standard A.18.18(8.1/5) !standard A.18.19(6.1/5) !standard A.18.20(6/3) !standard A.18.21(6/3) !standard A.18.22(6/3) !standard A.18.23(6/3) !standard A.18.24(6/3) !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 !difficulty Easy !subject Empty function for Container aggregates !summary 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 an implementation-defined default value. For other container types that do not have the notion of capacity, the Empty function is parameterless. !problem AI12-0212-1 defines the aggregate aspect, which adds the capability of specifying container aggregates. One part of the aggregate aspect specification, Empty, identifies the name that denotes a constant of the container type, or a function with a result of the container type that is used to produce an empty container object. Currently, the containers name the preexisting constant object defined in Ada 2012, for Empty. However, these constant objects, for container types that have the notion of capacity, have a capacity of 0 elements, but container aggregates often are used to create container aggregates that have 1 or more elements. It would be more efficient, for cases where multiple elements are needed, if the constructed container object was initially sized to have a capacity that could accommodate all the elements associated with the aggregate. It can be very inefficient for a container such as a vector container to start with 0 capacity, and increase the capacity as each element of the aggregate is inserted into the container. Should a mechanism be provided to allow container objects to be initially sized to a given capacity, allowing for more efficient construction of container objects? (Yes.) !proposal We propose to add an Empty function to all the containers that have the Aggregate aspect, and modify the Aggregate aspect such that the Empty field denotes the new function instead of the original constant object. For those containers that have the notion of capacity, the Empty function will accept a Capacity parameter to indicate the initial capacity of the container object of the result of the Empty function. The Capacity parameter will have a system defined default value. Otherwise, for containers that do not have the notion of capacity, the Empty function will be a parameter-less function, that returns a container object with zero elements. !wording Modify A.18.2(8/5): type Vector is tagged private with Constant_Indexing => Constant_Reference, Variable_Indexing => Reference, Default_Iterator => Iterate, Iterator_Element => Element_Type, Iterator_View => Stable.Vector, Aggregate => (Empty => Empty[_Vector], Add_Unnamed => Append_One, New_Indexed => New_Vector, Assign_Indexed => Replace_Element), Stable_Properties => (Length, Capacity, Tampering_With_Cursors_Prohibited, Tampering_With_Elements_Prohibited), Default_Initial_Condition => Length (Vector) = 0 and then (not Tampering_With_Cursors_Prohibited (Vector)) and then (not Tampering_With_Elements_Prohibited (Vector)); Insert after A.18.2(12.3/5): function Empty (Capacity : Count_Type := /implementation-defined/) return Vector with Pre => (if Capacity > Maximum_Length then raise Constraint_Error), Post => Capacity (Empty'Result) >= Capacity and then 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.2(78.2/5): type Vector (Base : not null access Vectors.Vector) is tagged limited private with Constant_Indexing => Constant_Reference, Variable_Indexing => Reference, Default_Iterator => Iterate, Iterator_Element => Element_Type, Aggregate => (Empty => Empty[_Vector], Add_Unnamed => Append_One, New_Indexed => New_Vector, Assign_Indexed => Replace_Element), Stable_Properties => (Length, Capacity), Global => (in Vector.Base.all, synchronized out Vector.Base.all), Default_Initial_Condition => Length (Vector) = 0; pragma Preelaborable_Initialization(Vector); Insert after A.18.2(98.6/5): function Empty (Capacity : Count_Type := /implementation-defined/) return Vector with Pre => (if Capacity > Maximum_Length then raise Constraint_Error), Post => Capacity (Empty'Result) = Capacity and then not Tampering_With_Elements_Prohibited (Empty'Result) and then not Tampering_With_Cursors_Prohibited (Empty'Result) and then 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 after A.18.3(10.2/5): function Empty return 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): 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)); pragma Preelaborable_Initialization(Map); Insert after A.18.5(7.2/5): function Empty (Capacity : Count_Type := /implementation-defined/) return Map with Post => Capacity (Empty'Result) >= Capacity and then 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.5(37.3/5): type Map (Base : not null access Hashed_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); Insert after A.18.5(46/2): function Empty (Capacity : Count_Type := /implementation-defined/) return Map with Post => Capacity (Empty'Result) >= Capacity and then not Tampering_With_Elements_Prohibited (Empty'Result) and then not Tampering_With_Cursors_Prohibited (Empty'Result) and then Length (Empty'Result) = 0; Returns an empty map. 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 after A.18.6(8.2/5): function Empty return 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): 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 after A.18.8(8.1/5): function Empty (Capacity : Count_Type := /implementation-defined/) return Set with Post => Capacity (Empty'Result) = Capacity and then 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.8(59.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 after A.18.8(68/2): function Empty (Capacity : Count_Type := /implementation-defined/) return Set with Post => Capacity (Empty'Result) >= Capacity and then not Tampering_With_Cursors_Prohibited (Empty'Result) and then 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 after A.18.9(9.1/5): function Empty return Set is (Empty_Set) with Post => 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(15.2/5): function Empty return 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 after A.18.18(8.1/5): function Empty return Holder is (Empty_Holder) with Post => not Tampering_With_The_Element_Prohibited (Empty'Result) and then Is_Empty (Empty'Result); Insert after A.18.19(6.1/5): The postcondition of Empty is altered to: 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 Length (Empty'Result) = 0; Insert after A.18.20(6/3): The function Empty is replaced by: function Empty (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 Length (Empty'Result) = 0; Insert after A.18.21(6/3): The postcondition of Empty is altered to: with Post => Empty'Result.Capacity = Capacity and then Empty'Result.Modulus = Default_Modulus (Capacity) and then not Tampering_With_Elements_Prohibited (Empty'Result) and then not Tampering_With_Cursors_Prohibited (Empty'Result) and then Length (Empty'Result) = 0; Insert before A.18.22(7/5): The function Empty is replaced by: function Empty (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 Length (Empty'Result) = 0; Insert after A.18.23(6/3): The postcondition of Empty is altered to: Insert after A.18.24(6/3): The function Empty is replaced by: function Empty (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 Length (Empty'Result) = 0; Insert after A.18.25(6/3): The function Empty is replaced by: function Empty (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 Node_Count (Empty'Result) = 1; !discussion We considered whether the Empty function should be added to the various synchronized queue containers. Those containers do not define stable views, do not have the Aggregate aspect, nor do they define an Empty_Queue object, so it seemed best to not attempt to define an empty function for these containers. !corrigendum A.18.2(8/3) @drepl @xcode< @b Vector @b @b Constant_Indexing =@> Constant_Reference, Variable_Indexing =@> Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type; @b Preelaborable_Initialization(Vector);> @dby @xcode< @b Vector @b @b Constant_Indexing =@> Constant_Reference, Variable_Indexing =@> Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type, Iterator_View =@> Stable.Vector, Aggregate =@> (Empty =@> Empty, Add_Unnamed =@> Append_One, New_Indexed =@> New_Vector, Assign_Indexed =@> Replace_Element), Stable_Properties =@> (Length, Capacity, Tampering_With_Cursors_Prohibited, Tampering_With_Elements_Prohibited), Default_Initial_Condition =@> Length (Vector) = 0 @b (@b Tampering_With_Cursors_Prohibited (Vector)) @b (@b Tampering_With_Elements_Prohibited (Vector)); @b Preelaborable_Initialization(Vector);> !corrigendum A.18.2(12/2) @dinsa @xcode< @b "=" (Left, Right : Vector) @b Boolean;> @dinst @xcode< @b Empty (Capacity : Count_Type := @ft<@i>) @b Vector @b Pre =@> (@b Capacity @> Maximum_Length @b Constraint_Error), Post =@> Capacity (Empty'Result) @>= Capacity @b @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !comment A.18.2(78.2/5) not in corrigendum text. !corrigendum A.18.2(98/3) @dinsa @xindent Empty (Capacity : Count_Type := @ft<@i>) @b Vector @b Pre =@> (@b Capacity @> Maximum_Length @b Constraint_Error), Post =@> Capacity (Empty'Result) @>= Capacity @b @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> @xindent !corrigendum A.18.3(6/3) @drepl @xcode< @b List @b @b Constant_Indexing =@> Constant_Reference, Variable_Indexing =@> Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type; @b Preelaborable_Initialization(List);> @dby @xcode< @b List @b @b Constant_Indexing =@> Constant_Reference, Variable_Indexing =@> Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type, Iterator_View =@> Stable.List, Aggregate =@> (Empty =@> Empty, Add_Unnamed =@> Append), Stable_Properties =@> (Length, Tampering_With_Cursors_Prohibited, Tampering_With_Elements_Prohibited), Default_Initial_Condition =@> Length (List) = 0 @b (@b Tampering_With_Cursors_Prohibited (List)) @b (@b Tampering_With_Elements_Prohibited (List)); @b Preelaborable_Initialization(List);> !corrigendum A.18.3(10/2) @dinsa @xcode< @b "=" (Left, Right : List) @b Boolean;> @dinst @xcode< @b Empty @b List @b (Empty_List) @b Post =@> @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !comment A.18.3(50.2/5) not in corrigendum text. !corrigendum A.18.5(3/2) @drepl @xcode< @b Map @b @b Constant_Indexing =@> Constant_Reference, Variable_Indexing =@> Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type; @b Preelaborable_Initialization(Map);> @dby @xcode< @b Map @b @b Constant_Indexing =@> Constant_Reference, Variable_Indexing =@> Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type, Iterator_View =@> Stable.Map, Aggregate =@> (Empty =@> Empty, Add_Named =@> Insert), Stable_Properties =@> (Length, Tampering_With_Cursors_Prohibited, Tampering_With_Elements_Prohibited), Default_Initial_Condition =@> Length (Map) = 0 @b (@b Tampering_With_Cursors_Prohibited (Map)) @b (@b Tampering_With_Elements_Prohibited (Map)); @b Preelaborable_Initialization(Map);> !corrigendum A.18.5(7/2) @dinsa @xcode< @b "=" (Left, Right : Map) @b Boolean;> @dinst @xcode< @b Empty (Capacity : Count_Type := @ft<@i>) @b Map @b Post =@> Capacity (Empty'Result) @>= Capacity @b @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !comment A.18.5(37.3/5) not in corrigendum text. !corrigendum A.18.5(46/2) @dinsa Which nodes are the first node and the last node of a map, and which node is the successor of a given node, are unspecified, other than the general semantics described in A.18.4. @dinss @xcode<@b Empty (Capacity : Count_Type := @ft<@i>) @b Map @b Post =@> Capacity (Empty'Result) @>= Capacity @b @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> @xindent !corrigendum A.18.6(4/3) @drepl @xcode< @b Map @b @b Constant_Indexing =@> Constant_Reference, Variable_Indexing =@> Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type; @b Preelaborable_Initialization(Map);> @dby @xcode< @b Map @b @b Constant_Indexing =@> Constant_Reference, Variable_Indexing =@> Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type, Iterator_View =@> Stable.Map, Aggregate =@> (Empty =@> Empty, Add_Named =@> Insert), Stable_Properties =@> (Length, Tampering_With_Cursors_Prohibited, Tampering_With_Elements_Prohibited), Default_Initial_Condition =@> Length (Map) = 0 @b (@b Tampering_With_Cursors_Prohibited (Map)) @b (@b Tampering_With_Elements_Prohibited (Map)); @b Preelaborable_Initialization(Map);> !corrigendum A.18.6(7/2) @dinsa @xcode< @b "=" (Left, Right : Map) @b Boolean;> @dinst @xcode< @b Empty @b Map @b (Empty_Map) @b Post =@> @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !comment A.18.6(51.4/5) not in corrigendum text. !corrigendum A.18.8(3/3) @drepl @xcode< @b Set @b @b Constant_Indexing =@> Constant_Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type; @b Preelaborable_Initialization(Set);> @dby @xcode< @b Set @b @b Constant_Indexing =@> Constant_Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type, Iterator_View =@> Stable.Set, Aggregate =@> (Empty =@> Empty, Add_Unnamed =@> Include), Stable_Properties =@> (Length, Tampering_With_Cursors_Prohibited), Default_Initial_Condition =@> Length (Set) = 0 @b (@b Tampering_With_Cursors_Prohibited (Set)); @b Preelaborable_Initialization(Set);> !corrigendum A.18.8(8/2) @dinsa @xcode< @b Equivalent_Sets (Left, Right : Set) @b Boolean;> @dinst @xcode< @b Empty (Capacity : Count_Type := @ft<@i>) @b Set @b Post =@> Capacity (Empty'Result) @>= Capacity @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !comment A.18.8(59.2/5) not in corrigendum text. !corrigendum A.18.8(68/2) @dinsa @xindent @dinst @xcode<@b Empty (Capacity : Count_Type := @ft<@i>) @b Set @b Post =@> Capacity (Empty'Result) @>= Capacity @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> @xindent !corrigendum A.18.9(4/3) @drepl @xcode< @b Set @b @b Constant_Indexing =@> Constant_Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type; @b Preelaborable_Initialization(Set);> @dby @xcode< @b Set @b @b Constant_Indexing =@> Constant_Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type, Iterator_View =@> Stable.Set, Aggregate =@> (Empty =@> Empty, Add_Unnamed =@> Include), Stable_Properties =@> (Length, Tampering_With_Cursors_Prohibited), Default_Initial_Condition =@> Length (Set) = 0 @b (@b Tampering_With_Cursors_Prohibited (Set)); @b Preelaborable_Initialization(Set);> !corrigendum A.18.9(9/2) @dinsa @xcode< @b Equivalent_Sets (Left, Right : Set) @b Boolean;> @dinst @xcode< @b Empty @b Set @b (Empty_Set) @b Post =@> @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !comment A.18.9(74.2/5) not in corrigendum text. !corrigendum A.18.10(15/3) @dinsa @xcode< @b "=" (Left, Right : Tree) @b Boolean;> @dinst @xcode< @b Empty @b Tree @b (Empty_Tree) @b Post =@> @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Node_Count (Empty'Result) = 1;> !corrigendum A.18.18(8/3) @dinsa @xcode< @b "=" (Left, Right : Holder) @b Boolean;> @dinst @xcode< @b Empty @b Holder @b (Empty_Holder) @b Post =@> @b Tampering_With_The_Element_Prohibited (Empty'Result) @b Is_Empty (Empty'Result);> !corrigendum A.18.19(6/3) @dinsa @xbullet @dinss @xbullet @xcode< Post =@> Empty'Result.Capacity = Capacity @b @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !corrigendum A.18.20(6/3) @dinsa @xbullet @dinss @xbullet @xcode< @b Empty (Capacity : Count_Type := @ft<@i>) @b List @b Post =@> Empty'Result.Capacity = Capacity @b @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !corrigendum A.18.21(6/3) @dinsa @xbullet @dinss @xbullet @xcode< Post =@> Empty'Result.Capacity = Capacity @b Empty'Result.Modulus = Default_Modulus (Capacity) @b @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !corrigendum A.18.22(6/3) @dinsa @xbullet @dinss @xbullet @xcode< @b Empty (Capacity : Count_Type := @ft<@i>) @b Map @b Post =@> Empty'Result.Capacity = Capacity @b @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !corrigendum A.18.23(6/3) @dinsa @xbullet @dinss @xbullet @xcode< Post =@> Empty'Result.Capacity = Capacity @b Empty'Result.Modulus = Default_Modulus (Capacity) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !corrigendum A.18.24(6/3) @dinsa @xbullet @dinss @xbullet @xcode< @b Empty (Capacity : Count_Type := @ft<@i>) @b Set @b Post =@> Empty'Result.Capacity = Capacity @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Length (Empty'Result) = 0;> !corrigendum A.18.25(6/3) @dinsa @xbullet @dinss @xbullet @xcode< @b Empty (Capacity : Count_Type := @ft<@i>) @b Tree @b Post =@> Empty'Result.Capacity = Capacity @b @b Tampering_With_Elements_Prohibited (Empty'Result) @b @b Tampering_With_Cursors_Prohibited (Empty'Result) @b Node_Count (Empty'Result) = 1;> !ASIS No ASIS effect. !ACATS test ACATS B and C-Tests are needed to check that the new capabilities are supported. !appendix From: Tucker Taft Sent: Wednesday, June 12, 2019 12:23 AM A comment from an GNAT user mentioned that we have not provided in Ada 202X "Empty" functions that take a capacity, to support the capability available to container aggregates. Perhaps we should do so to make the container aggregate construction process more efficient! Seems particularly important for vectors, but could be useful for any case where the compiler can predict the size of the aggregate being created. **************************************************************** From: Randy Brukardt Sent: Wednesday, June 12, 2019 7:59 AM Seems like it would be necessary for bounded containers, esp. if someone wanted to use :=. **************************************************************** From: Tucker Taft Sent: Wednesday, June 12, 2019 9:47 AM It seems important for dynamic containers as well, from an efficiency point of view. Otherwise the container might be expanded for each element, or over-expanded well beyond the size needed. **************************************************************** From: Brad Moore 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 - Editor.] **************************************************************** 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. **************************************************************** From: Brad Moore Sent: wednesday, July 17, 2019 10:02 PM Your edits look good to me, Thanks, Randy! ****************************************************************