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

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

--- ai12s/ai12-0112-1.txt	2019/02/14 05:25:23	1.14
+++ ai12s/ai12-0112-1.txt	2019/02/21 05:29:33	1.15
@@ -110,9 +110,9 @@
                                  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));
+           Default_Initial_Condition => Length (Vector) = 0 and then
+                                        (not Tampering_With_Cursors_Prohibited (Vector)) and then
+                                        (not Tampering_With_Elements_Prohibited (Vector));
    pragma Preelaborable_Initialization(Vector);
 
    type Cursor is private;
@@ -169,7 +169,8 @@
 raised during evaluation of element equality is propagated.
 
 New
-function Tampering_With_Cursors_Prohibited (Container : Vector) return Boolean
+function Tampering_With_Cursors_Prohibited 
+   (Container : Vector) return Boolean
    with Nonblocking => True,
         Global => null;
 New
@@ -179,7 +180,8 @@
 cursors, so we have this function reflect that.
 
 New
-function Tampering_With_Elements_Prohibited (Container : Vector) return Boolean
+function Tampering_With_Elements_Prohibited 
+   (Container : Vector) return Boolean
    with Nonblocking => True,
         Global => null;
 New
@@ -187,7 +189,9 @@
 and returns False otherwise.
 
 New
-function Maximum_Length return Count_Type;
+function Maximum_Length return Count_Type
+   with Nonblocking => True,
+        Global => null;
 New
 Returns the maximum Length of a Vector, based on the index type.
 
@@ -202,8 +206,9 @@
 preconditions defined below (on "&" and Insert) will raise Constraint_Error if 
 the length of the container exceeds Count_Type'Last, while that would raise 
 Capacity_Error in Ada 2005/2012. This seems exceedingly unlikely to actually 
-happen, such that it isn't worth having two conditions to avoid changing the
-exception.]
+happen, as Count_Type'Last is likely to be 2**31-1, and such a vector probably
+would overflow memory long before this problem occurred. As such, it isn't 
+worth having two conditions to avoid changing the exception.]
 
 100/2+
 function To_Vector (Length : Count_Type) return Vector
@@ -230,16 +235,13 @@
 
 104/2+
 function "&" (Left, Right : Vector) return Vector
