CVS difference for ai12s/ai12-0112-1.txt
--- ai12s/ai12-0112-1.txt 2018/01/18 20:36:46 1.3
+++ ai12s/ai12-0112-1.txt 2018/03/02 02:14:10 1.4
@@ -1,16 +1,26 @@
-!standard A.18.2(99/3) 14-05-15 AI12-0112-1/01
+!standard A.18.2(99/3) 18-03-01 AI12-0112-1/02
!class Amendment 14-05-15
!status work item 14-05-15
!status received 15-02-11
!priority Medium
-!difficulty Hard
-!subject Preconditions for container operations
+!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.
+
+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
@@ -18,27 +28,195 @@
which would make them available to compilers for optimization and to proof
tools, as well as being less ambiguous for human readers.
-** Must add some text about the missing reading operations -- see the January 2017
-mail in this AI **
+Additionally, check suppression 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.
+Therefore, we add new analogs of these operations that include a container
+parameter.
+
!proposal
(See summary.)
+[Questions:
+
+(1) I used the name "Container_Check" for the check name (for use in pragma
+Suppress). This sort of stomps on GNAT's existing implementation, although
+they should be pretty close in functionality (exceptions not raised through
+preconditions are not included in this Ada definition). Is this a problem?
+Is there an alternative name? (See !discussion.)
+
+(2) Should the preconditions be repeated in the semantics section or just
+shown in the package specification? I have them repeated for now, but that's
+relatively easy to change.
+
+(3) I 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). Objections?
+
+(4) I've overridden 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. Can anyone think of a reason NOT to require these routines to be
+pure (in general or specifically)?
+
+(5) 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. I'm assuming that is the case.
+
+(6) I had to use prefixed notation in some preconditions, as the function
+I wanted to call 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. Should all
+of these be written in prefixed notation for consistency? (We decided the
+reverse the previous time, I think.) I suppose I could have used an expanded
+name instead (Vectors.Length (Container)) - but that's just longer for no
+obvious reason.
+
+(7) I intend to check that this specification is compilable, and would prefer
+to check it against GNAT's existing implementation (meaning compiling the spec
+with the existing GNAT body enhanced with the additional routines). For that,
+I'll need some help from someone at AdaCore, as I don't have access to the
+AdaCore test suite and would need help finding the source code and recompiling
+part of the runtime with GNAT (never having done that). Is there a volunteer??
+
+(8) It would be best if we had a way to specify a precondition for anonymous
+access-to-subprogram types in order to properly handle
+Tampering_With_Cursors_Prohibited for
+Query_Element/Update_Element/subprogram iterators. None has been proposed
+to date. (The only sane way seems to be via a named anonymous access subtype,
+which clearly would need a better name. ;-)
+
+We also would need a way to indicate that Tampering_With_Cursors_Prohibited
+is true during the lifetime of an iterator or reference object. It's not clear
+to me how best to indicate this in the specification of the containers.
+Perhaps SPARK users would have a suggestion.
+
+Neither of these are critical, in the sense that the specification will work
+without them. It just means that tools and compilers cannot detect failing
+tampering checks (and optimize away unnecessary checks) based on these
+properties alone.
+
+]
+
+
!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 &
+ in out Ada.Containers.Vectors &
+ <<some impl-defed helper packages>> 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. <<some impl-defed helper packages>> is a placeholder for however we
+decide to deal with helper packages. Note that in the Bounded version, Global
+is just Equal_Element'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,
+ Stable_Properties => Length, Capacity, Tampering_With_Cursors_Prohibited,
+ Tampering_With_Elements_Prohibited;
+ 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.]
+
+[The rest of the package is as described in the detailed wording below. The
+specs would match.]
+
-Prototype of revised package Ada.Containers.Vectors, paragraphs A.18.2(97.2/3)
-through A.18.2(237).
+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;
+function Has_Element (Position : Cursor) return Boolean
+ with Nonblocking => True,
+ Global => 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 => True,
+ Global => in out 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.
@@ -48,32 +226,29 @@
raised during evaluation of element equality is propagated.
New
-function Cursor_Belongs_To_Container (Container : Vector; Position : Cursor)
- return Boolean;
+function Tampering_With_Cursors_Prohibited (Container : Vector) return Boolean
+ with Nonblocking => True,
+ Global => in out null;
New
-Returns True if Position designates an element in Container, and returns False
-otherwise.
-
-New AARM Ramification:
-If Position is No_Element, Cursor_Belongs_To_Container returns False.
-
-New
-function Tampering_With_Cursors_Prohibited (Container : Vector) return Boolean;
-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;
+function Tampering_With_Elements_Prohibited (Container : Vector) return Boolean
+ with Nonblocking => True,
+ Global => in out null;
New
Returns True if tampering with elements is currently prohibited for Container,
and returns False otherwise.
100/2+
function To_Vector (Length : Count_Type) return Vector
- with Post'Class => Length (To_Vector'Result) = Length;
+ with Post => To_Vector'Result.Length = Length and then
+ not Tampering_With_Elements_Prohibited (To_Vector'Result) and then
+ not Tampering_With_Cursors (To_Vector'Result) and then
+ To_Vector'Result.Capacity >= Length;
101/2
Returns a vector with a length of Length, filled with empty elements.
@@ -81,14 +256,20 @@
function To_Vector
(New_Item : Element_Type;
Length : Count_Type) return Vector
- with Post'Class => Length (To_Vector'Result) = Length;
+ with Post => Length (To_Vector'Result) = Length and then
+ not Tampering_With_Elements_Prohibited (To_Vector'Result) and then
+ not Tampering_With_Cursors (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 Post'Class => Length ("&"'Result) = Length (Left) + Length (Right);
+ with Post => Length (Vectors."&"'Result) = Length (Left) + Length (Right),
+ not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
+ not Tampering_With_Cursors (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.
@@ -96,31 +277,44 @@
106/2+
function "&" (Left : Vector;
Right : Element_Type) return Vector
- with Post'Class => Length ("&"'Result) = Length (Left) + 1;
+ with Post => Vectors."&"'Result.Length = Length (Left) + 1 and then
+ not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
+ not Tampering_With_Cursors (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 Post'Class => Length ("&"'Result) = Length (Right) + 1;
+ with Post => Length (Vectors."&"'Result) = Length (Right) + 1 and then
+ not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
+ not Tampering_With_Cursors (Vectors."&"'Result),
+ 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 Post'Class => Length ("&"'Result) = 2;
+ with Post => Length ("&"'Result) = 2 and then
+ not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
+ not Tampering_With_Cursors (Vectors."&"'Result) and
+ 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;
+function Capacity (Container : Vector) return Count_Type
+ with Nonblocking => True,
+ Global => in out null;
113/2
Returns the capacity of Container.
114/2
procedure Reserve_Capacity (Container : in out Vector;
- Capacity : in Count_Type);
+ 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
@@ -132,16 +326,19 @@
is propagated and Container is not modified.
116/2
-function Length (Container : Vector) return Count_Type;
+function Length (Container : Vector) return Count_Type
+ with Nonblocking => True,
+ Global => in out 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'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error),
- Post'Class => Length (To_Vector'Result) = Length;
+ with Pre => (if Tampering_With_Cursors_Prohibited (Container)
+ then raise Program_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
@@ -149,15 +346,17 @@
elements are added to Container; otherwise, elements are removed from Container.
120/2
-function Is_Empty (Container : Vector) return Boolean;
+function Is_Empty (Container : Vector) return Boolean
+ with Nonblocking => True,
+ Global => in out null;
121/2
Equivalent to Length (Container) = 0.
122/2+
procedure Clear (Container : in out Vector)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
+ with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
- Post'Class => Length (Container) = 0;
+ Post => Length (Container) = 0;
123/2
Removes all the elements from Container. The capacity of Container does not
change.
@@ -165,75 +364,113 @@
124/2+
function To_Cursor (Container : Vector;
Index : Extended_Index) return Cursor
- with Post'Class => (if Index in First_Index (Container) .. Last_Index (Container)
- then Cursor_Belongs_To_Container (Container, To_Cursor'Result)
- else To_Cursor'Result = No_Element);
+ 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 => True;
125/2
If Index is not in the range First_Index (Container) .. Last_Index (Container),
then No_Element is returned. Otherwise, a cursor designating the element at
-position Index in Container is returned.
+position Index in Container is returned. 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;
+function To_Index (Position : Cursor) return Extended_Index
+ with Global => Vectors'Global & in access Vector,
+ Nonblocking => True;
+
+[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
+ when 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 => True;
+New
+If Position is No_Element, No_Index is returned. Otherwise, the index (within
+its containing vector) of the element designated by Position is returned.
+
128/2+
function Element (Container : Vector;
Index : Index_Type)
return Element_Type
- with Pre'Class => (if Index not in First_Index (Container) .. Last_Index (Container)
+ with Pre => (if Index not in First_Index (Container) .. Last_Index (Container)
then raise Constraint_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ Nonblocking => True;
+
129/2+
Element returns the element at position Index.
130/2+
function Element (Position : Cursor) return Element_Type
- with Pre'Class => (if Position = No_Element then raise Constraint_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ with Pre => (if Position = No_Element then raise Constraint_Error),
+ Nonblocking => True,
+ Global => Vectors'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 => True;
+New
+Element returns the element designated by Position.
+
+
132/2+
procedure Replace_Element (Container : in out Vector;
Index : in Index_Type;
New_Item : in Element_Type)
- with Pre'Class => (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),
- Post'Class => Length (Container)'Old = Length (Container);
+ 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.
+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'Class => (if Tampering_With_Elements_Prohibited (Container)
- then raise Program_Error) and then
- (if Position = No_Element then raise Constraint_Error) and then
- (if not Cursor_Belongs_To_Container (Container, Position)
- then raise Program_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ 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.
+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'Class => (if Index not in First_Index (Container) .. Last_Index (Container)
- then raise Constraint_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ with Pre => (if Index not in First_Index (Container) .. Last_Index (Container)
+ then raise Constraint_Error);
+
+[Tampering ought to be indicated for the access procedure here, but we don't
+have a mechanism to do that. See the questions above.]
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
@@ -244,8 +481,7 @@
procedure Query_Element
(Position : in Cursor;
Process : not null access procedure (Element : in Element_Type))
- with Pre'Class => (if Position = No_Element then raise Constraint_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ with Pre => (if Position = No_Element then raise Constraint_Error);
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
@@ -257,9 +493,8 @@
(Container : in out Vector;
Index : in Index_Type;
Process : not null access procedure (Element : in out Element_Type))
- with Pre'Class => (if Index not in First_Index (Container) .. Last_Index (Container)
- then raise Constraint_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ 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
@@ -281,10 +516,8 @@
(Container : in out Vector;
Position : in Cursor;
Process : not null access procedure (Element : in out Element_Type))
- with Pre'Class => (if Position = No_Element then raise Constraint_Error) and then
- (if not Cursor_Belongs_To_Container (Container, Position)
- then raise Program_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ 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
@@ -314,9 +547,8 @@
function Constant_Reference (Container : aliased in Vector;
Index : in Index_Type)
return Constant_Reference_Type
- with Pre'Class => (if Index not in First_Index (Container) .. Last_Index (Container)
- then raise Constraint_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ with Pre => (if Index not in First_Index (Container) .. Last_Index (Container)
+ then raise Constraint_Error);
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
@@ -331,9 +563,8 @@
function Reference (Container : aliased in out Vector;
Index : in Index_Type)
return Reference_Type
- with Pre'Class => (if Index not in First_Index (Container) .. Last_Index (Container)
- then raise Constraint_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ with Pre => (if Index not in First_Index (Container) .. Last_Index (Container)
+ then raise Constraint_Error);
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
@@ -351,10 +582,9 @@
function Constant_Reference (Container : aliased in Vector;
Position : in Cursor)
return Constant_Reference_Type
- with Pre'Class => (if Position = No_Element then raise Constraint_Error) and then
- (if not Cursor_Belongs_To_Container (Container, Position)
- then raise Program_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ with Pre => (if Position = No_Element then raise Constraint_Error) and then
+ (if not Has_Element (Container, Position)
+ then raise Program_Error);
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
@@ -369,10 +599,9 @@
function Reference (Container : aliased in out Vector;
Position : in Cursor)
return Reference_Type is
- with Pre'Class => (if Position = No_Element then raise Constraint_Error) and then
- (if not Cursor_Belongs_To_Container (Container, Position)
- then raise Program_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ with Pre => (if Position = No_Element then raise Constraint_Error) and then
+ (if not Has_Element (Container, Position)
+ then raise Program_Error);
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
@@ -388,9 +617,10 @@
147.19/3+
procedure Assign (Target : in out Vector; Source : in Vector)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Target)
+ with Pre => (if Tampering_With_Cursors_Prohibited (Target)
then raise Program_Error),
- Post'Class => Length (Source) = Length (Target);
+ 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
@@ -401,49 +631,50 @@
147.21/3+
function Copy (Source : Vector; Capacity : Count_Type := 0)
return Vector
- with Pre'Class => (if Capacity /= 0 and then Capacity < Length (Source)
- then raise Capacity_Error),
- Post'Class => Length (Copy'Result) = Length (Source);
+ with Pre => (if Capacity /= 0 and then Capacity < Length (Source)
+ then raise Capacity_Error),
+ Post => Length (Copy'Result) = Length (Source) 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. If Capacity is 0, then the vector capacity is the length of Source;
-if Capacity is equal to or greater than the length of Source, the vector
-capacity is at least the specified value.
+of Source.
148/2+
procedure Move (Target : in out Vector;
Source : in out Vector)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Target)
- then raise Program_Error) and then
- (if Tampering_With_Cursors_Prohibited (Source)
- then raise Program_Error),
- Post'Class => (if Target = Source then True
- else
- Length (Target) = Length (Source'Old) and then
- Length (Source) = 0);
-149/3
+ 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. The length of Source is 0 after a
-successful call to Move.
+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'Class => (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),
- Post'Class => Length (Container)'Old + Length (New_Item) = Length (Container);
+ 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) + Length (New_Item) > Index_Type'Last
+ 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); if the
-value of Last appropriate for length NL would be greater than Index_Type'Last,
-then Constraint_Error is propagated.
-[Editor's note: This last check might overflow if written as a Precondition;
-I didn't try.]
+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
@@ -455,13 +686,16 @@
procedure Insert (Container : in out Vector;
Before : in Cursor;
New_Item : in Vector);
- with Pre'Class => (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 Cursor_Belongs_To_Container (Container, Before))
- then raise Program_Error),
- Post'Class => Length (Container)'Old + Length (New_Item) = Length (Container);
+ 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) + Length (New_Item) > Index_Type'Last
+ 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,
@@ -473,13 +707,14 @@
Before : in Cursor;
New_Item : in Vector;
Position : out Cursor);
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error) and then
- (if Before /= No_Element and then
- (not Cursor_Belongs_To_Container (Container, Before))
- then raise Program_Error),
- Post'Class => Length (Container)'Old + Length (New_Item) = Length (Container) and then
- Cursor_Belongs_To_Container (Container, Position);
+ 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),
+ 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
@@ -490,11 +725,14 @@
Before : in Extended_Index;
New_Item : in Element_Type;
Count : in Count_Type := 1)
- with Pre'Class => (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),
- Post'Class => Length (Container)'Old + Count = Length (Container);
+ 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) + Count > Index_Type'Last
+ 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));
@@ -503,13 +741,16 @@
Before : in Cursor;
New_Item : in Element_Type;
Count : in Count_Type := 1)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error) and then
- (if Count /= 0 and then
- Before /= No_Element and then
- (not Cursor_Belongs_To_Container (Container, Before))
- then raise Program_Error),
- Post'Class => Length (Container)'Old + Count = Length (Container);
+ 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) + Count > Index_Type'Last
+ 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));
@@ -519,13 +760,14 @@
New_Item : in Element_Type;
Position : out Cursor;
Count : in Count_Type := 1)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error) and then
- (if Before /= No_Element and then
- (not Cursor_Belongs_To_Container (Container, Before))
- then raise Program_Error),
- Post'Class => Length (Container)'Old + Count = Length (Container) and then
- Cursor_Belongs_To_Container (Container, Position);
+ 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),
+ 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);
@@ -533,16 +775,17 @@
procedure Insert (Container : in out Vector;
Before : in Extended_Index;
Count : in Count_Type := 1)
- with Pre'Class => (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),
- Post'Class => Length (Container)'Old + Count = Length (Container);
+ 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) + Count > Index_Type'Last
+ 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; if the value of Last appropriate
-for length NL would be greater than Index_Type'Last, then Constraint_Error is
-propagated.
+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
@@ -555,14 +798,17 @@
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error) and then
- (if Before /= No_Element and then
- (not Cursor_Belongs_To_Container (Container, Before))
- then raise Program_Error),
- Post'Class => Length (Container)'Old + Count = Length (Container) and then
- Cursor_Belongs_To_Container (Container, Position);
-167/2
+ 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) + Count > Index_Type'Last
+ 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).
@@ -570,9 +816,12 @@
168/2+
procedure Prepend (Container : in out Vector;
New_Item : in Vector)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error),
- Post'Class => Length (Container)'Old + Length (New_Item) = Length (Container);
+ with Pre => (if Tampering_With_Cursors_Prohibited (Container)
+ then raise Program_Error) and then
+ (if Length (Container) + Length (New_Item) > Index_Type'Last
+ 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).
@@ -580,18 +829,24 @@
procedure Prepend (Container : in out Vector;
New_Item : in Element_Type;
Count : in Count_Type := 1)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error),
- Post'Class => Length (Container)'Old + Count = Length (Container);
+ with Pre => (if Tampering_With_Cursors_Prohibited (Container)
+ then raise Program_Error) and then
+ (if Length (Container) + Count > Index_Type'Last
+ 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'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error),
- Post'Class => Length (Container)'Old + Length (New_Item) = Length (Container);
+ with Pre => (if Tampering_With_Cursors_Prohibited (Container)
+ then raise Program_Error) and then
+ (if Length (Container) + Length (New_Item) > Index_Type'Last
+ 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).
@@ -599,9 +854,12 @@
procedure Append (Container : in out Vector;
New_Item : in Element_Type;
Count : in Count_Type := 1)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error),
- Post'Class => Length (Container)'Old + Count = Length (Container);
+ with Pre => (if Tampering_With_Cursors_Prohibited (Container)
+ then raise Program_Error) and then
+ (if Length (Container) + Count > Index_Type'Last
+ 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).
@@ -609,16 +867,17 @@
procedure Insert_Space (Container : in out Vector;
Before : in Extended_Index;
Count : in Count_Type := 1);
- with Pre'Class => (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),
- Post'Class => Length (Container)'Old + Count = Length (Container);
-177/3
+ 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) + Count > Index_Type'Last
+ 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; if the value of Last
-appropriate for length NL would be greater than Index_Type'Last, then
-Constraint_Error is propagated.
+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
@@ -630,13 +889,16 @@
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error) and then
- (if Before /= No_Element and then
- (not Cursor_Belongs_To_Container (Container, Before))
- then raise Program_Error),
- Post'Class => Length (Container)'Old + Count = Length (Container) and then
- Cursor_Belongs_To_Container (Container, Position);
+ 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),
+ (if Length (Container) + Count > Index_Type'Last
+ 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
@@ -646,11 +908,11 @@
procedure Delete (Container : in out Vector;
Index : in Extended_Index;
Count : in Count_Type := 1)
- with Pre'Class => (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),
- Post'Class => Length (Container)'Old - Count <= Length (Container);
+ 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),
+ 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
@@ -660,12 +922,12 @@
procedure Delete (Container : in out Vector;
Position : in out Cursor;
Count : in Count_Type := 1)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error) and then
- (if Position = No_Element then raise Constraint_Error) and then
- (if not Cursor_Belongs_To_Container (Container, Position)
- then raise Program_Error),
- Post'Class => Length (Container)'Old - Count <= Length (Container);
+ 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);
184/2
Delete (Container, To_Index (Position), Count) is called, and then
Position is set to No_Element.
@@ -673,18 +935,18 @@
185/2+
procedure Delete_First (Container : in out Vector;
Count : in Count_Type := 1)
- with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error),
- Post'Class => Length (Container)'Old - Count <= Length (Container);
+ 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'Class => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error),
- Post'Class => Length (Container)'Old - Count <= Length (Container);
+ 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,
@@ -692,105 +954,181 @@
189/2+
procedure Reverse_Elements (Container : in out Vector)
- with Pre'Class => (if Tampering_With_Elements_Prohibited (Container)
- then raise Program_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ 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'Class => (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),
- Post'Class => Length (Container)'Old = Length (Container);
+ 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'Class => (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 Cursor_Belongs_To_Container (Container, I)
- then raise Program_Error) and then
- (if not Cursor_Belongs_To_Container (Container, J)
- then raise Program_Error),
- Post'Class => Length (Container)'Old - Count <= Length (Container);
+ 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;
+function First_Index (Container : Vector) return Index_Type is
+ with Nonblocking => True,
+ Global => in out 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'Class => (if not Is_Empty (Container)
- then Cursor_Belongs_To_Container (Container, First'Result)
- else First'Result = No_Element);
+ with Post => (if not Is_Empty (Container)
+ then Has_Element (Container, First'Result)
+ else First'Result = No_Element);
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;
+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;
+function Last_Index (Container : Vector) return Extended_Index
+ with Nonblocking => True,
+ Global => in out 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'Class => (if not Is_Empty (Container)
- then Cursor_Belongs_To_Container (Container, Last'Result)
- else Last'Result = No_Element);
+ with Post => (if not Is_Empty (Container)
+ then Has_Element (Container, Last'Result)
+ else Last'Result = No_Element);
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;
+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;
+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.
-209/2
-procedure Next (Position : in out Cursor);
+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
+ else Next'Result = No_Element and then
+ Position'Old = Last (Container)),
+ Global => in out null,
+ Nonblocking => True;
+New
+If Position equals No_Element or designates the last element of 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.
+
+209/2+
+procedure Next (Position : in out Cursor)
+ with Global => Vectors'Global & in access Vector,
+ Nonblocking => True;
210/2
Equivalent to Position := Next (Position).
-211/2
-function Previous (Position : Cursor) return Cursor;
+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 => in out 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.
-213/2
-procedure Previous (Position : in out Cursor);
+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
+ else Previous'Result = No_Element and then
+ Position'Old = First (Container)),
+ Global => in out null,
+ Nonblocking => True;
+New
+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.
+
+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 => in out null,
+ Nonblocking => True;
+New
+Equivalent to Position := Previous (Position).
+
215/2
function Find_Index (Container : Vector;
Item : Element_Type;
@@ -808,11 +1146,11 @@
Item : Element_Type;
Position : Cursor := No_Element)
return Cursor
- with Pre'Class => (if Position /= No_Element and then
- (not Cursor_Belongs_To_Container (Container, Position))
- then raise Program_Error),
- with Post'Class => (if Find'Result then True
- else Cursor_Belongs_To_Container (Container, Find'Result));
+ 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
@@ -840,11 +1178,11 @@
Item : Element_Type;
Position : Cursor := No_Element)
return Cursor
- with Pre'Class => (if Position /= No_Element and then
- (not Cursor_Belongs_To_Container (Container, Position))
- then raise Program_Error),
- with Post'Class => (if Reverse_Find'Result then True
- else Cursor_Belongs_To_Container (Container, Reverse_Find'Result));
+ 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
@@ -863,8 +1201,7 @@
227/2+
procedure Iterate
(Container : in Vector;
- Process : not null access procedure (Position : in Cursor))
- with Post'Class => Length (Container)'Old = Length (Container);
+ Process : not null access procedure (Position : in Cursor));
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
@@ -875,7 +1212,6 @@
procedure Reverse_Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
- with Post'Class => Length (Container)'Old = Length (Container);
230/3
Iterates over the elements in Container as per procedure Iterate, except that
elements are traversed in reverse index order.
@@ -894,13 +1230,13 @@
iterator_specification denotes this object). The iterator object needs
finalization.
-230.3/3
+230.3/3+
function Iterate (Container : in Vector; Start : in Cursor)
return Vector_Iterator_Interfaces.Reversible_Iterator'Class;
-230.4/3
-If Start is not No_Element and does not designate an item in Container, then
-Program_Error is propagated. If Start is No_Element, then Constraint_Error is
-propagated. Otherwise, Iterate returns a reversible iterator object (see 5.5.1)
+ with Pre => (if Start = No_Element then raise Constraint_Error) and then
+ (if not Has_Element (Start, Position) then raise Program_Error);
+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
@@ -928,8 +1264,7 @@
234/2+
procedure Sort (Container : in out Vector)
with Pre'Class => (if Tampering_With_Elements_Prohibited (Container)
- then raise Program_Error),
- Post'Class => Length (Container)'Old = Length (Container);
+ then raise Program_Error);
[We could check in the postcondition that these are sorted, but that's rather
expensive, and these assertions won't usually be ignored.]
235/2
@@ -944,12 +1279,14 @@
then raise Program_Error) and then
(if Tampering_With_Elements_Prohibited (Source)
then raise Program_Error),
- Post'Class => Length (Source) = 0 and then
- Length (Target) = Length (Source)'Old + Length (Target)'Old;
+ Post'Class => (if Target = Source then True
+ else Length (Source) = 0 and then
+ Length (Target) =
+ Length (Source)'Old + Length (Target)'Old and then
+ Capacity (Target) >=
+ Length (Source)'Old + Length (Target)'Old;
[Checking whether these are sorted is too expensive, so we won't try;
-especially as wee don't specify what happens if they're not.
-We don't have a foolproof way to check if these are the same object,
-so we don't try that, either.]
+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
@@ -960,26 +1297,126 @@
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
+
+[So far as I can tell, the contracts of Vectors are also correct for
+Indefinite_Vectors. The capacity rules and heap usage are essentially
+similar.]
+
+-----------------------------------------
+
+A.18.19 The Generic Package Containers.Bounded_Vectors
+
+Add after A.18.19(3/3):
+
+* The Global aspect of the package is replaced by
+ Global => in out null,
+
+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.
+
+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 <some length expression> > Index_Type'Last
+ then raise Constraint_Error)
+ is replaced by:
+ (if <some length expression> > Index_Type'Last
+ then raise Constraint_Error) and then
+ (if <some length expression> > Container.Capacity
+ then raise Capacity_Error)
+
+
+-----------------------------------------
+
+
+Add after 11.5(23):
+
+Redundant[The following check corresponds to situations in which the exception
+Assertion_Error is raised upon failure.]
+
+Container_Check
+
+Check the precondition of a routine declared in a child unit of Ada.Containers
+or in an instance of a generic unit declared in a child unit of
+Ada.Containers.
+
+AARM Reason: One could use the 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 includes
+/raise/ Program_Error 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.
+
!discussion
-For this initial version, we've prototyped the changes needed for a single
-package (Ada.Containers.Vectors). The other 6 basic containers would need
-similar wording changes. We also might want some additional preconditions
-related to capacity for the bounded versions (although that would be
-painful to do, as the bounded versions are described by difference).
-
-Since the other containers would be very similar, we did just this
-one container in order to determine whether it is worth following through with
-the effort to do the remainder of the containers.
-
-The prototype only shows the wording for the main body of the definition
-of Ada.Containers.Vectors. 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.
+For this version, we've prototyped the changes needed for a single
+package (Ada.Containers.Vectors) and the bounded and indefinite versions thereof.
+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. All other operations are pre-existing; the
+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
@@ -987,43 +1424,45 @@
converting English checks to Ada expressions. (A lot of connector words
were dropped, especially "otherwise", which should improve readability.)
-The prototype includes very simple postconditions on the operations. These
-are by no means complete; for instance, we could easily have postconditions
-on the capacity of the container. The question of how far we ought to go with
-postconditions is one that will need to be discussed.
-
-One postcondition not included that should be is
- Tampering_With_Cursors_Prohibited (Container)'Old = Tampering_With_Cursors_Prohibited (Container) and
- Tampering_With_Elements_Prohibited (Container)'Old = Tampering_With_Elements_Prohibited (Container)
-
-This says that the tampering state is not changed by the subprogram. Knowing
-that will allow compilers to eliminate extra tampering checks - often multiple
-modifications will be grouped together such that only a single check is needed.
-
-This should be included on every subprogram that has a Container parameter other
-that Reference and Constant_Reference. (Note that the routines with callbacks,
-like Iterate and Query_Element, change the tampering state internally, but the
-state is unchanged when they complete.) I would suggest doing that with a
-blanket rule rather than cluttering the definitions with these two extra lines.
-
-There are two additional issues with this addition. First, most of the reading
-routines do not have a Container parameter. We would need a global out
-annotation (Global out => null) on most of those routines to state that the
-container tampering state (as well as any other global state) is unchanged.
-If we had such an annotation, we would probably want to specify it with a
-blanket rule as well. (But we could also forget the blanket rules and simply
-repeat these on every routine, after all, that's what an implementation would
-do. Or alternatively, write everything out in the package specification and
-use a simplified version in the body of the clause.)
-
-Second, I don't see any way to show where the tampering is prohibited. That
-occurs in callbacks (Query_Element, Update_Element, Iterate, Reverse_Iterate),
-when an iterator object returned by Iterate is used, and during the lifetime
-of the object returned by Reference and Constant_Reference. Unfortunately,
-none of these places can be described by the constract aspects currently
-available with Ada. One could imagine having appropriate preconditions on
-the callback access values such that we could describe it there, but I don't
-have any idea of a way to describe its association with use of the objects.
+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). 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.)
+
+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.
+
+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 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).
!ASIS
Questions? Ask the ACAA Technical Agent