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

Differences between 1.3 and version 1.4
Log of other versions for file 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