-   with Pre  => (if Length (Left) + Length (Right) > Maximum_Length 
+   with Pre  => (if Length (Left) > Maximum_Length - Length (Right) 
                  then raise Constraint_Error),
         Post => Length (Vectors."&"'Result) = Length (Left) + Length (Right) and then
                 not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
                 not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then
                 Vectors."&"'Result.Capacity >= Length (Left) + Length (Right);
 
-[Author's note: The precondition can overflow, but if that happens 
-Constraint_Error would be raised just as we want anyway.]
-
 105/2
 Returns a vector comprising the elements of Left followed by the elements of
 Right.
@@ -247,7 +249,7 @@
 106/2+
 function "&" (Left  : Vector;
               Right : Element_Type) return Vector
-   with Pre  => (if Length (Left) + 1 > Maximum_Length 
+   with Pre  => (if Length (Left) > Maximum_Length - 1
                  then raise Constraint_Error),
         Post => Vectors."&"'Result.Length = Length (Left) + 1 and then
                 not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
@@ -259,7 +261,7 @@
 108/2+
 function "&" (Left  : Element_Type;
               Right : Vector) return Vector
-   with Pre  => (if Length (Right) + 1 > Maximum_Length 
+   with Pre  => (if Length (Right) > Maximum_Length - 1
                  then raise Constraint_Error),
         Post => Length (Vectors."&"'Result) = Length (Right) + 1 and then
                 not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
@@ -529,10 +531,12 @@
 type Constant_Reference_Type
       (Element : not null access constant Element_Type) is private
    with Implicit_Dereference => Element,
+        Global => in out access Vector,
         Default_Initial_Condition => (raise Program_Error);
 147.2/3
 type Reference_Type (Element : not null access Element_Type) is private
    with Implicit_Dereference => Element,
+        Global => in out access Vector,
         Default_Initial_Condition => (raise Program_Error);
 147.3/3
 The types Constant_Reference_Type and Reference_Type need finalization.
@@ -543,9 +547,15 @@
 function Constant_Reference (Container : aliased in Vector;
                              Index     : in Index_Type)
    return Constant_Reference_Type
-   with Pre  => (if Index not in First_Index (Container) .. Last_Index (Container)
-                       then raise Constraint_Error),
+   with Pre    => (if Index not in First_Index (Container) .. Last_Index (Container)
+                   then raise Constraint_Error),
+        Post   => Tampering_With_Cursors_Prohibited (Container),
         Global => null;
+
+[Author's note: We have to use Tampering_With_Cursors_Prohibited here, as 
+Tampering_With_Elements_Prohibited is always False. We'll use the right function in
+the indefinite containers.]
+
 147.6/3
 This function (combined with the Constant_Indexing and Implicit_Dereference
 aspects) provides a convenient way to gain read access to an individual element
@@ -560,8 +570,10 @@
 function Reference (Container : aliased in out Vector;
                     Index     : in Index_Type)
    return Reference_Type
-   with Pre  => (if Index not in First_Index (Container) .. Last_Index (Container)
-                 then raise Constraint_Error);
+   with Pre    => (if Index not in First_Index (Container) .. Last_Index (Container)
+                   then raise Constraint_Error),
+        Post   => Tampering_With_Cursors_Prohibited (Container),
+        Global => null;
 147.9/3
 This function (combined with the Variable_Indexing and Implicit_Dereference
 aspects) provides a convenient way to gain read and write access to an
@@ -579,9 +591,10 @@
 function Constant_Reference (Container : aliased in Vector;
                              Position  : in Cursor)
    return Constant_Reference_Type
-   with Pre => (if Position = No_Element then raise Constraint_Error) and then
-               (if not Has_Element (Container, Position)
-                then raise Program_Error),
+   with Pre    => (if Position = No_Element then raise Constraint_Error) and then
+                  (if not Has_Element (Container, Position)
+                   then raise Program_Error),
+        Post   => Tampering_With_Cursors_Prohibited (Container),
         Global => null;
 147.13/3
 This function (combined with the Constant_Indexing and Implicit_Dereference
@@ -597,9 +610,11 @@
 function Reference (Container : aliased in out Vector;
                     Position  : in Cursor)
    return Reference_Type is
-   with Pre => (if Position = No_Element then raise Constraint_Error) and then
-               (if not Has_Element (Container, Position)
-                then raise Program_Error);
+   with Pre    => (if Position = No_Element then raise Constraint_Error) and then
+                  (if not Has_Element (Container, Position)
+                   then raise Program_Error);
+        Post   => Tampering_With_Cursors_Prohibited (Container),
+        Global => null;
 147.16/3
 This function (combined with the Variable_Indexing and Implicit_Dereference
 aspects) provides a convenient way to gain read and write access to an
@@ -616,7 +631,7 @@
 147.19/3+
 procedure Assign (Target : in out Vector; Source : in Vector)
    with Pre  => (if Tampering_With_Cursors_Prohibited (Target)
-                       then raise Program_Error),
+                 then raise Program_Error),
         Post => Length (Source) = Length (Target),
                 Capacity (Target) >= Length (Target);
 147.20/3
@@ -666,7 +681,7 @@
                  then raise Program_Error) and then
                 (if Before not in First_Index (Container) .. Last_Index (Container) + 1
                  then raise Constraint_Error) and then
-                (if Length (Container) + Length (New_Item) > Maximum_Length
+                (if Length (Container) > Maximum_Length - Length (New_Item) 
                  then raise Constraint_Error),
 [Note: This length calculation might overflow, but if it does, that's OK, as the rules
 require Constraint_Error to be raised in this case.]
@@ -692,7 +707,7 @@
                     Before /= No_Element and then 
                     (not Has_Element (Container, Before))
                  then raise Program_Error) and then
-                (if Length (Container) + Length (New_Item) > Maximum_Length
+                (if Length (Container) > Maximum_Length - Length (New_Item)
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Length (New_Item) = Length (Container),
                 Capacity (Container) >= Length (Container);
@@ -712,7 +727,7 @@
                 (if Before /= No_Element and then 
                  (not Has_Element (Container, Before))
                  then raise Program_Error) and then
-                (if Length (Container) + Length (New_Item) > Maximum_Length
+                (if Length (Container) > Maximum_Length - Length (New_Item)
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
                 Has_Element (Container, Position) and then
@@ -731,7 +746,7 @@
                  then raise Program_Error) and then
                 (if Before not in First_Index (Container) .. Last_Index (Container) + 1
                  then raise Constraint_Error) and then
-                (if Length (Container) + Count > Maximum_Length
+                (if Length (Container) > Maximum_Length - Count
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Capacity (Container) >= Length (Container);
@@ -749,7 +764,7 @@
                  Before /= No_Element and then 
                  (not Has_Element (Container, Before))
                  then raise Program_Error) and then
-                (if Length (Container) + Count > Maximum_Length
+                (if Length (Container) > Maximum_Length - Count
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Capacity (Container) >= Length (Container);
@@ -767,7 +782,7 @@
                 (if Before /= No_Element and then 
                     (not Has_Element (Container, Before))
                  then raise Program_Error) and then
-                (if Length (Container) + Count > Maximum_Length
+                (if Length (Container) > Maximum_Length - Count
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Has_Element (Container, Position) and then
@@ -783,7 +798,7 @@
                  then raise Program_Error) and then
                 (if Before not in First_Index (Container) .. Last_Index (Container) + 1
                  then raise Constraint_Error) and then
-                (if Length (Container) + Count > Maximum_Length
+                (if Length (Container) > Maximum_Length - Count
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Capacity (Container) >= Length (Container);
@@ -807,7 +822,7 @@
                 (if Before /= No_Element and then 
                     (not Has_Element (Container, Before))
                  then raise Program_Error) and
-                (if Length (Container) + Count > Maximum_Length
+                (if Length (Container) > Maximum_Length - Count
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Has_Element (Container, Position) and then
@@ -822,7 +837,7 @@
                    New_Item  : in     Vector)
    with Pre  => (if Tampering_With_Cursors_Prohibited (Container)
                  then raise Program_Error) and then
-                (if Length (Container) + Length (New_Item) > Maximum_Length
+                (if Length (Container) > Maximum_Length - Length (New_Item) 
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
                 Capacity (Container) >= Length (Container);
@@ -835,7 +850,7 @@
                    Count     : in     Count_Type := 1)
    with Pre  => (if Tampering_With_Cursors_Prohibited (Container)
                  then raise Program_Error) and then
-                (if Length (Container) + Count > Maximum_Length
+                (if Length (Container) > Maximum_Length - Count
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Capacity (Container) >= Length (Container);
@@ -847,7 +862,7 @@
                   New_Item  : in     Vector)
    with Pre  => (if Tampering_With_Cursors_Prohibited (Container)
                  then raise Program_Error) and then
-                (if Length (Container) + Length (New_Item) > Maximum_Length
+                (if Length (Container) > Maximum_Length - Length (New_Item) 
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
                 Capacity (Container) >= Length (Container);
@@ -860,7 +875,7 @@
                   Count     : in     Count_Type := 1)
    with Pre  => (if Tampering_With_Cursors_Prohibited (Container)
                  then raise Program_Error) and then
-                (if Length (Container) + Count > Maximum_Length
+                (if Length (Container) > Maximum_Length - Count
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Capacity (Container) >= Length (Container);
@@ -873,7 +888,7 @@
                       New_Item  : in     Element_Type)
    with Pre  => (if Tampering_With_Cursors_Prohibited (Container)
                  then raise Program_Error) and then
-                (if Length (Container) + 1 > Maximum_Length
+                (if Length (Container) > Maximum_Length - 1
                  then raise Constraint_Error),
         Post => Length (Container)'Old + 1 = Length (Container) and then
                 Capacity (Container) >= Length (Container);
@@ -888,7 +903,7 @@
                  then raise Program_Error) and then
                 (if Before not in First_Index (Container) .. Last_Index (Container) + 1
                  then raise Constraint_Error),
-                (if Length (Container) + Count > Maximum_Length
+                (if Length (Container) > Maximum_Length - Count
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Capacity (Container) >= Length (Container);
@@ -911,7 +926,7 @@
                 (if Before /= No_Element and then 
                     (not Has_Element (Container, Before))
                  then raise Program_Error) and then
-                (if Length (Container) + Count > Maximum_Length
+                (if Length (Container) > Maximum_Length - Count
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Has_Element (Container, Position) and then
@@ -1244,7 +1259,9 @@
 
 230.1/3
 function Iterate (Container : in Vector)
-   return Vector_Iterator_Interfaces.Reversible_Iterator'Class;
+   return Vector_Iterator_Interfaces.Reversible_Iterator'Class
+   with Post   => Tampering_With_Cursors_Prohibited (Container);
+
 230.2/3
 Iterate returns a reversible iterator object (see 5.5.1) that will generate a
 value for a loop parameter (see 5.5.2) designating each node in Container,
@@ -1259,8 +1276,9 @@
 230.3/3+
 function Iterate (Container : in Vector; Start : in Cursor)
    return Vector_Iterator_Interfaces.Reversible_Iterator'Class;
-   with Pre  => (if Start = No_Element then raise Constraint_Error) and then
-                (if not Has_Element (Start, Position) then raise Program_Error);
+   with Pre    => (if Start = No_Element then raise Constraint_Error) and then
+                  (if not Has_Element (Start, Position) then raise Program_Error),
+        Post   => Tampering_With_Cursors_Prohibited (Container);
 230.4/3+
 Iterate returns a reversible iterator object (see 5.5.1)
 that will generate a value for a loop parameter (see 5.5.2) designating each
@@ -1289,10 +1307,9 @@
 
 234/2+
 procedure Sort (Container : in out Vector)
-   with Pre'Class  => (if Tampering_With_Elements_Prohibited (Container)
-                       then raise Program_Error);
-[We could check in the postcondition that these are sorted, but that's rather
-expensive, and these assertions won't usually be ignored.]
+   with Pre  => (if Tampering_With_Elements_Prohibited (Container)
+                 then raise Program_Error);
+[Checking whether these are sorted is too expensive, so we won't try.]
 235/2
 Reorders the elements of Container such that the elements are sorted smallest
 first as determined by the generic formal "<" operator provided. Any exception
@@ -1301,16 +1318,18 @@
 236/2+
 procedure Merge (Target  : in out Vector;
                  Source  : in out Vector)
-   with Pre'Class  => (if Tampering_With_Elements_Prohibited (Target)
-                       then raise Program_Error) and then
-                      (if Tampering_With_Elements_Prohibited (Source)
-                       then raise Program_Error),
-        Post'Class => (if Target = Source then True
-                       else Length (Source) = 0 and then
-                            Length (Target) =
-                               Length (Source)'Old + Length (Target)'Old and then
-                            Capacity (Target) >=
-                               Length (Source)'Old + Length (Target)'Old;
+   with Pre  => (if Tampering_With_Elements_Prohibited (Target)
+                 then raise Program_Error) and then
+                (if Tampering_With_Elements_Prohibited (Source)
+                 then raise Program_Error) and then
+                (if Length (Target) > Maximum_Length - Length (Source)
+                 then raise Constraint_Error),
+        Post => (if Target = Source then True
+                 else Length (Source) = 0 and then
+                 Length (Target) =
+                 Length (Source)'Old + Length (Target)'Old and then
+                 Capacity (Target) >=
+                     Length (Source)'Old + Length (Target)'Old;
 [Checking whether these are sorted is too expensive, so we won't try;
 especially as we don't specify what happens if they're not.]
 237/3
@@ -1327,10 +1346,12 @@
 
 A.18.11 The Generic Package Containers.Indefinite_Vectors
 
-[So far as I can tell, the contracts of Vectors are also correct for
-Indefinite_Vectors. The capacity rules and heap usage are essentially
-similar.]
+Add after A.18.11(9/4):
 
+Tampering_With_Cursors_Prohibited is replaced by
+Tampering_With_Elements_Prohibited in the postcondition for the operations
+Reference and Constant_Reference.
+
 -----------------------------------------
 
 A.18.19 The Generic Package Containers.Bounded_Vectors
@@ -1410,7 +1431,6 @@
    type Holder is tagged private
       with Stable_Properties => (Is_Empty, Tampering_With_The_Element_Prohibited),
            Default_Initial_Condition => Is_Empty (Holder);
-
    pragma Preelaborable_Initialization (Holder);
 
 7/3Empty_Holder : constant Holder;
@@ -1439,14 +1459,14 @@
 
 38/3+
 function To_Holder (New_Item : Element_Type) return Holder
-    with Post => not Is_Empty (To_Holder'Result);
+   with Post => not Is_Empty (To_Holder'Result);
 39/4
    Returns a nonempty holder containing an element initialized to New_Item.
    To_Holder performs indefinite insertion (see A.18).
 
 40/3+
 function Is_Empty (Container : Holder) return Boolean
-    with Global => null;
+   with Global => null;
 41/3
     Returns True if Container is empty, and False if it contains an element.
 
@@ -1503,10 +1523,12 @@
 type Constant_Reference_Type
       (Element : not null access constant Element_Type) is private
    with Implicit_Dereference => Element,
+        Global => in out access Holder,
         Default_Initial_Condition => (raise Program_Error);
 53/3+
 type Reference_Type (Element : not null access Element_Type) is private
    with Implicit_Dereference => Element,
+        Global => in out access Holder,
         Default_Initial_Condition => (raise Program_Error);
 54/3
    The types Constant_Reference_Type and Reference_Type need finalization.
@@ -1516,27 +1538,31 @@
 56/3+
 function Constant_Reference (Container : aliased in Holder)
    return Constant_Reference_Type
-   with Pre => (if Is_Empty (Container) then raise Constraint_Error);
+   with Pre    => (if Is_Empty (Container) then raise Constraint_Error),
+        Post   => Tampering_With_The_Element_Prohibited (Container),
+        Global => null;
 57/3
    This function (combined with the Implicit_Dereference aspect) provides a
    convenient way to gain read access to the contained element of a holder
    container.
 58/3+
    Constant_Reference returns an object whose discriminant is an access value
-   that designates the contained element. Tampering with the elements of
+   that designates the contained element. Tampering with the element of
    Container is prohibited while the object returned by Constant_Reference
    exists and has not been finalized.
 
 59/3+
 function Reference (Container : aliased in out Holder) return Reference_Type
-   with Pre => (if Is_Empty (Container) then raise Constraint_Error);
+   with Pre    => (if Is_Empty (Container) then raise Constraint_Error),
+        Post   => Tampering_With_The_Element_Prohibited (Container),
+        Global => null;
 60/3
    This function (combined with the Implicit_Dereference aspects) provides
    a convenient way to gain read and write access to the contained element
    of a holder container.
 61/3+
    Reference returns an object whose discriminant is an access value that 
-   designates the contained element. Tampering with the elements of Container
+   designates the contained element. Tampering with the element of Container
    is prohibited while the object returned by Reference exists and has not
    been finalized.
 
@@ -1891,6 +1917,98 @@
 specific type of the object returned from a function that returns an object 
 of an iterator interface, as well as the primitive operations of that specific 
 type, shall be nonblocking.
+
+!comment For the actual container's definitions (A.18.2-A.18.36), we only 
+!comment provide Corrigendum sections for those that conflict with other
+!comment AI changes.
+
+!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
+See the conflict file!!
+
+
+!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
+See the conflict file!!
+
+
+!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
+See the conflict file!!
+
+
+!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
+See the conflict file!!
+
+
+!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
+See the conflict file!!
+
+
+!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
+See the conflict file!!
+
+
+!corrigendum A.18.10(8/3)
+
+@drepl
+@xcode<   @b<type> Tree @b<is tagged private>
+      @b<with> Constant_Indexing =@> Constant_Reference,
+           Variable_Indexing =@> Reference,
+           Default_Iterator  =@> Iterate,
+           Iterator_Element  =@> Element_Type;
+   @b<pragma> Preelaborable_Initialization(Tree);>
+@dby
+See the conflict file!!
 
 
 !ASIS

Questions? Ask the ACAA Technical Agent