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

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

--- ai12s/ai12-0339-1.txt	2019/07/19 04:34:42	1.3
+++ ai12s/ai12-0339-1.txt	2019/07/20 00:59:46	1.4
@@ -1,29 +1,32 @@
-!standard A.18.2(8/5)                                  19-07-16  AI12-0339-1/02
-!standard A.18.2(13/5)
+!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(99/5)
+!standard A.18.2(98.6/5)
 !standard A.18.3(6/5)
-!standard A.18.3(9.1/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(6.1/5)
+!standard A.18.5(7.2/5)
 !standard A.18.5(37.3/5)
-!standard A.18.5(47/5)
+!standard A.18.5(46/2)
 !standard A.18.6(4/5)
-!standard A.18.6(7.1/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(6.1/5)
+!standard A.18.8(8.1/5)
 !standard A.18.8(59.2/5)
-!standard A.18.8(69/5)
+!standard A.18.8(68/2)
 !standard A.18.9(4/5)
-!standard A.18.9(7.1/5)
+!standard A.18.9(9.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.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
@@ -94,7 +97,7 @@
               (not Tampering_With_Cursors_Prohibited (Vector)) and then
               (not Tampering_With_Elements_Prohibited (Vector));
 
-Insert before A.18.2(13/5):
+Insert after A.18.2(12.3/5):
 
 function Empty
      (Capacity   : Count_Type := /implementation-defined/) return Vector
@@ -123,7 +126,7 @@
               Default_Initial_Condition => Length (Vector) = 0;
       pragma Preelaborable_Initialization(Vector);
 
-Insert before A.18.2(99/5):
+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),
@@ -152,7 +155,7 @@
               (not Tampering_With_Cursors_Prohibited (List)) and then
               (not Tampering_With_Elements_Prohibited (List));
 
-Insert before A.18.3(9.1/5):
+Insert after A.18.3(10.2/5):
 
 function Empty return List
    is (Empty_List)
@@ -195,7 +198,7 @@
               (not Tampering_With_Elements_Prohibited (Map));
    pragma Preelaborable_Initialization(Map);
 
-Insert before A.18.5(6.1/5):
+Insert after A.18.5(7.2/5):
 
 function Empty
      (Capacity   : Count_Type := /implementation-defined/) return Map
@@ -220,7 +223,7 @@
               Default_Initial_Condition => Length (Map) = 0;
       pragma Preelaborable_Initialization(Map);
 
-Insert before A.18.5(47/5):
+Insert after A.18.5(46/2):
 
 function Empty (Capacity : Count_Type := /implementation-defined/) return Map
    with Post =>
@@ -228,8 +231,9 @@
            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.
 
+  Returns an empty map.
+
 Modify A.18.6(4/5):
 
 type Map is tagged private
@@ -248,7 +252,7 @@
               (not Tampering_With_Cursors_Prohibited (Map)) and then
               (not Tampering_With_Elements_Prohibited (Map));
 
-Insert before A.18.6(7.1/5):
+Insert after A.18.6(8.2/5):
 
 function Empty return Map
    is (Empty_Map)
@@ -288,10 +292,10 @@
               (not Tampering_With_Cursors_Prohibited (Set));
    pragma Preelaborable_Initialization(Set);
 
-Insert before A.18.8(6.1/5):
+Insert after A.18.8(8.1/5):
 
-function Empty
-     (Capacity   : Count_Type := /implementation-defined/) return Map
+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
@@ -312,12 +316,12 @@
               Default_Initial_Condition => Length (Set) = 0;
       pragma Preelaborable_Initialization(Set);
 
-Insert before A.18.8(69/5):
+Insert after A.18.8(68/2):
 
-function Empty (Capacity : Count_Type := /implementation-defined/) return Set
+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;
  Returns an empty set.
@@ -338,12 +342,11 @@
               (not Tampering_With_Cursors_Prohibited (Set));
    pragma Preelaborable_Initialization(Set);
 
-Insert before A.18.9(7.1/5):
+Insert after A.18.9(9.1/5):
 
 function Empty return 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;
 
@@ -361,7 +364,7 @@
               Default_Initial_Condition => Length (Set) = 0;
       pragma Preelaborable_Initialization(Set);
 
-Insert before A.18.10(11.1/5):
+Insert before A.18.10(15.2/5):
 
 function Empty return Tree
    is (Empty_Tree)
@@ -370,16 +373,25 @@
            not Tampering_With_Cursors_Prohibited (Empty'Result) and then
            Node_Count (Empty'Result) = 1;
 
-Insert before A.18.18(7.1/5):
+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
-           Is_Empty (Empty'Result);
+           Length (Empty'Result) = 0;
 
-Insert before A.18.20(7/5):
+Insert after A.18.20(6/3):
 
 The function Empty is replaced by:
 
@@ -390,8 +402,17 @@
               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:
 
- Returns an empty list.
+   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):
 
@@ -405,10 +426,12 @@
               not Tampering_With_Cursors_Prohibited (Empty'Result) and then
               Length (Empty'Result) = 0;
 
- Returns an empty map.
+Insert after A.18.23(6/3):
 
-Insert before A.18.24(7/5):
+The postcondition of Empty is altered to:
 
+Insert after A.18.24(6/3):
+
 The function Empty is replaced by:
 
 function Empty
@@ -418,10 +441,8 @@
               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 set.
 
-Insert before A.18.25(8/3):
+Insert after A.18.25(6/3):
 
 The function Empty is replaced by:
 
@@ -433,8 +454,6 @@
               not Tampering_With_Cursors_Prohibited (Empty'Result) and then
               Node_Count (Empty'Result) = 1;
 
- Returns an empty tree.
-
 !discussion
 
 We considered whether the Empty function should be added to the various
@@ -443,7 +462,423 @@
 so it seemed best to not attempt to define an empty function for these 
 containers.
 
+!corrigendum A.18.2(8/3)
+
+@drepl
+@xcode<   @b<type> Vector @b<is tagged private>
+      @b<with> Constant_Indexing =@> Constant_Reference,
+           Variable_Indexing =@> Reference,
+           Default_Iterator  =@> Iterate,
+           Iterator_Element  =@> Element_Type;
+   @b<pragma> Preelaborable_Initialization(Vector);>
+@dby
+@xcode<   @b<type> Vector @b<is tagged private>
+      @b<with> 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<and then>
+              (@b<not> Tampering_With_Cursors_Prohibited (Vector)) @b<and then>
+              (@b<not> Tampering_With_Elements_Prohibited (Vector));
+   @b<pragma> Preelaborable_Initialization(Vector);>
+
+!corrigendum A.18.2(12/2)
+
+@dinsa
+@xcode<   @b<function> "=" (Left, Right : Vector) @b<return> Boolean;>
+@dinst
+@xcode<   @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
+      @b<return> Vector
+      @b<with> Pre  =@> (@b<if> Capacity @> Maximum_Length @b<then raise> Constraint_Error),
+           Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
+                   @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                   @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                   Length (Empty'Result) = 0;>
+
+!comment A.18.2(78.2/5) not in corrigendum text.
+
+!corrigendum A.18.2(98/3)
+
+@dinsa
+@xindent<If Left and Right denote the same vector object, then the function 
+returns True. If Left and Right have different lengths, then the function 
+returns False. Otherwise, it compares each element in Left to the 
+corresponding element in Right using the generic formal equality operator. 
+If any such comparison returns False, the function returns False; otherwise,
+it returns True. Any exception raised during evaluation of element equality is 
+propagated.
+@dinst
+@xcode<@b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
+   @b<return> Vector
+   @b<with> Pre  =@> (@b<if> Capacity @> Maximum_Length @b<then raise> Constraint_Error),
+        Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
+                @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                Length (Empty'Result) = 0;>
+
+@xindent<Returns an empty vector.>
+
+
+!corrigendum A.18.3(6/3)
+
+@drepl
+@xcode<   @b<type> List @b<is tagged private>
+      @b<with> Constant_Indexing =@> Constant_Reference,
+           Variable_Indexing =@> Reference,
+           Default_Iterator  =@> Iterate,
+           Iterator_Element  =@> Element_Type;
+   @b<pragma> Preelaborable_Initialization(List);>
+@dby
+@xcode<   @b<type> List @b<is tagged private>
+      @b<with> 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<and then>
+              (@b<not> Tampering_With_Cursors_Prohibited (List)) @b<and then>
+              (@b<not> Tampering_With_Elements_Prohibited (List));
+   @b<pragma> Preelaborable_Initialization(List);>
+
+!corrigendum A.18.3(10/2)
+
+@dinsa
+@xcode<   @b<function> "=" (Left, Right : List) @b<return> Boolean;>
+@dinst
+@xcode<   @b<function> Empty @b<return> List
+      @b<is> (Empty_List)
+      @b<with> Post =@> @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                  @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                  Length (Empty'Result) = 0;>
+
+!comment  A.18.3(50.2/5) not in corrigendum text.
+
+
+!corrigendum A.18.5(3/2)
+
+@drepl
+@xcode<   @b<type> Map @b<is tagged private>
+      @b<with> Constant_Indexing =@> Constant_Reference,
+           Variable_Indexing =@> Reference,
+           Default_Iterator  =@> Iterate,
+           Iterator_Element  =@> Element_Type;
+   @b<pragma> Preelaborable_Initialization(Map);>
+@dby
+@xcode<   @b<type> Map @b<is tagged private>
+      @b<with> 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<and then>
+              (@b<not> Tampering_With_Cursors_Prohibited (Map)) @b<and then>
+              (@b<not> Tampering_With_Elements_Prohibited (Map));
+   @b<pragma> Preelaborable_Initialization(Map);>
+
+!corrigendum A.18.5(7/2)
+
+@dinsa
+@xcode<   @b<function> "=" (Left, Right : Map) @b<return> Boolean;>
+@dinst
+@xcode<   @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
+      @b<return> Map
+      @b<with> Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
+                   @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                   @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                   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<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
+   @b<return> Map
+   @b<with> Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
+                @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                Length (Empty'Result) = 0;>
+
+@xindent<Returns an empty map.>
+
+!corrigendum A.18.6(4/3)
+
+@drepl
+@xcode<   @b<type> Map @b<is tagged private>
+      @b<with> Constant_Indexing =@> Constant_Reference,
+           Variable_Indexing =@> Reference,
+           Default_Iterator  =@> Iterate,
+           Iterator_Element  =@> Element_Type;
+   @b<pragma> Preelaborable_Initialization(Map);>
+@dby
+@xcode<   @b<type> Map @b<is tagged private>
+      @b<with> 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<and then>
+              (@b<not> Tampering_With_Cursors_Prohibited (Map)) @b<and then>
+              (@b<not> Tampering_With_Elements_Prohibited (Map));
+   @b<pragma> Preelaborable_Initialization(Map);>
+
+!corrigendum A.18.6(7/2)
+
+@dinsa
+@xcode<   @b<function> "=" (Left, Right : Map) @b<return> Boolean;>
+@dinst
+@xcode<   @b<function> Empty @b<return> Map
+      @b<is> (Empty_Map)
+      @b<with> Post =@> @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                  @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                  Length (Empty'Result) = 0;>
+
+!comment A.18.6(51.4/5) not in corrigendum text.
+
+!corrigendum A.18.8(3/3)
+
+@drepl
+@xcode<   @b<type> Set @b<is tagged private>
+      @b<with> Constant_Indexing =@> Constant_Reference,
+           Default_Iterator  =@> Iterate,
+           Iterator_Element  =@> Element_Type;
+   @b<pragma> Preelaborable_Initialization(Set);>
+@dby
+@xcode<   @b<type> Set @b<is tagged private>
+      @b<with> 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<and then>
+              (@b<not> Tampering_With_Cursors_Prohibited (Set));
+   @b<pragma> Preelaborable_Initialization(Set);>
+
+!corrigendum A.18.8(8/2)
+
+@dinsa
+@xcode<   @b<function> Equivalent_Sets (Left, Right : Set) @b<return> Boolean;>
+@dinst
+@xcode<   @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
+      @b<return> Set
+      @b<with> Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
+                   @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                   Length (Empty'Result) = 0;>
+
+!comment A.18.8(59.2/5) not in corrigendum text.
+
+!corrigendum A.18.8(68/2)
+
+@dinsa
+@xindent<Which elements are the first element and the last element of a set, 
+and which element is the successor of a given element, are unspecified, other
+than the general semantics described in A.18.7.>
+@dinst
+@xcode<@b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
+   @b<return> Set
+   @b<with> Post =@> Capacity (Empty'Result) @>= Capacity @b<and then>
+                @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                Length (Empty'Result) = 0;>
+
+@xindent<Returns an empty set.>
+
+
+!corrigendum A.18.9(4/3)
+
+@drepl
+@xcode<   @b<type> Set @b<is tagged private>
+      @b<with> Constant_Indexing =@> Constant_Reference,
+           Default_Iterator  =@> Iterate,
+           Iterator_Element  =@> Element_Type;
+   @b<pragma> Preelaborable_Initialization(Set);>
+@dby
+@xcode<   @b<type> Set @b<is tagged private>
+      @b<with> 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<and then>
+              (@b<not> Tampering_With_Cursors_Prohibited (Set));
+   @b<pragma> Preelaborable_Initialization(Set);>
+
+!corrigendum A.18.9(9/2)
+
+@dinsa
+@xcode<   @b<function> Equivalent_Sets (Left, Right : Set) @b<return> Boolean;>
+@dinst
+@xcode<   @b<function> Empty @b<return> Set
+      @b<is> (Empty_Set)
+      @b<with> Post =@> @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                  @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                  Length (Empty'Result) = 0;>
+
+!comment A.18.9(74.2/5) not in corrigendum text.
+
+
+!corrigendum A.18.10(15/3)
+
+@dinsa
+@xcode<   @b<function> "=" (Left, Right : Tree) @b<return> Boolean;>
+@dinst
+@xcode<   @b<function> Empty @b<return> Tree
+      @b<is> (Empty_Tree)
+      @b<with> Post =@> @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                  @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                  Node_Count (Empty'Result) = 1;>
+
+
+!corrigendum A.18.18(8/3)
+
+@dinsa
+@xcode<   @b<function> "=" (Left, Right : Holder) @b<return> Boolean;>
+@dinst
+@xcode<   @b<function> Empty @b<return> Holder
+      @b<is> (Empty_Holder)
+      @b<with> Post =@> @b<not> Tampering_With_The_Element_Prohibited (Empty'Result) @b<and then>
+                  Is_Empty (Empty'Result);>
+
+!corrigendum A.18.19(6/3)
+
+@dinsa
+@xbullet<The type Vector needs finalization if and only if type Element_Type 
+needs finalization.>
+@dinss
+@xbullet<In function Empty, the postcondition is altered to:>
+
+@xcode<   Post =@> Empty'Result.Capacity = Capacity @b<and then>
+           @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+           @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+           Length (Empty'Result) = 0;>
+
+!corrigendum A.18.20(6/3)
+
+@dinsa
+@xbullet<The type List needs finalization if and only if type Element_Type 
+needs finalization.>
+@dinss
+@xbullet<The function Empty is replaced by:>
+
+@xcode<   @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
+      @b<return> List
+      @b<with> Post =@> Empty'Result.Capacity = Capacity @b<and then>
+                   @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                   @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                   Length (Empty'Result) = 0;>
+
+!corrigendum A.18.21(6/3)
+
+@dinsa
+@xbullet<The type Map needs finalization if and only if type Key_Type or 
+type Element_Type needs finalization.>
+@dinss
+@xbullet<In function Empty, the postcondition is altered to:>
+
+@xcode<   Post =@> Empty'Result.Capacity = Capacity @b<and then>
+           Empty'Result.Modulus = Default_Modulus (Capacity) @b<and then>
+           @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+           @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+           Length (Empty'Result) = 0;>
+
+!corrigendum A.18.22(6/3)
+
+@dinsa
+@xbullet<The type Map needs finalization if and only if type Key_Type or 
+type Element_Type needs finalization.>
+@dinss
+@xbullet<The function Empty is replaced by:>
+
+@xcode<   @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
+      @b<return> Map
+      @b<with> Post =@> Empty'Result.Capacity = Capacity @b<and then>
+                   @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                   @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                   Length (Empty'Result) = 0;>
+
+!corrigendum A.18.23(6/3)
+
+@dinsa
+@xbullet<The type Set needs finalization if and only if  
+type Element_Type needs finalization.>
+@dinss
+@xbullet<In function Empty, the postcondition is altered to:>
+
+@xcode<   Post =@> Empty'Result.Capacity = Capacity @b<and then>
+           Empty'Result.Modulus = Default_Modulus (Capacity) @b<and then>
+           @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+           Length (Empty'Result) = 0;>
+
+!corrigendum A.18.24(6/3)
+
+@dinsa
+@xbullet<The type Set needs finalization if and only if  
+type Element_Type needs finalization.>
+@dinss
+@xbullet<The function Empty is replaced by:>
+
+@xcode<   @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
+      @b<return> Set
+      @b<with> Post =@> Empty'Result.Capacity = Capacity @b<and then>
+                   @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                   Length (Empty'Result) = 0;>
+
+!corrigendum A.18.25(6/3)
+
+@dinsa
+@xbullet<The type Tree needs finalization if and only if type Element_Type needs 
+finalization.>
+@dinss
+@xbullet<The function Empty is replaced by:>
+
+@xcode<   @b<function> Empty (Capacity : Count_Type := @ft<@i<implementation-defined>>)
+      @b<return> Tree
+      @b<with> Post =@> Empty'Result.Capacity = Capacity @b<and then>
+                   @b<not> Tampering_With_Elements_Prohibited (Empty'Result) @b<and then>
+                   @b<not> Tampering_With_Cursors_Prohibited (Empty'Result) @b<and then>
+                   Node_Count (Empty'Result) = 1;>
+
 !ASIS
+
+No ASIS effect.
 
 !ACATS test
 

Questions? Ask the ACAA Technical Agent