!standard A.18.2(99/3) 19-01-21 AI12-0112-1/07 !standard 11.4.2(23.1/3) !standard 11.5(23) !standard 11.5(26) !standard A(4) !standard A.18(10) !class Amendment 14-05-15 !status Amendment 1-2012 18-12-10 !status ARG Approved 9-0-2 18-12-10 !status work item 14-05-15 !status received 15-02-11 !priority Medium !difficulty Medium !subject Contracts for container operations !summary We add contracts to all of the container operations. These include aspect Nonblocking and aspect Global (needed for the parallel operations). Most container checks are described with preconditions rather than English, so that the definitions are more formal (and can be processed by tools) and that the text is simpler. We add some additional operations to the containers to use in the preconditions and to simplify the needed Global aspects. We also add the new aspect Allows_Exit as needed to iterator subprograms so that procedural iterators of containers can use the full power of Ada control flow. Finally, we added a mechanism to suppress precondition checks for the containers; this puts the containers on the same footing as arrays in regards to the trade-offs of checking and performance. !problem Many of the subprograms defined by the containers start with a series of checks described in English. These would be better written as preconditions, which would make them available to compilers for optimization and to proof tools, as well as being less ambiguous for human readers. Additionally, check suppression for containers is a missing feature in Ada. While a user of an array can suppress checks if they are sufficiently convinced of correctness (and thus get better performance), there is no way to do this for the containers. We also need to add the Nonblocking (AI12-0064-2) and Global (AI12-0079-1) aspects to the containers, so that they can usefully be used with the new parallel features (including AI12-0119-1 and AI12-0242-1), as well as in statically checked protected operations (using aspect Nonblocking). Finally, some of the container reading operations are defined so that the container object is not passed explicitly. This has a number of bad effects: (1) The reading operations are not primitive, so a derivation of a container type is missing reading operations and thus is rather useless; (2) Prefix notation cannot be used on such reading operations, as one wants the prefix to be the container object (it can be used on writing operations, which is asymetric); (3) Since the container is not named explicitly, it is used implicitly. That requires a Global aspect including all containers of the correct type -- which could prevent parallel operation in some cases. !proposal (See summary.) !wording [See the !discussion for general notes before reading this.] [Notes: This version only shows the final result; it does not show any deleted text. See the very end of this section for the text to be added to 11.5; it was put last as it isn't particularly important, but it should be at the start in the final AI as we usually show changes in order. Various notes are given in square brackets; these are for the benefit of ARG readers and will be removed in the Standard.] with Ada.Iterator_Interfaces; generic type Index_Type is range <>; type Element_Type is private; with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Vectors with Preelaborate, Remote_Types, Nonblocking => Equal_Element'Nonblocking, Global => Equal_Element'Global & Element_Type'Global & in out synchronized Ada.Containers.Vectors is [These are the default Nonblocking and Global settings; they're used unless otherwise specified. Note that these depend on the formal parameters of the package. Note that in the Bounded version, Global is just Equal_Element'Global & Element_Type'Global.] subtype Extended_Index is Index_Type'Base range Index_Type'First-1 .. Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; No_Index : constant Extended_Index := Extended_Index'First; type Vector is tagged 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, 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)); pragma Preelaborable_Initialization(Vector); type Cursor is private; pragma Preelaborable_Initialization(Cursor); Empty_Vector : constant Vector; No_Element : constant Cursor; function Equal_Element (Left, Right : Element_Type) return Boolean renames "="; [Note: We need this renames of the formal parameter in order to be able to write the Nonblocking and Global aspects. "="'Global is ambigious.] [The rest of the package is as described in the detailed wording below. The specs would match.] [Note: A.18.2(89.1/3) can be removed; it is covered by preconditions.] Revised package Ada.Containers.Vectors, paragraphs A.18.2(97.2/3) through A.18.2(237): 97.2/3 function Has_Element (Position : Cursor) return Boolean with Nonblocking, Global => in access Vector; [We have to assume this looks at the container object.] 97.3/3 Returns True if Position designates an element, and returns False otherwise. New function Has_Element (Container : Vector; Position : Cursor) return Boolean with Nonblocking, Global => null; New Returns True if Position designates an element in Container, and returns False otherwise. New AARM Ramification: If Position is No_Element, Has_Element returns False. 98/2 function "=" (Left, Right : Vector) return Boolean; [Note: This depends on the formal parameter "=", so we use the default values for Global and Nonblocking.] 99/3 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. New function Tampering_With_Cursors_Prohibited (Container : Vector) return Boolean with Nonblocking, Global => null; New Returns True if tampering with cursors or tampering with elements is currently prohibited for Container, and returns False otherwise. New AARM Note: Prohibiting tampering with elements also prohibits tampering with cursors, so we have this function reflect that. New function Tampering_With_Elements_Prohibited (Container : Vector) return Boolean with Nonblocking, Global => null; New Returns True if tampering with elements is currently prohibited for Container, and returns False otherwise. New function Maximum_Length return Count_Type with Nonblocking => True, Global => null; New Returns the maximum Length of a Vector, based on the index type. AARM Implementation Note: This is just Count_Type (Index_Type'Last - Index_Type'First + 1) but since the inner calculation can overflow or the type conversion can fail, this can't be evaluated in general with an expression function. Note that if this expression raises Constraint_Error, then the result is Count_Type'Last, since the Capacity of a Vector cannot exceed Count_Type'Last. [Author's note: This definition is incompatible on the margins, as the 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, 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 with Pre => (if Length > Maximum_Length then raise Constraint_Error), Post => To_Vector'Result.Length = Length and then not Tampering_With_Elements_Prohibited (To_Vector'Result) and then not Tampering_With_Cursors_Prohibited (To_Vector'Result) and then To_Vector'Result.Capacity >= Length; 101/2 Returns a vector with a length of Length, filled with empty elements. 102/2+ function To_Vector (New_Item : Element_Type; Length : Count_Type) return Vector with Pre => (if Length > Maximum_Length then raise Constraint_Error), Post => Length (To_Vector'Result) = Length and then not Tampering_With_Elements_Prohibited (To_Vector'Result) and then not Tampering_With_Cursors_Prohibited (To_Vector'Result) and then To_Vector'Result.Capacity >= Length; 103/2 Returns a vector with a length of Length, filled with elements initialized to the value New_Item. 104/2+ function "&" (Left, Right : Vector) return Vector 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); 105/2 Returns a vector comprising the elements of Left followed by the elements of Right. 106/2+ function "&" (Left : Vector; Right : Element_Type) return Vector 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 not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then Vectors."&"'Result.Capacity >= Length (Left) + 1; 107/2 Returns a vector comprising the elements of Left followed by the element Right. 108/2+ function "&" (Left : Element_Type; Right : Vector) return Vector 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 not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then Vectors."&"'Result.Capacity >= Length (Right) + 1; 109/2 Returns a vector comprising the element Left followed by the elements of Right. 110/2+ function "&" (Left, Right : Element_Type) return Vector with Pre => (if Maximum_Length < 2 then raise Constraint_Error), Post => Length ("&"'Result) = 2 and then not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then Vectors."&"'Result.Capacity >= 2; 111/2 Returns a vector comprising the element Left followed by the element Right. 112/2+ function Capacity (Container : Vector) return Count_Type with Nonblocking, Global => null; 113/2 Returns the capacity of Container. 114/2+ procedure Reserve_Capacity (Container : in out Vector; Capacity : in Count_Type) with Post => Container.Capacity >= Capacity; 115/3 If the capacity of Container is already greater than or equal to Capacity, then Reserve_Capacity has no effect. Otherwise, Reserve_Capacity allocates additional storage as necessary to ensure that the length of the resulting vector can become at least the value Capacity without requiring an additional call to Reserve_Capacity, and is large enough to hold the current length of Container. Reserve_Capacity then, as necessary, moves elements into the new storage and deallocates any storage no longer needed. Any exception raised during allocation is propagated and Container is not modified. 116/2+ function Length (Container : Vector) return Count_Type with Nonblocking, Global => null; 117/2 Returns the number of elements in Container. 118/2+ procedure Set_Length (Container : in out Vector; Length : in Count_Type) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Length > Maximum_Length then raise Constraint_Error), Post => Container.Length = Length and then Capacity (Container) >= Length; 119/3 If Length is larger than the capacity of Container, Set_Length calls Reserve_Capacity (Container, Length), then sets the length of the Container to Length. If Length is greater than the original length of Container, empty elements are added to Container; otherwise, elements are removed from Container. 120/2+ function Is_Empty (Container : Vector) return Boolean with Nonblocking, Global => null, Post => Is_Empty'Result = Length (Container) = 0; 121/2+ Returns True if Container is empty. 122/2+ procedure Clear (Container : in out Vector) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error), Post => Length (Container) = 0; 123/2 Removes all the elements from Container. The capacity of Container does not change. 124/2+ function To_Cursor (Container : Vector; Index : Extended_Index) return Cursor with Post => (if Index in First_Index (Container) .. Last_Index (Container) then Has_Element (Container, To_Cursor'Result) else To_Cursor'Result = No_Element), Nonblocking, Global => null; 125/2 Returns a cursor designating the element at position Index in Container; returns No_Element if Index does not designate an element. For the purposes of determining whether the parameters overlap in a call to To_Cursor, the Container parameter is not considered to overlap with any object [(including itself)]. 126/2+ function To_Index (Position : Cursor) return Extended_Index with Nonblocking, Global => in access Vector; [Note: No postcondition here, since we can't name the container. See below.] 127/2 If Position is No_Element, No_Index is returned. Otherwise, the index (within its containing vector) of the element designated by Position is returned. New function To_Index (Container : Vector; Position : Cursor) return Extended_Index with Pre => (if Position /= No_Element and then not Has_Element (Container, Position) then raise Program_Error), Post => (if Position = No_Element then To_Index'Result = No_Index else To_Index'Result in First_Index (Container) .. Last_Index (Container)), Nonblocking, Global => null; New Returns the index (within Container) of the element designated by Position; returns No_Index if Position does not designate an element. For the purposes of determining whether the parameters overlap in a call to To_Cursor, the Container parameter is not considered to overlap with any object [(including itself)]. 128/2+ function Element (Container : Vector; Index : Index_Type) return Element_Type with Pre => (if Index not in First_Index (Container) .. Last_Index (Container) then raise Constraint_Error), Nonblocking, Global => Element_Type'Global; 129/2+ Element returns the element at position Index. 130/2+ function Element (Position : Cursor) return Element_Type with Pre => (if Position = No_Element then raise Constraint_Error), Nonblocking => True, Global => Element_Type'Global & in access Vector; 131/2+ Element returns the element designated by Position. New function Element (Container : Vector; Position : Cursor) return Element_Type with Pre => (if Position = No_Element then raise Constraint_Error) and then (if not Has_Element (Container, Position) then raise Program_Error), Nonblocking, Global => Element_Type'Global; New Element returns the element designated by Position in Container. 132/2+ procedure Replace_Element (Container : in out Vector; Index : in Index_Type; New_Item : in Element_Type) with Pre => (if Tampering_With_Elements_Prohibited (Container) then raise Program_Error) and then (if Index not in First_Index (Container) .. Last_Index (Container) then raise Constraint_Error); 133/3+ Replace_Element assigns the value New_Item to the element at position Index. Any exception raised during the assignment is propagated. The element at position Index is not an empty element after successful call to Replace_Element. For the purposes of determining whether the parameters overlap in a call to Replace_Element, the Container parameter is not considered to overlap with any object [(including itself)], and the Index parameter is considered to overlap with the element at position Index. 134/2+ procedure Replace_Element (Container : in out Vector; Position : in Cursor; New_Item : in Element_Type); with Pre => (if Tampering_With_Elements_Prohibited (Container) then raise Program_Error) and then (if Position = No_Element then raise Constraint_Error) and then (if not Has_Element (Container, Position) then raise Program_Error); 135/3+ Replace_Element assigns New_Item to the element designated by Position. Any exception raised during the assignment is propagated. The element at Position is not an empty element after successful call to Replace_Element. For the purposes of determining whether the parameters overlap in a call to Replace_Element, the Container parameter is not considered to overlap with any object [(including itself)]. 136/2+ procedure Query_Element (Container : in Vector; Index : in Index_Type; Process : not null access procedure (Element : in Element_Type)) with Pre => (if Index not in First_Index (Container) .. Last_Index (Container) then raise Constraint_Error). Global => Element_Type'Global; [Tampering ought to be indicated for the access procedure here, but we don't have a mechanism to do that.] 137/3+ Query_Element calls Process.all with the element at position Index as the argument. Tampering with the elements of Container is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated. 138/2+ procedure Query_Element (Position : in Cursor; Process : not null access procedure (Element : in Element_Type)) with Pre => (if Position = No_Element then raise Constraint_Error); Global => Element_Type'Global & in access Vector; 139/3+ Query_Element calls Process.all with the element designated by Position as the argument. Tampering with the elements of the vector that contains the element designated by Position is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated. New procedure Query_Element (Container : in Vector; Position : in Cursor; Process : not null access procedure (Element : in Element_Type)) with Pre => (if Position = No_Element then raise Constraint_Error) or else (not Has_Element (Container, Position) then raise Program_Error) Global => Element_Type'Global; New Query_Element calls Process.all with the element designated by Position as the argument. Tampering with the elements of the vector that contains the element designated by Position is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated. 140/2+ procedure Update_Element (Container : in out Vector; Index : in Index_Type; Process : not null access procedure (Element : in out Element_Type)) with Pre => (if Index not in First_Index (Container) .. Last_Index (Container) then raise Constraint_Error); [Editor's note: Yes, Update_Element does not tamper with elements, because it cannot replace the memory of the element. There is AARM note: A.18.2(97.a/2). When Process is called, it prohibits tampering with elements; I don't know of any way with the current aspects to show that.] 141/3+ Update_Element calls Process.all with the element at position Index as the argument. Tampering with the elements of Container is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated. 142/2 If Element_Type is unconstrained and definite, then the actual Element parameter of Process.all shall be unconstrained. 143/2 The element at position Index is not an empty element after successful completion of this operation. 144/2+ procedure Update_Element (Container : in out Vector; Position : in Cursor; Process : not null access procedure (Element : in out Element_Type)) with Pre => (if Position = No_Element then raise Constraint_Error) and then (if not Has_Element (Container, Position) then raise Program_Error); 145/3+ Update_Element calls Process.all with the element designated by Position as the argument. Tampering with the elements of Container is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated. 146/2 If Element_Type is unconstrained and definite, then the actual Element parameter of Process.all shall be unconstrained. 147/2 The element designated by Position is not an empty element after successful completion of this operation. 147.1/3+ type Constant_Reference_Type (Element : not null access constant Element_Type) is private with Implicit_Dereference => Element, Global => synchronized in out access Vector, Nonblocking => True, 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 => synchronized in out access Vector, Nonblocking => True, Default_Initial_Condition => (raise Program_Error); 147.3/3 The types Constant_Reference_Type and Reference_Type need finalization. 147.4/3+ <> 147.5/3+ 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), 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 of a vector given an index value. 147.7/3+ Constant_Reference returns an object whose discriminant is an access value that designates the element at position Index. Tampering with the elements of Container is prohibited while the object returned by Constant_Reference exists and has not been finalized. 147.8/3+ 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), 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 individual element of a vector given an index value. 147.10/3+ Reference returns an object whose discriminant is an access value that designates the element at position Index. Tampering with the elements of Container is prohibited while the object returned by Reference exists and has not been finalized. 147.11/3 The element at position Index is not an empty element after successful completion of this operation. 147.12/3+ 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), Post => Tampering_With_Cursors_Prohibited (Container), Global => null; 147.13/3 This function (combined with the Constant_Indexing and Implicit_Dereference aspects) provides a convenient way to gain read access to an individual element of a vector given a cursor. 147.14/3+ Constant_Reference returns an object whose discriminant is an access value that designates the element designated by Position. Tampering with the elements of Container is prohibited while the object returned by Constant_Reference exists and has not been finalized. 147.15/3+ 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); 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 individual element of a vector given a cursor. 147.17/3+ Reference returns an object whose discriminant is an access value that designates the element designated by Position. Tampering with the elements of Container is prohibited while the object returned by Reference exists and has not been finalized. 147.18/3 The element designated by Position is not an empty element after successful completion of this operation. 147.19/3+ procedure Assign (Target : in out Vector; Source : in Vector) with Pre => (if Tampering_With_Cursors_Prohibited (Target) then raise Program_Error), Post => Length (Source) = Length (Target), Capacity (Target) >= Length (Target); 147.20/3 If Target denotes the same object as Source, the operation has no effect. If the length of Source is greater than the capacity of Target, Reserve_Capacity (Target, Length (Source)) is called. The elements of Source are then copied to Target as for an assignment_statement assigning Source to Target (this includes setting the length of Target to be that of Source). 147.21/3+ function Copy (Source : Vector; Capacity : Count_Type := 0) return Vector with Pre => (if Capacity /= 0 and then Capacity < Length (Source) then raise Capacity_Error), Post => Length (Copy'Result) = Length (Source) and then not Tampering_With_Elements_Prohibited (Copy'Result) and then not Tampering_With_Cursors_Prohibited (Copy'Result) and then Copy'Result.Capacity >= (if Capacity = 0 then Length (Source) else Capacity); 147.22/3+ Returns a vector whose elements are initialized from the corresponding elements of Source. 148/2+ procedure Move (Target : in out Vector; Source : in out Vector) with Pre => (if Tampering_With_Cursors_Prohibited (Target) then raise Program_Error) and then (if Tampering_With_Cursors_Prohibited (Source) then raise Program_Error), Post => (if Target = Source then True else Length (Target) = Length (Source'Old) and then Length (Source) = 0 and then Capacity (Target) >= Length (Source'Old)); 149/3+ If Target denotes the same object as Source, then the operation has no effect. Otherwise, Move first calls Reserve_Capacity (Target, Length (Source)) and then Clear (Target); then, each element from Source is removed from Source and inserted into Target in the original order. 150/2+ procedure Insert (Container : in out Vector; Before : in Extended_Index; New_Item : in Vector) with Pre => (if Tampering_With_Cursors_Prohibited (Container) 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) > 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.] Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then Capacity (Container) >= Length (Container); 151/3+ If Length (New_Item) is 0, then Insert does nothing. Otherwise, it computes the new length NL as the sum of the current length and Length (New_Item). 152/2 If the current vector capacity is less than NL, Reserve_Capacity (Container, NL) is called to increase the vector capacity. Then Insert slides the elements in the range Before .. Last_Index (Container) up by Length (New_Item) positions, and then copies the elements of New_Item to the positions starting at Before. Any exception raised during the copying is propagated. 153/2+ procedure Insert (Container : in out Vector; Before : in Cursor; New_Item : in Vector); with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Length (New_Item) /= 0 and then Before /= No_Element and then (not Has_Element (Container, Before)) then raise Program_Error) and then (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); 154/3+ If Length (New_Item) is 0, then Insert does nothing. If Before is No_Element, then the call is equivalent to Insert (Container, Last_Index (Container) + 1, New_Item); otherwise, the call is equivalent to Insert (Container, To_Index (Before), New_Item); 155/2+ procedure Insert (Container : in out Vector; Before : in Cursor; New_Item : in Vector; Position : out Cursor); with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Before /= No_Element and then (not Has_Element (Container, Before)) then raise Program_Error) and then (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 Capacity (Container) >= Length (Container); 156/2+ If Before equals No_Element, then let T be Last_Index (Container) + 1; otherwise, let T be To_Index (Before). Insert (Container, T, New_Item) is called, and then Position is set to To_Cursor (Container, T). 157/2+ procedure Insert (Container : in out Vector; Before : in Extended_Index; New_Item : in Element_Type; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) 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) > Maximum_Length - Count then raise Constraint_Error), Post => Length (Container)'Old + Count = Length (Container) and then Capacity (Container) >= Length (Container); 158/2 Equivalent to Insert (Container, Before, To_Vector (New_Item, Count)); 159/2+ procedure Insert (Container : in out Vector; Before : in Cursor; New_Item : in Element_Type; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Count /= 0 and then Before /= No_Element and then (not Has_Element (Container, Before)) then raise Program_Error) and then (if Length (Container) > Maximum_Length - Count then raise Constraint_Error), Post => Length (Container)'Old + Count = Length (Container) and then Capacity (Container) >= Length (Container); 160/2 Equivalent to Insert (Container, Before, To_Vector (New_Item, Count)); 161/2+ procedure Insert (Container : in out Vector; Before : in Cursor; New_Item : in Element_Type; Position : out Cursor; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Before /= No_Element and then (not Has_Element (Container, Before)) then raise Program_Error) and then (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 Capacity (Container) >= Length (Container); 162/2 Equivalent to Insert (Container, Before, To_Vector (New_Item, Count), Position); 163/2+ procedure Insert (Container : in out Vector; Before : in Extended_Index; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) 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) > Maximum_Length - Count then raise Constraint_Error), Post => Length (Container)'Old + Count = Length (Container) and then Capacity (Container) >= Length (Container); 164/3+ If Count is 0, then Insert does nothing. Otherwise, it computes the new length NL as the sum of the current length and Count. 165/2 If the current vector capacity is less than NL, Reserve_Capacity (Container, NL) is called to increase the vector capacity. Then Insert slides the elements in the range Before .. Last_Index (Container) up by Count positions, and then inserts elements that are initialized by default (see 3.3.1) in the positions starting at Before. 166/2+ procedure Insert (Container : in out Vector; Before : in Cursor; Position : out Cursor; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Before /= No_Element and then (not Has_Element (Container, Before)) then raise Program_Error) and (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 Capacity (Container) >= Length (Container); 67/2 If Before equals No_Element, then let T be Last_Index (Container) + 1; otherwise, let T be To_Index (Before). Insert (Container, T, Count) is called, and then Position is set to To_Cursor (Container, T). 168/2+ procedure Prepend (Container : in out Vector; New_Item : in Vector) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (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); 169/2 Equivalent to Insert (Container, First_Index (Container), New_Item). 170/2+ procedure Prepend (Container : in out Vector; New_Item : in Element_Type; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Length (Container) > Maximum_Length - Count then raise Constraint_Error), Post => Length (Container)'Old + Count = Length (Container) and then Capacity (Container) >= Length (Container); 171/2 Equivalent to Insert (Container, First_Index (Container), New_Item, Count). 172/2+ procedure Append (Container : in out Vector; New_Item : in Vector) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (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); 173/2 Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item). 174/2+ procedure Append (Container : in out Vector; New_Item : in Element_Type; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Length (Container) > Maximum_Length - Count then raise Constraint_Error), Post => Length (Container)'Old + Count = Length (Container) and then Capacity (Container) >= Length (Container); 175/2 Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item, Count). 175.1/5 procedure Append_One (Container : in out Vector; New_Item : in Element_Type) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Length (Container) > Maximum_Length - 1 then raise Constraint_Error), Post => Length (Container)'Old + 1 = Length (Container) and then Capacity (Container) >= Length (Container); 175.2/5 Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item, 1). 176/2+ procedure Insert_Space (Container : in out Vector; Before : in Extended_Index; Count : in Count_Type := 1); with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Before not in First_Index (Container) .. Last_Index (Container) + 1 then raise Constraint_Error), (if Length (Container) > Maximum_Length - Count then raise Constraint_Error), Post => Length (Container)'Old + Count = Length (Container) and then Capacity (Container) >= Length (Container); 177/3+ If Count is 0, then Insert_Space does nothing. Otherwise, it computes the new length NL as the sum of the current length and Count. 178/2 If the current vector capacity is less than NL, Reserve_Capacity (Container, NL) is called to increase the vector capacity. Then Insert_Space slides the elements in the range Before .. Last_Index (Container) up by Count positions, and then inserts empty elements in the positions starting at Before. 179/2+ procedure Insert_Space (Container : in out Vector; Before : in Cursor; Position : out Cursor; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Before /= No_Element and then (not Has_Element (Container, Before)) then raise Program_Error) and then (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 Capacity (Container) >= Length (Container); 180/2 If Before equals No_Element, then let T be Last_Index (Container) + 1; otherwise, let T be To_Index (Before). Insert_Space (Container, T, Count) is called, and then Position is set to To_Cursor (Container, T). 181/2+ procedure Delete (Container : in out Vector; Index : in Extended_Index; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Index not in First_Index (Container) .. Last_Index (Container) + 1 then raise Constraint_Error) and then (if Length (Container) + Count > Maximum_Length then raise Constraint_Error), Post => Length (Container)'Old - Count <= Length (Container); 182/3+ If Count is 0, Delete has no effect. Otherwise, Delete slides the elements (if any) starting at position Index + Count down to Index. Any exception raised during element assignment is propagated. 183/2+ procedure Delete (Container : in out Vector; Position : in out Cursor; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error) and then (if Position = No_Element then raise Constraint_Error) and then (if not Has_Element (Container, Position) then raise Program_Error), Post => Length (Container)'Old - Count <= Length (Container) and then Position = No_Element; 184/2 Delete (Container, To_Index (Position), Count) is called, and then Position is set to No_Element. 185/2+ procedure Delete_First (Container : in out Vector; Count : in Count_Type := 1) with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error), Post => Length (Container)'Old - Count <= Length (Container); 186/2 Equivalent to Delete (Container, First_Index (Container), Count). 187/2+ procedure Delete_Last (Container : in out Vector; Count : in Count_Type := 1); with Pre => (if Tampering_With_Cursors_Prohibited (Container) then raise Program_Error), Post => Length (Container)'Old - Count <= Length (Container); 188/3 If Length (Container) <= Count, then Delete_Last is equivalent to Clear (Container). Otherwise, it is equivalent to Delete (Container, Index_Type'Val(Index_Type'Pos(Last_Index (Container)) – Count + 1), Count). 189/2+ procedure Reverse_Elements (Container : in out Vector) with Pre => (if Tampering_With_Elements_Prohibited (Container) then raise Program_Error); 190/2 Reorders the elements of Container in reverse order. 191/2+ procedure Swap (Container : in out Vector; I, J : in Index_Type) with Pre => (if Tampering_With_Elements_Prohibited (Container) then raise Program_Error) and then (if I not in First_Index (Container) .. Last_Index (Container) then raise Constraint_Error) and then (if J not in First_Index (Container) .. Last_Index (Container) then raise Constraint_Error); 192/2+ Swap exchanges the values of the elements at positions I and J. 193/2+ procedure Swap (Container : in out Vector; I, J : in Cursor); with Pre => (if Tampering_With_Elements_Prohibited (Container) then raise Program_Error) and then (if I = No_Element or else J = No_Element then raise Constraint_Error) and then (if not Has_Element (Container, I) then raise Program_Error) and then (if not Has_Element (Container, J) then raise Program_Error); 194/2+ Swap exchanges the values of the elements designated by I and J. 195/2 function First_Index (Container : Vector) return Index_Type is with Nonblocking => True, Global => null, Post => First_Index'Result = Index_Type'First; 196/2 Returns the value Index_Type'First. 197/2+ function First (Container : Vector) return Cursor with Post => (if not Is_Empty (Container) then Has_Element (Container, First'Result) else First'Result = No_Element), Global => null, Nonblocking => True; 198/2 If Container is empty, First returns No_Element. Otherwise, it returns a cursor that designates the first element in Container. 199/2 function First_Element (Container : Vector) return Element_Type is with Pre => (if Is_Empty (Container) then raise Constraint_Error); 200/2 Equivalent to Element (Container, First_Index (Container)). 201/2 function Last_Index (Container : Vector) return Extended_Index with Nonblocking => True, Global => null, Post => (if Length (Container) = 0 then Last_Index'Result = No_Index else Last_Index'Result = Length (Container) - 1 + Index_Type'First); 202/2 If Container is empty, Last_Index returns No_Index. Otherwise, it returns the position of the last element in Container. 203/2+ function Last (Container : Vector) return Cursor; with Post => (if not Is_Empty (Container) then Has_Element (Container, Last'Result) else Last'Result = No_Element), Global => null, Nonblocking => True; 204/2 If Container is empty, Last returns No_Element. Otherwise, it returns a cursor that designates the last element in Container. 205/2+ function Last_Element (Container : Vector) return Element_Type with Pre => (if Is_Empty (Container) then raise Constraint_Error); 206/2 Equivalent to Element (Container, Last_Index (Container)). 207/2+ function Next (Position : Cursor) return Cursor with Global => Vectors'Global & in access Vector, Nonblocking => True, Post => (if Position = No_Element then Next'Result = No_Element else True); 208/2 If Position equals No_Element or designates the last element of the container, then Next returns the value No_Element. Otherwise, it returns a cursor that designates the element with index To_Index (Position) + 1 in the same vector as Position. New function Next (Container : Vector; Position : Cursor) return Cursor with Pre => (if Position /= No_Element and then (not Has_Element (Container, Position)) then raise Program_Error), Post => (if Position = No_Element then Next'Result = No_Element elsif Has_Element (Container, Next'Result) then True elsif Next'Result = No_Element then Position = Last (Container) else To_Index (Container, Next'Result) = To_Index (Container, Position) + 1), Global => null, Nonblocking => True; New Returns a cursor designating the next element in the Container, if any. 209/2+ procedure Next (Position : in out Cursor) with Global => Vectors'Global & in access Vector, Nonblocking => True; 210/2 Equivalent to Position := Next (Position). New procedure Next (Container : Vector; Position : in out Cursor) with Pre => (if Position /= No_Element and then (not Has_Element (Container, Position)) then raise Program_Error), Post => (if Position /= No_Element then Has_Element (Container, Position)), Global => null, Nonblocking => True; New Equivalent to Position := Next (Position). 211/2+ function Previous (Position : Cursor) return Cursor with Global => Vectors'Global & in access Vector, Nonblocking => True, Post => (if Position = No_Element then Previous'Result = No_Element else True); 212/2 If Position equals No_Element or designates the first element of the container, then Previous returns the value No_Element. Otherwise, it returns a cursor that designates the element with index To_Index (Position) – 1 in the same vector as Position. New function Previous (Container : Vector; Position : Cursor) return Cursor with Pre => (if Position /= No_Element and then (not Has_Element (Container, Position)) then raise Program_Error), Post => (if Position = No_Element then Previous'Result = No_Element elsif Has_Element (Container, Previous'Result) then True elsif Next'Result = No_Element then Position = First (Container) else To_Index (Container, Next'Result) = To_Index (Container, Position) - 1), Global => null, Nonblocking => True; New Returns a cursor designating the previous element in the Container, if any. 213/2+ procedure Previous (Position : in out Cursor) with Global => Vectors'Global & in access Vector, Nonblocking => True; 214/2 Equivalent to Position := Previous (Position). New procedure Previous (Container : Vector; Position : in out Cursor) with Pre => (if Position /= No_Element and then (not Has_Element (Container, Position)) then raise Program_Error), Post => (if Position /= No_Element then Has_Element (Container, Position)), Global => null, Nonblocking => True; New Equivalent to Position := Previous (Position). 215/2 function Find_Index (Container : Vector; Item : Element_Type; Index : Index_Type := Index_Type'First) return Extended_Index; 216/2 Searches the elements of Container for an element equal to Item (using the generic formal equality operator). The search starts at position Index and proceeds towards Last_Index (Container). If no equal element is found, then Find_Index returns No_Index. Otherwise, it returns the index of the first equal element encountered. 217/2+ function Find (Container : Vector; Item : Element_Type; Position : Cursor := No_Element) return Cursor with Pre => (if Position /= No_Element and then (not Has_Element (Container, Position)) then raise Program_Error), with Post => (if Find'Result = No_Element then True else Has_Element (Container, Find'Result)); 218/3+ Find searches the elements of Container for an element equal to Item (using the generic formal equality operator). The search starts at the first element if Position equals No_Element, and at the element designated by Position otherwise. It proceeds towards the last element of Container. If no equal element is found, then Find returns No_Element. Otherwise, it returns a cursor designating the first equal element encountered. 219/2 function Reverse_Find_Index (Container : Vector; Item : Element_Type; Index : Index_Type := Index_Type'Last) return Extended_Index; 220/2 Searches the elements of Container for an element equal to Item (using the generic formal equality operator). The search starts at position Index or, if Index is greater than Last_Index (Container), at position Last_Index (Container). It proceeds towards First_Index (Container). If no equal element is found, then Reverse_Find_Index returns No_Index. Otherwise, it returns the index of the first equal element encountered. 221/2+ function Reverse_Find (Container : Vector; Item : Element_Type; Position : Cursor := No_Element) return Cursor with Pre => (if Position /= No_Element and then (not Has_Element (Container, Position)) then raise Program_Error), with Post => (if Reverse_Find'Result = No_Element then True else Has_Element (Container, Reverse_Find'Result)); 222/3+ Reverse_Find searches the elements of Container for an element equal to Item (using the generic formal equality operator). The search starts at the last element if Position equals No_Element, and at the element designated by Position otherwise. It proceeds towards the first element of Container. If no equal element is found, then Reverse_Find returns No_Element. Otherwise, it returns a cursor designating the first equal element encountered. 223/2 function Contains (Container : Vector; Item : Element_Type) return Boolean; 224/2 Equivalent to Has_Element (Find (Container, Item)). 227/2+ procedure Iterate (Container : in Vector; Process : not null access procedure (Position : in Cursor) with Allows_Exit; 228/3 Invokes Process.all with a cursor that designates each element in Container, in index order. Tampering with the cursors of Container is prohibited during the execution of a call on Process.all. Any exception raised by Process.all is propagated. 229/2 procedure Reverse_Iterate (Container : in Vector; Process : not null access procedure (Position : in Cursor)) with Allows_Exit; 230/3 Iterates over the elements in Container as per procedure Iterate, except that elements are traversed in reverse index order. 230.1/3 function Iterate (Container : in Vector) 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, starting with the first node and moving the cursor as per the Next function when used as a forward iterator, and starting with the last node and moving the cursor as per the Previous function when used as a reverse iterator. Tampering with the cursors of Container is prohibited while the iterator object exists (in particular, in the sequence_of_statements of the loop_statement whose iterator_specification denotes this object). The iterator object needs finalization. 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), 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 node in Container, starting with the node designated by Start and moving the cursor as per the Next function when used as a forward iterator, or moving the cursor as per the Previous function when used as a reverse iterator. Tampering with the cursors of Container is prohibited while the iterator object exists (in particular, in the sequence_of_statements of the loop_statement whose iterator_specification denotes this object). The iterator object needs finalization. 231/3 The actual function for the generic formal function "<" of Generic_Sorting is expected to return the same value each time it is called with a particular pair of element values. It should define a strict weak ordering relationship (see A.18); it should not modify Container. If the actual for "<" behaves in some other manner, the behavior of the subprograms of Generic_Sorting are unspecified. The number of times the subprograms of Generic_Sorting call "<" is unspecified. 232/2 function Is_Sorted (Container : Vector) return Boolean; 233/2 Returns True if the elements are sorted smallest first as determined by the generic formal "<" operator; otherwise, Is_Sorted returns False. Any exception raised during evaluation of "<" is propagated. 234/2+ procedure Sort (Container : in out Vector) 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 raised during evaluation of "<" is propagated. 236/2+ procedure Merge (Target : in out Vector; Source : in out Vector) 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 If Source is empty, then Merge does nothing. If Source and Target are the same nonempty container object, then Program_Error is propagated. Otherwise, Merge removes elements from Source and inserts them into Target; afterwards, Target contains the union of the elements that were initially in Source and Target; Source is left empty. If Target and Source are initially sorted smallest first, then Target is ordered smallest first as determined by the generic formal "<" operator; otherwise, the order of elements in Target is unspecified. Any exception raised during evaluation of "<" is propagated. ----------------------------------------- A.18.11 The Generic Package Containers.Indefinite_Vectors Add after A.18.11(9/4): The description of Tampering_With_Elements_Prohibited is replaced by: Returns True if tampering with elements is prohibited for Container, and False otherwise. 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 Modify A.18.19(2/3): * The {aspect}[pragma] Preelaborate is replaced with {aspect}[pragma] Pure. Add after A.18.19(3/3): * The Global aspect of the package is replaced by Global => Equal_Element'Global & Element_Type'Global, AARM Reason: This package is pure, and thus it cannot have or depend upon any other packages that have state. Thus we require no global uses whatsoever other than those of the formals. Add after A.18.19(6/3): * Capacity is omitted from the Stable_Properties of type Vector. AARM Reason: The capacity is a discriminant here, so it can't be changed by most routines; thus including it in the stable properties adds no information. Modify A.18.19(7/3): In function Copy, [if the Capacity parameter is equal to or greater than the length of Source, the vector capacity exactly equals the value of the Capacity parameter]{the postcondition is altered to:} Post => Length (Copy'Result) = Length (Source) and then (if Capacity > Length (Source) then Copy'Result.Capacity = Capacity else Copy'Result.Capacity >= Length (Source)); [Note: Reading the discriminant here, not a prefix call.] Replace A.18.19(9.3) by: procedure Reserve_Capacity (Container : in out Vector; Capacity : in Count_Type) with Pre => (if Capacity > Container.Capacity then raise Capacity_Error); This operation has no effect[Redundant: other than checking the precondition]. Add after A.18.19(9/3): * The portion of the postcondition checking the capacity is omitted from subprograms Set_Length, Assign, Insert, Insert_Space, Prepend, Append, Delete, * For procedures Insert, Insert_Space, Prepend, and Append, the part of the precondition reading: (if > Maximum_Length then raise Constraint_Error) is replaced by: (if > Maximum_Length then raise Constraint_Error) and then (if > Container.Capacity then raise Capacity_Error) ----------------------------------------- A.18.18 The Generic Package Containers.Indefinite_Holders The generic library package Containers.Indefinite_Holders has the following declaration: 5/3+ generic type Element_Type (<>) is private; with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Indefinite_Holders with Preelaborate, Remote_Types, Nonblocking => Equal_Element'Nonblocking, Global => Equal_Element'Global & Element_Type'Global & in out synchronized Ada.Containers.Indefinite_Holders is 6/3+ 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; New function Equal_Element (Left, Right : Element_Type) return Boolean renames "="; [Same from here to start of specifications. 36/3 function "=" (Left, Right : Holder) return Boolean; 37/3 If Left and Right denote the same holder object, then the function returns True. Otherwise, it compares the element contained in Left to the element contained in Right using the generic formal equality operator, returning the result of that operation. Any exception raised during the evaluation of element equality is propagated. New function Tampering_With_The_Element_Prohibited (Container : Holder) return Boolean with Nonblocking => True, Global => null; New Returns True if tampering with the element is currently prohibited for Container, and returns False otherwise. 38/3+ function To_Holder (New_Item : Element_Type) return Holder 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; 41/3 Returns True if Container is empty, and False if it contains an element. 42/3+ procedure Clear (Container : in out Holder) with Pre => (if Tampering_With_The_Element_Prohibited (Container) then raise Program_Error), Post => Is_Empty (Container); 43/3+ Removes the element from Container. 44/3+ function Element (Container : Holder) return Element_Type with Pre => (if Is_Empty(Container) then raise Constraint_Error), Global => Element_Type'Global; 45/3+ Returns the element stored in Container. 46/3+ procedure Replace_Element (Container : in out Holder; New_Item : in Element_Type) with Pre => (if Tampering_With_The_Element_Prohibited (Container) then raise Program_Error), Post => not Is_Empty (Container); 47/4+ Replace_Element assigns the value New_Item into Container, replacing any preexisting content of Container; Replace_Element performs indefinite insertion (see A.18). 48/3+ procedure Query_Element (Container : in Holder; Process : not null access procedure (Element : in Element_Type)) with Pre => (if Is_Empty (Container) then raise Constraint_Error), Global => null; 49/3+ Query_Element calls Process.all with the contained element as the argument. Tampering with the element of Container is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated. 50/3+ procedure Update_Element (Container : in out Holder; Process : not null access procedure (Element : in out Element_Type)) with Pre => (if Is_Empty (Container) then raise Constraint_Error); 51/3+ Update_Element calls Process.all with the contained element as the argument. Tampering with the element of Container is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated. 52/3+ 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. 55/3+ <> 56/3+ function Constant_Reference (Container : aliased in Holder) return Constant_Reference_Type 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 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), 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 element of Container is prohibited while the object returned by Reference exists and has not been finalized. 62/3+ procedure Assign (Target : in out Holder; Source : in Holder) with Post => (Is_Empty (Source) = Is_Empty (Target)); 63/3 If Target denotes the same object as Source, the operation has no effect. If Source is empty, Clear (Target) is called. Otherwise, Replace_Element (Target, Element (Source)) is called. 64/3+ function Copy (Source : Holder) return Holder with Post => Is_Empty (Source) = Is_Empty (Copy'Result); 65/3 If Source is empty, returns an empty holder container; otherwise, returns To_Holder (Element (Source)). 66/3+ procedure Move (Target : in out Holder; Source : in out Holder) with Pre => (if Tampering_With_The_Element_Prohibited (Container) then raise Program_Error), Post => (if Target /= Source then Is_Empty (Source) and then (not Is_Empty (Target)); 67/3+ If Target denotes the same object as Source, then the operation has no effect. Otherwise, the element contained by Source (if any) is removed from Source and inserted into Target, replacing any preexisting content. ----------------------------------------- Add after 11.4.2(23.5/5): Any precondition expression occurring in the specification of a language-defined unit is enabled (see 6.1.1) unless suppressed (see 11.5). Similarly, any predicate checks for a subtype occurring in the specification of a language-defined unit are enabled (see 3.2.4) unless suppressed. AARM Reason: This allows the Standard to express runtime requirements on the client of a language-defined unit as preconditions or predicates (which are invariably clearer than English prose would be). Some such requirements can be Suppressed. Ada 2012 and before did not provide a mechanism to suppress such code. Add after 11.5(23): Redundant[The following check corresponds to situations in which the exception Assertion_Error is raised upon failure of a language-defined check.] Containers_Assertion_Check Check the precondition of a routine declared in a descendant unit of Containers or in an instance of a generic unit that is declared in, or is, a descendant unit of Containers. AARM Reason: One could use @b Assertion_Policy to eliminate such checks, but that would require recompiling the Ada.Containers packages (the assertion policy that determines whether the checks are made is that used to compile the unit). In addition, we do not want to specify the behavior of the Ada.Containers operations if the precondition fails; that is different than the usual behavior of Assertion_Policy. By using Suppress for this purpose, we make it clear that a failed check that is suppressed means erroneous execution. Modify 11.5(26): If a given check has been suppressed, and the corresponding error situation occurs, the execution of the program is erroneous. {Similarly, if a precondition check has been suppressed and the evaluation of the precondition would have raised an exception, execution is erroneous.} AARM Reason: It's unclear that a precondition expression that executes /raise/ *some_exception* is an "error situation"; the precondition never actually evaluates to False in that case. Thus, we spell out that case. We only allow suppressing preconditions associated with language-defined units; other preconditions follow the rules of the appropriate Assertion_Policy. Add after Annex A(4): [Implementation Permissions] The implementation may add specifications of synchronized entities of implementation-defined packages to the global specification (see 6.1.2) for any language-defined entity that is not declare pured or has a global specification of \null\. AARM Reason: Ada runtime libraries often use implementation-defined helper packages to implement the language-defined units. For instance, it is common to use a common low-level package to implement I/O; if that package includes support for Current Input and Current Output, then it is likely to have state that needs to be reflected in the packages that use it such as Ada.Text_IO. We want to allow such packages, so we have defined this permission to allow them to include state if necessary. We require that any such state is synchronized to ensure that appropriate use (as defined above) is allowed in parallel operations. We exclude units that are declared pure from this permission since this is a declaration that the unit doesn't have any global state, so specifying otherwise would defeat the purpose. Similarly, entities that explicitly specify Global as \null\ are supposed to have no side-effects, and we don't want implementations to add any. End AARM Reason. AARM Ramification: Implementations are of course allowed to make other changes to the specifications of language-defined units, so long as those changes are semantically neutral (that is, no program could change legality or effect because of the changes). In particular, an implementation would need to add implementation-defined units to the context clause in order to use the previous permission; this is allowed and does not need a separate permission. Similarly, an implementation can add postconditions to language-defined subprograms, so long as those postconditions always evaluate to True. This is useful if the implementation can use those postconditions for optimization. End AARM Ramification. Add after A.18(11/5): For an instance I of a container package with a container type C, the specific type T of the object returned from a function that returns an object of an iterator interface, as well as the primitive operations of T, shall be nonblocking. The Global aspect specified for T and the primitive operations of T shall be (in access C, synchronized out access C) or a specification that allows accesses fewer global objects. AARM Implementation Note: This requires that the traversal and iteration operations of a container do not create, destroy, or assign any objects of a formal type of I, nor call any formal subprograms of I. Those objects and subprograms might be blocking or write globals (depending on the actual parameters). We put similar requirements on the individual traversal operations in the container package definitions. !discussion For this version, we've prototyped the changes needed for a single container (Ada.Containers.Vectors) and the bounded and indefinite versions thereof, along with the indefinite holders. Additional changes will be needed if AI12-0111-1 is approved. [Editor's note: I would want to apply both of these AIs together, since the changes needed are interrelated.] This version only shows the wording for the main body of the definition of Ada.Containers.Vectors and the start of the package specification. The rest of the package specification would also have to be modified, and there might be some wording simplifications possible in the other sections. These were not looked at for this prototype. A handful of new predicate functions are needed for these preconditions. These are clearly marked as new. Also new are versions of a few reading routines that did not take a container parameter. (One routine, Has_Element with a container parameter, is both.) All other operations are pre-existing; the contracts are new and some of the English text has been simplified but no change in semantics is intended. The paragraph numbers of modified paragraphs are marked with a "+". The edits to text (including deletions) is not shown in order to illustrate the improvement (or lack thereof) in readability after converting English checks to Ada expressions. (A lot of connector words were dropped, especially "otherwise", which should improve readability.) There are a few cases where I was able to drop wording when it was specified by the postcondition (mostly where the length or capacity was specified) or the default initial conditions (for the various reference types). This follows the policy we adopted earlier when working on the random number package. We are only including 4 stable properties in the postconditions. These are the Length, Capacity, and tampering state. These should be able to be reasoned about by humans and tools, so there is value in specifying that they are not changed. We only give explicit postconditions when one of the stable properties is changed by a routine, or when the routine creates a cursor (in those cases, the postcondition asserts that the cursor belongs to the appropriate container). --- We define a new check name Container_Check for pragma Suppress. As noted in the AARM note, Assertion_Policy is the wrong way to turn off these preconditions. We definitely do not want to require implementations to make duplicate checks in case the precondition isn't evaluated; therefore we need to say that execution is erroneous in case the precondition would have evaluated to False or raised an exception. (It would be nice to say this is just unspecified, with the intent of allowing anything Ada-related to happen, but not allow overwriting memory or the like, but that's a hard concept to define - and it's unclear how that would apply to a non-Ada implementation.) I would have preferred to have this as a global setting for the entire Ada library, but Precondition_Check seems to imply this covers *any* precondition (which it doesn't). The "correct" name is Language_Defined_Unit_Precondition_Check, which I think the Ada community would clobber us for using (and probably me for even proposing it ;-). Therefore, I hit on the idea of naming the check for the first level "grouping" package. Thus, the check names would be Container_Check (as used here), Numerics_Check (for Ada.Numerics), Strings_Check (for Ada.Strings), IO_Check (for the missing Ada.IO package; the packages involved would have to be listed), and so on. This provides a bit more granularity (although that only matters if we define many more routines with preconditions). Note: This topic is now split out into AI12-0311-1 so we can define this consistently for the entire set of language-defined units. --- AI12-0189-1 defines procedural iterators and the Allows_Exit aspect to be used on routines that are prepared to support arbitrary completions caused by the use of transfers of control in the loop body of such an iterator. We intend that the Iterate routines defined by the containers can be used by such procedural iterators with the full spectrum of transfers-of-control defined by Ada for loops. We indicate that by including Allows_Exit on such routines. Including this aspect requires that implementers design the Iterate implementations so that they properly clean up even in the face of arbitrary completions. That may or may not be true of existing implementations; hopefully the new aspect will trigger implementers to inspect their implementations for issues. --- For the pre- and postconditions, we used Pre and Post rather than Pre'Class and Post'Class, since these mostly belong to the specific routine rather than any routine matching the profile. This way, they can be eliminated for a derived type if desired. (The usual rules mean that any delegation to the original routine will check the original Pre/Post.) This does mean that they won't necessarily follow LSP for a dispatching call, but that seems unnecessary for the containers (extensions seem unusual, and using multiple versions of a single container simultaenously more so). By using Pre, an implementation can generate the precondition as part of the subprogram body if it wishes (or it can generate it at the call site to support optimization and suppressibility). --- We override the usual Nonblocking and Global status for the various predicate routines, to essentially mark these as Pure. If Nonblocking => True is used, this would prevent calling the formal subprograms in the associated routines. But that shouldn't be necessary to implement these (they usually are direct queries on the container state). Similarly, we require the container navigation routines to be "pure" in this sense; no access to the formal subprograms or elements is needed to move around in a container. --- The global setting "Access subtype_mark" says that it applies to all of the "(aliased)" objects of subtype_mark. For a tagged type (like Vector), it needs to apply to all objects of the type, since 'Access can be used inside of the package, and has to for the containers packages in order to create the needed cursor semantics. --- We use prefixed notation in some pre- and postconditions, as the function that needs to be called has the same name as a parameter of the routine (see To_Vector and Reserve_Capacity for examples). The direct name is hidden in that case, so prefixed notation seems like the best way to call the function. In other cases, we have used conventional notation for subprogram calls. --- Note that we duplicate contracts in the complete specification and in the individual descriptions of entities. This simplifies reading of the contracts -- constantly looking at the full specification is not needed. This seems important for routines that have part of their semantics defined by contracts, and is done for all routines for consistency. --- Not everything can be handled with the existing contracts. For instance, we can't provide a precondition for anonymous access-to-subprogram parameters. Thus we can't specify in the contract that Tampering_With_Cursors_Prohibited is True for Query_Element/Update_Element/subprogram iterators. It also would be nice to be able to indicate that Tampering_With_Cursors_Prohibited is True during the lifetime of an iterator or reference object. This doesn't correspond to any of the "traditional" contracts. The lack of these specifications is not critical. It just prevents tools and compilers from detecting failing tampering checks (and optimizing away unnecessary checks) based on these properties alone. !corrigendum 11.4.2(23.1/3) @dinsa It is a bounded error to invoke a potentially blocking operation (see 9.5.1) during the evaluation of an assertion expression associated with a call on, or return from, a protected operation. If the bounded error is detected, Program_Error is raised. If not detected, execution proceeds normally, but if it is invoked within a protected action, it might result in deadlock or a (nested) protected action. @dinst Any precondition expression occurring in the specification of a language-defined unit is enabled (see 6.1.1) unless suppressed (see 11.5). Similarly, any predicate checks for a subtype occurring in the specification of a language-defined unit are enabled (see 3.2.4) unless suppressed. !corrigendum 11.5(23) @dinsa @xhang<@xterm Check that evaluation of an @fa does not require more space than is available for a storage pool. Check that the space available for a task or subprogram has not been exceeded.> @dinss @xbullet @xhang<@xterm Check the precondition of a routine declared in a descendant unit of Containers or in an instance of a generic unit that is declared in, or is, a descendant unit of Containers.> !corrigendum 11.5(26) @drepl If a given check has been suppressed, and the corresponding error situation occurs, the execution of the program is erroneous. @dby If a given check has been suppressed, and the corresponding error situation occurs, the execution of the program is erroneous. Similarly, if a precondition check has been suppressed and the evaluation of the precondition would have raised an exception, execution is erroneous. !corrigendum A(4) @dinsa The implementation may restrict the replacement of language-defined compilation units. The implementation may restrict children of language-defined library units (other than Standard). @dinst The implementation may add specifications of synchronized entities of implementation-defined packages to the global specification (see 6.1.2) for any language-defined entity that is not declared pure or has a global specification of @b. !corrigendum A.18(10) @dinsa For an indefinite container (one whose type is defined in an instance of a child package of Containers whose @fa contains "Indefinite"), each element of the container shall be created when it is inserted into the container and finalized when it is deleted from the container (or when the container object is finalized if the element has not been deleted). For a bounded container (one whose type is defined in an instance of a child package of Containers whose @fa starts with "Bounded") that is not an indefinite container, all of the elements of the capacity of the container shall be created and default initialized when the container object is created; the elements shall be finalized when the container object is finalized. For other kinds of containers, when elements are created and finalized is unspecified. @dinst For an instance @i of a container package with a container type @i, the specific type @i of the object returned from a function that returns an object of an iterator interface, as well as the primitive operations of @i, shall be nonblocking. The Global aspect specified for @i and the primitive operations of @i shall be @fc<(@b @i, @b @i)> or a specification that allows access to fewer global objects. !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 Vector @b @b Constant_Indexing =@> Constant_Reference, Variable_Indexing =@> Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type; @b Preelaborable_Initialization(Vector);> @dby See the conflict file!! !corrigendum A.18.2(47/2) @dinsa @xcode< @b Append (Container : @b Vector; New_Item : @b Element_Type; Count : @b Count_Type := 1);> @dinst @xcode< @b Append_One (Container : @b Vector; New_Item : @b Element_Type) @b Pre =@> (@b Tampering_With_Cursors_Prohibited (Container) @b Program_Error) @b (@b Length (Container) @> Maximum_Length - 1 @b Constraint_Error), Post =@> Length (Container)'Old + 1 = Length (Container) @b Capacity (Container) @>= Length (Container);> !corrigendum A.18.2(125/2) @drepl @xindent @dby @xindent !corrigendum A.18.2(133/3) @drepl @xindent @dby @xindent !corrigendum A.18.2(135/3) @drepl @xindent @dby @xindent !corrigendum A.18.2(175/2) @dinsa @xindent @dinss @xcode<@b Append_One (Container : @b Vector; New_Item : @b Element_Type) @b Pre =@> (@b Tampering_With_Cursors_Prohibited (Container) @b Program_Error) @b (@b Length (Container) @> Maximum_Length - 1 @b Constraint_Error), Post =@> Length (Container)'Old + 1 = Length (Container) @b Capacity (Container) @>= Length (Container);> @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 See the conflict file!! !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 See the conflict file!! !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 See the conflict file!! !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 See the conflict file!! !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 See the conflict file!! !corrigendum A.18.10(8/3) @drepl @xcode< @b Tree @b @b Constant_Indexing =@> Constant_Reference, Variable_Indexing =@> Reference, Default_Iterator =@> Iterate, Iterator_Element =@> Element_Type; @b Preelaborable_Initialization(Tree);> @dby See the conflict file!! !ASIS No ASIS impact. !ACATS test These changes are not intended to change any of the semantics of the containers, so no new ACATS tests are needed. To the extent that the ACATS doesn't test the error cases, C-Tests are needed to do that (but those are needed whether or not this AI is approved). !appendix From: Randy Brukardt Sent: Tuesday, February 11, 2014 12:18 PM [A partial message in response to messages in the thread filed in AI12-0111-1.] > One thing that would have helped is to design all the safety stuff so > that it was in the form of preconditions and postconditions, which > could be easily suppressed. I've suggested that before (including on Friday). It's still possible, of course, it would be compatible to do so (we couldn't use predicates, but preconditions would work). (But it would be a lot of work for the Standard, and some for implementers.) Of course, we couldn't have done this for Ada 2005, as we didn't have preconditions then. In particular, if we added the routine Is_Tampering_with_Cursors (Container : in Vector) return Boolean, then the bounded vector Insert could be: procedure Insert (Container : in out Vector; Before : in Extended_Index; New_Item : in Vector) with Pre => (if Container.Is_Tampering_with_Cursors then raise Program_Error with "Tampering check") and then (if Before not in Container.First_Index .. Container.Last_Index + 1 then raise Constraint_Error) and then (if Container.Length = Container.Capacity then raise Capacity_Error), Post => (Container.Is_Tampering_with_Cursors'Old = Container.Is_Tampering_with_Cursors) and Container.Length'Old + 1 = Container.Length); The postcondition is intended to show provers that a call of Insert doesn't change the tampering state. Having these as preconditions and postconditions would allow easy suppression of the checks (and also would allow the compiler to combine and/or eliminate them, so it wouldn't be as necessary to suppress them). This seems to me to be the best way to fix the performance problem caused by the checking. But that presumes that we're sure that the performance problem is caused solely by the checking. **************************************************************** From: Randy Brukardt Sent: Wednesday, January 11, 2017 7:33 PM [The quote is from the e-mail discussion of AI12-0215-1 - Editor.] >Yes, this exhibit N in the long list of reasons that we should have had all >of the container operations having a container parameter. It strikes me that it might make sense to put on the record all of these reasons. We're talking about a routine like: function Next (Position : Cursor) return Cursor; (1) This routine (and its relatives) is not primitive for the container type, so it doesn't get inherited by derivation. Thus derivation of the container type is incomplete and rather useless; (2) One can't use the prefixed notation to call this routine (Cursor is not tagged, and you wouldn't want it to be the prefix anyway); (3) The Global aspect for this routine is problematic, as we have to include any container object of the correct type. (The object being read not being part of the specification.) That means we either need some unusual Global specification for this case, or we have to fall back to "reads all", which is far from ideal. (Recall that Cursor is a private type, from outside of the package it doesn't appear to designate anything.) (4) Reading and writing the container is not symmetric. One uses different parameter lists for each. (This is mitigated somewhat by the Ada 2012 Reference routine and the indexed notation - probably most new code will use that, but of course the original routines still can be used.) --- If, instead, the routine had been declared as (I'm showing the precondition, which would have been written in English in Ada 2005/12): function Next (Container : Map; Position : Cursor) return Cursor with Pre => (if not Cursor_Belongs_To_Container (Container, Position) then raise Program_Error); The routine is primitive, so (1) and (2) are eliminated (in particular, prefixed notation can be used). The precondition eliminates (3); we only need to include global container state (the storage pool, at a minimum) in the Global aspect [and nothing at all for the bounded containers). (4) is eliminated as Element and Replace have the same type profile (different modes, of course). The only negative is expressed by the precondition: a check is needed that the cursor belongs to the container. Of course as a precondition this can often be eliminated. [It's likely that an earlier precondition or postcondition will have previously checked/asserted this fact, and this could easily be a stable property that doesn't change for most routines.] --- A possibility here would be to add the necessary additional routines. For the Maps, there are only 6 routines that could be added (2 Nexts, 2 Previouses, Key, and Element) -- the others are operators which obviously can't have more parameters. [The next three parameter "<" that I see will be the first. ;-)] That would allow applications that care about Global or want to uniformly use prefixed notation or to do a derivation to work usefully, and won't (I think) require any other code to change. [It would be only incompatible with anyone that decided to add these themselves somewhere; that might make some calls ambiguous. That's the normal problem from added new routines.] I'm thinking that adding these routines might be a good idea, especially for the purposes of AI12-0112-1 (which intends to add Pre/Post/Global/Nonblocking/ Stable_Properties to all of the containers, along with some additional routines to support those, and remove English text where possible). The nasty Global aspect for the existing routines seems to be justification enough (and the other reasons add importance). Any objections to adding them to the next draft of AI12-0112-1??? **************************************************************** From: Randy Brukardt Sent: Thursday, January 12, 2017 3:46 PM [From mail found about AI12-0215-1 - Editor.] > > My initial thought was that this is fine, (with the obvious caveat > > that this is a tagged type, so there has to be a null extension on > > the > > type) but then I remembered that you can't usefully derive > a type in a containers package. > > This seems more of a failing of the structure of the containers > packages, and doesn't argue against the value of the feature more > generally. As you mention below, and we have discovered for other > reasons in the context of SPARK, having cursor operations that don't > take the associated container as a parameter create numerous problems > when it comes to doing anything "formal" with the containers. I take it from this that you agree with my suggestion to add the missing container reading operations so that derivation and formal analysis work appropriately? (I made that a separate thread, that no one seems to have commented on so far.) We can't get rid of the existing operations for obvious reasons, but we could add ones that work "right" and formal uses could just ignore the ones without a container parameter. (That seems like a more practical solution than defining a completely separate set of containers that have better behavior.) **************************************************************** From: Tucker Taft Sent: Thursday, January 12, 2017 4:31 PM [Just the reply to the above message, see AI12-0215-1 for the whole thread - Editor.] > ... I take it from this that you agree with my suggestion to add the > missing container reading operations so that derivation and formal > analysis work appropriately? (I made that a separate thread, that no > one seems to have commented on so far.) Yes, I agree with that proposal. **************************************************************** From: Bob Duff Sent: Sunday, January 15, 2017 6:01 PM > If, instead, the routine had been declared as (I'm showing the > precondition, which would have been written in English in Ada 2005/12): > > function Next (Container : Map; Position : Cursor) return Cursor > with Pre => (if not Cursor_Belongs_To_Container (Container, Position) > then raise Program_Error); I have often thought that those ops should take a Container param. The SPARK folks at AdaCore designed "formal containers" to be used with proofs. Not proving the implementation of the container is correct, but proving that clients obey the pre/post. They came to the same conclusion. They tried to keep their interface similar to the language-defined ones, but they found the need to add the Container params. > I'm thinking that adding these routines might be a good idea, > especially for the purposes of AI12-0112-1 (which intends to add > Pre/Post/Global/Nonblocking/Stable_Properties to all of the > containers, along with some additional routines to support those, and > remove English text where possible). The nasty Global aspect for the > existing routines seems to be justification enough (and the other > reasons add importance). Any objections to adding them to the next draft of > AI12-0112-1??? I don't object to adding those routines, but I think I object to AI12-0112-1. Sounds like a lot of useless work for little gain. And if we do that, it should be done by hacking on an existing container implementation, with regression testing. There's no way ARG can get it right in a vacuum. **************************************************************** From: Randy Brukardt Sent: Monday, January 16, 2017 7:59 PM > I don't object to adding those routines, but I think I object to > AI12-0112-1. Sounds like a lot of useless work for little gain. > > And if we do that, it should be done by hacking on an existing > container implementation, with regression testing. > There's no way ARG can get it right in a vacuum. Why? It certainly doesn't hurt to try the changes in an implementation, but I don't think there is much chance that much beyond a handful of typos would be found. For Pre and Nonblocking, this is just replacing English rules with specifications. It's rather rote; all of the preconditions are of the form "(if Some_Predicate (Container) then raise Some_Exception)", combined with "and then". Any cut-and-errors would be clearly obvious (failing the Dewar rules). Besides, we're planning to use Nonblocking in the entire Ada library (it doesn't work if that's not done), so whether or not a containers overhaul is done isn't relevant to it. For Post/Stable_Properties, we're also encoding the English rules; there's a bit more risk of omission but again errors would be clearly obvious (requiring an obvious nonsense property). Global could be more of a problem, but there I think we have to be very conservative; no existing implementation is going to help much there, as the rules have to allow far more than any single implementation needs -- regardless of design. If there is any risk, it is in the English wording changes (deleting too much certainly would be possible). But if you look at the prototype AI12-0112-1, you'll see that the descriptions of the container operations are *much* more understandable. Getting the English for what really was code was very difficult and probably isn't exactly right. Most likely, we'll fix some errors by this exercise (and probably fix some errors in existing implementations, too, if our experience with containers ACATS tests is any guide). [Indeed, by making these checks first-class preconditions, we will eliminate most of the need for ACATS tests on those checks, which are annoying to write, and only important if someone has screwed up. That would allow redirecting that effort elsewhere.] **************************************************************** topic Pragma Suppress (Container_Checks) !reference Ada 202x 2012 RM11.5, A.18.4 !from Gautier de Montmollin 17-12-05 !keywords Suppress Container_Checks !discussion Hello, Like it or not, GNAT has a pragma Suppress (Container_Checks) which is activated with the -gnatp option. It changes changes the behaviour of Maps (and perhaps other containers) when an element hasn't been found: the behaviour of function Element @ A.18.4 34/2 fails, and Constraint_Error is NOT propagated as expected. Especially, function Element (Container : Map; Key : Key_Type) return Element_Type; (68/2) cannot be used at all. Actually my proposal is either: - For the Ada standard, to add this pragma. It would join the other documented pragmata in 11.5 (Suppressing Checks) that have to be used with caution. - Or for the GNAT compiler, to warn better of the risks of this undocumented (in the Ada standard sense) pragma **************************************************************** From: Randy Brukardt Sent: Tuesday, December 5, 2017 3:57 PM (1) pragma Suppress always causes the risk of making a program's erroneous. If this is a real concern (and it should be), don't use pragma Suppress. (It's almost never necessary with modern compilers which can eliminate the vast majority of checks by optimizations.) [I'm not going to say more here, as it would get off-topic; I had much more to say about this in a recent comp.lang.ada thread.] (2) We already have this issue on our radar. In particular, AI12-0112-1 intends to make almost all of the container checks into explicit preconditions and provide a way to suppress language-defined preconditions. This will make the description of the checks clearer and still provide the functionality if it is needed. (3) 11.5(27/2) allows an implementation to define additional check names for Suppress. There's no requirement that the check names be language-defined. So GNAT is perfectly OK defining Container_Check, Box_Check, Gautier_Check, or any other name that they like. :-) As to the quality of their documentation, that's hardly a language Standard concern. **************************************************************** From: Randy Brukardt Sent: Thursday, December 6, 2018 8:44 PM I've been thinking about the job of putting these contracts into the Standard. I've concluded that writing a full AI for this would just double the work, as I'd have to create an AI version of the changes, and then put the same changes into RM. While this might be good for my bank account (and that assumes an unlimited willingness of AdaCore to put in more money -- something that does not likely exist), it seems silly. My thinking is that simply putting the changes directly into the RM, with proper change marks, would be likely more useful for human reviewers than any amount of time spent on the actual AI. Moreover, for machine testing, it is relatively easy to extract the required specifications from the RM (it would be easy to write a tool to process the HTML to do that, including removing the paragraph numbers which would prevent directly cut-and-pasting). Machine testing seems mandated, although having a compiler that could ignore Nonblocking and Global aspects would seem very useful (else having a tool to strip those would be required - doing it by hand would take ages). However, in order to follow this approach, I'll need essentially a "blank check" to make such changes as described in AI12-0112-1. Once these changes are inserted in the RM (at the same time as changes for AIs 212, 111, and 266) would pretty much mean that the work to back them out would be equivalent to the original work. (Summary: not gonna happen.) Is this a reasonable approach? Should I put this on the agenda for discussion on Monday??? **************************************************************** From: Tucker Taft Sent: Thursday, December 6, 2018 9:35 PM Makes sense to me. It would be nice to do this during a "lull" in making other changes to the RM, so we could review the final product before signing off on it. **************************************************************** From: Randy Brukardt Sent: Friday, December 14, 2018 9:15 PM We've talked on several occasions about having a global permission for implementation-defined packages to appear in the Global specification of language-defined entities. This is needed, for instance, to support an implementation-defined helper package that implements all of the low-level IO operations. If that package has state, it needs to appear in the global contracts of packages that use it. Forcing implementations to move all of the state seems like a nightmare for implementers and adverse to good Ada design practice (share as much as possible of the implementation). At the recent meeting we talked about putting this into the start of Annex A. We also talked about allowing additional postconditions, which we agreed was possible without any permission. Here is suggested wording for this permission and some associated AARM notes. Improvements welcome. ============= Add after Annex A(4): [Implementation Permissions] The implementation may add specifications of synchronized entities of implementation-defined packages to the global specification for any language-defined entity that is not declare pure or has a global specification of \null\. AARM Reason: Ada runtime libraries often use implementation-defined helper packages to implement the language-defined units. For instance, it is common to use a common low-level package to implement I/O; if that package includes support for Current Input and Current Output, then it is likely to have state that needs to be reflected in the packages that use it such as Ada.Text_IO. We want to allow such packages, so we have defined this permission to allow them to include state if necessary. We require that any such state is synchronized to ensure that appropriate use (as defined above) is allowed in parallel operations. We exclude units that are declared pure from this permission since this is a declaration that the unit doesn't have any global state, so specifying otherwise would defeat the purpose. Similarly, entities that explicitly specify Global as \null\ are supposed to have no side-effects, and we don't want implementations to add any. End AARM Reason. AARM Ramification: Implementations are allowed to make other changes to the specifications of language-defined units, so long as those changes are semantically neutral (that is, no program could change legality or effect because of the changes). In particular, an implementation would need to add implementation-defined units to the context clause in order to use the previous permission; this is allowed and does not need a separate permission. Similarly, an implementation can add/enhance postconditions to language-defined subprograms, so long as those postconditions reflect the definition of the subprogram. This might be useful, for instance, if the implementation can use those postconditions to eliminate following code (perhaps by proving that a following precondition must be true based on the postcondition). End AARM Ramification. **************************************************************** From: Bob Duff Sent: Saturday, December 15, 2018 10:50 AM > Here is suggested wording for this permission and some associated AARM > notes. > ... Looks good to me. By the way, how would one express the fact that Text_IO is messing around with the state on the disk? Is that even possible? > AARM Ramification: Implementations are allowed to make other changes > to the specifications of language-defined units, so long as those > changes are semantically neutral (that is, no program could change > legality or effect because of the changes). In particular, an > implementation would need to add implementation-defined units to the > context clause in order to use the previous permission; this is > allowed and does not need a separate permission. That's so obvious, I'm tempted to add "of course": "Implementations are allowed..." And maybe remove the parenthetical remark -- anybody reading the AARM should know what "semantically neutral" means. > Similarly, an implementation can add/enhance postconditions to > language-defined subprograms, so long as those postconditions reflect > the definition of the subprogram. This might be useful, for instance, > if the implementation can use those postconditions to eliminate > following code (perhaps by proving that a following precondition must > be true based on the postcondition). I suggest shortening that a bit: Similarly, an implementation can add postconditions to language-defined subprograms, so long as those postconditions are True. This is useful if the implementation can use those postconditions for optimization. *************************************************************** From: Bob Duff Sent: Saturday, December 15, 2018 10:58 AM > That's so obvious, I'm tempted to add "of course": > "Implementations are allowed..." Ooops, I meant to write: That's so obvious, I'm tempted to add "of course": "Implementations are of course allowed..." ^^^^^^^^^ Of COURSE that's what I meant! ;-) *************************************************************** From: Randy Brukardt Sent: Sunday, December 16, 2018 12:09 AM > > Here is suggested wording for this permission and some associated > > AARM notes. > > ... > > Looks good to me. Thanks for the comments. > By the way, how would one express the fact that Text_IO is messing > around with the state on the disk? > Is that even possible? Not sure. I've always imagined it as the "state" of one of the helper packages, but I don't know if that is really the right model. ... > And maybe remove the parenthetical remark -- anybody reading the AARM > should know what "semantically neutral" means. I've heard several times from people on comp.lang.ada that they found the AARM interesting reading. That is, not everyone reading it is an implementer or language lawyer. (I probably would have found it interesting had it existed when I was at the University of Wisconsin.) So I don't want to assume too much about the reader's knowledge. Besides, it really easy to assume that such things are obvious when you've been talking about such things for decades. So I think the parenthetical remark is helpful to some readers, and reinforcing to others (including me!). > > Similarly, an implementation can add/enhance postconditions to > > language-defined subprograms, so long as those postconditions > > reflect the definition of the subprogram. This might be useful, for > > instance, if the implementation can use those postconditions to > > eliminate following code (perhaps by proving that a following > > precondition must be true based on the postcondition). > > I suggest shortening that a bit: > > Similarly, an implementation can add postconditions to > language-defined subprograms, so long as those postconditions > are True. This is useful if the > implementation can use those postconditions for optimization. Seems a bit too short to me, it seems to say that you can only add "True" as postconditions. (Obviously, no one would write a note to say that, so it's nonsense, but it takes some thought to figure that out.) How about: Similarly, an implementation can add postconditions to language-defined subprograms, so long as those postconditions always evaluate to True. This is useful if the implementation can use those postconditions for optimization. or maybe "always would evaluate to True" (since they won't actually be evaluated in most circumstances). *************************************************************** From: Bob Duff Sent: Sunday, December 16, 2018 1:50 PM > Seems a bit too short to me, it seems to say that you can only add > "True" as postconditions. Good point. > Similarly, an implementation can add postconditions to > language-defined subprograms, so long as those postconditions > always evaluate to True. This is useful if the > implementation can use those postconditions for optimization. Yes, that's better. > or maybe "always would evaluate to True" (since they won't actually be > evaluated in most circumstances). I slightly prefer leaving out the "would". ***************************************************************