CVS difference for ai12s/ai12-0112-1.txt
--- ai12s/ai12-0112-1.txt 2019/02/07 06:31:29 1.13
+++ ai12s/ai12-0112-1.txt 2019/02/14 05:25:23 1.14
@@ -38,10 +38,10 @@
which would make them available to compilers for optimization and to proof
tools, as well as being less ambiguous for human readers.
-Additionally, check suppression 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.
+Additionally, check suppression for containers is a missing feature in Ada.
+While a user of an array can suppress checks if they are sufficiently
+convinced of correctness (and thus get better performance), there is no way
+to do this for the containers.
We also need to add the Nonblocking (AI12-0064-2) and Global (AI12-0079-1)
aspects to the containers, so that they can usefully be used with the new
@@ -60,87 +60,10 @@
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.) [This is fine.]
-
-(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. [Repeated.]
-
-(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? [This is OK.]
-
-(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. But that shouldn't be necessary to implement these (they usually
-are direct queries on the container state). Can anyone think of a reason NOT
-to require these routines to be pure (in general or specifically)? [This is
-also OK.]
-
-(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. [Using prefix is OK, but only use it when necessary.]
-
-(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??
-[Both Bob and Tucker at various times have offered to help.]
-
-(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. [Don't worry about this.]
-
-]
-
-
!wording
[See the !discussion for general notes before reading this.]
@@ -181,6 +104,10 @@
Variable_Indexing => Reference,
Default_Iterator => Iterate,
Iterator_Element => Element_Type,
+ Aggregate => (Empty => Empty_Vector,
+ Add_Unnamed => Append_One,
+ New_Indexed => New_Vector,
+ Assign_Indexed => Replace_Element),
Stable_Properties => (Length, Capacity, Tampering_With_Cursors_Prohibited,
Tampering_With_Elements_Prohibited),
Default_Initial_Condition => Length(Vector) = 0 and then
@@ -204,6 +131,7 @@
[The rest of the package is as described in the detailed wording below. The
specs would match.]
+[Note: A.18.2(89.1/3) can be removed; it is covered by preconditions.]
Revised package Ada.Containers.Vectors, paragraphs A.18.2(97.2/3)
through A.18.2(237):
@@ -258,9 +186,29 @@
Returns True if tampering with elements is currently prohibited for Container,
and returns False otherwise.
+New
+function Maximum_Length return Count_Type;
+New
+Returns the maximum Length of a Vector, based on the index type.
+
+AARM Implementation Note: This is just
+ Count_Type (Index_Type'Last - Index_Type'First + 1)
+but since the inner calculation can overflow or the type conversion can fail,
+this can't be evaluated in general with an expression function. Note that if
+this expression raises Constraint_Error, then the result is Count_Type'Last,
+since the Capacity of a Vector cannot exceed Count_Type'Last.
+
+[Author's note: This definition is incompatible on the margins, as the
+preconditions defined below (on "&" and Insert) will raise Constraint_Error if
+the length of the container exceeds Count_Type'Last, while that would raise
+Capacity_Error in Ada 2005/2012. This seems exceedingly unlikely to actually
+happen, such that it isn't worth having two conditions to avoid changing the
+exception.]
+
100/2+
function To_Vector (Length : Count_Type) return Vector
- with Post => To_Vector'Result.Length = Length and then
+ with Pre => (if Length > Maximum_Length then raise Constraint_Error),
+ Post => To_Vector'Result.Length = Length and then
not Tampering_With_Elements_Prohibited (To_Vector'Result) and then
not Tampering_With_Cursors_Prohibited (To_Vector'Result) and then
To_Vector'Result.Capacity >= Length;
@@ -271,7 +219,8 @@
function To_Vector
(New_Item : Element_Type;
Length : Count_Type) return Vector
- with Post => Length (To_Vector'Result) = Length and then
+ with Pre => (if Length > Maximum_Length then raise Constraint_Error),
+ Post => Length (To_Vector'Result) = Length and then
not Tampering_With_Elements_Prohibited (To_Vector'Result) and then
not Tampering_With_Cursors_Prohibited (To_Vector'Result) and then
To_Vector'Result.Capacity >= Length;
@@ -281,10 +230,16 @@
104/2+
function "&" (Left, Right : Vector) return Vector
- with Post => Length (Vectors."&"'Result) = Length (Left) + Length (Right) and then
+ with Pre => (if Length (Left) + Length (Right) > Maximum_Length
+ then raise Constraint_Error),
+ Post => Length (Vectors."&"'Result) = Length (Left) + Length (Right) and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then
Vectors."&"'Result.Capacity >= Length (Left) + Length (Right);
+
+[Author's note: The precondition can overflow, but if that happens
+Constraint_Error would be raised just as we want anyway.]
+
105/2
Returns a vector comprising the elements of Left followed by the elements of
Right.
@@ -292,7 +247,9 @@
106/2+
function "&" (Left : Vector;
Right : Element_Type) return Vector
- with Post => Vectors."&"'Result.Length = Length (Left) + 1 and then
+ with Pre => (if Length (Left) + 1 > Maximum_Length
+ then raise Constraint_Error),
+ Post => Vectors."&"'Result.Length = Length (Left) + 1 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then
Vectors."&"'Result.Capacity >= Length (Left) + 1;
@@ -302,7 +259,9 @@
108/2+
function "&" (Left : Element_Type;
Right : Vector) return Vector
- with Post => Length (Vectors."&"'Result) = Length (Right) + 1 and then
+ with Pre => (if Length (Right) + 1 > Maximum_Length
+ then raise Constraint_Error),
+ Post => Length (Vectors."&"'Result) = Length (Right) + 1 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then
Vectors."&"'Result.Capacity >= Length (Right) + 1;
@@ -311,7 +270,8 @@
110/2+
function "&" (Left, Right : Element_Type) return Vector
- with Post => Length ("&"'Result) = 2 and then
+ with Pre => (if Maximum_Length < 2 then raise Constraint_Error),
+ Post => Length ("&"'Result) = 2 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then
Vectors."&"'Result.Capacity >= 2;
@@ -351,7 +311,8 @@
procedure Set_Length (Container : in out Vector;
Length : in Count_Type)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
- then raise Program_Error),
+ then raise Program_Error) and then
+ (if Length > Maximum_Length then raise Constraint_Error),
Post => Container.Length = Length and then
Capacity (Container) >= Length;
119/3
@@ -705,7 +666,7 @@
then raise Program_Error) and then
(if Before not in First_Index (Container) .. Last_Index (Container) + 1
then raise Constraint_Error) and then
- (if Length (Container) + Length (New_Item) > Index_Type'Last
+ (if Length (Container) + Length (New_Item) > Maximum_Length
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.]
@@ -731,7 +692,7 @@
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
+ (if Length (Container) + Length (New_Item) > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container),
Capacity (Container) >= Length (Container);
@@ -750,7 +711,9 @@
then raise Program_Error) and then
(if Before /= No_Element and then
(not Has_Element (Container, Before))
- then raise Program_Error),
+ then raise Program_Error) and then
+ (if Length (Container) + Length (New_Item) > Maximum_Length
+ then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Has_Element (Container, Position) and then
Capacity (Container) >= Length (Container);
@@ -768,7 +731,7 @@
then raise Program_Error) and then
(if Before not in First_Index (Container) .. Last_Index (Container) + 1
then raise Constraint_Error) and then
- (if Length (Container) + Count > Index_Type'Last
+ (if Length (Container) + Count > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -786,7 +749,7 @@
Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error) and then
- (if Length (Container) + Count > Index_Type'Last
+ (if Length (Container) + Count > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -803,7 +766,9 @@
then raise Program_Error) and then
(if Before /= No_Element and then
(not Has_Element (Container, Before))
- then raise Program_Error),
+ then raise Program_Error) and then
+ (if Length (Container) + Count > Maximum_Length
+ then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then
Capacity (Container) >= Length (Container);
@@ -818,7 +783,7 @@
then raise Program_Error) and then
(if Before not in First_Index (Container) .. Last_Index (Container) + 1
then raise Constraint_Error) and then
- (if Length (Container) + Count > Index_Type'Last
+ (if Length (Container) + Count > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -842,7 +807,7 @@
(if Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error) and
- (if Length (Container) + Count > Index_Type'Last
+ (if Length (Container) + Count > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then
@@ -857,7 +822,7 @@
New_Item : in Vector)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
- (if Length (Container) + Length (New_Item) > Index_Type'Last
+ (if Length (Container) + Length (New_Item) > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -870,7 +835,7 @@
Count : in Count_Type := 1)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
- (if Length (Container) + Count > Index_Type'Last
+ (if Length (Container) + Count > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -882,7 +847,7 @@
New_Item : in Vector)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
- (if Length (Container) + Length (New_Item) > Index_Type'Last
+ (if Length (Container) + Length (New_Item) > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -895,13 +860,26 @@
Count : in Count_Type := 1)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
- (if Length (Container) + Count > Index_Type'Last
+ (if Length (Container) + Count > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
175/2
Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item, Count).
+
+175.1/5
+procedure Append_One (Container : in out Vector;
+ New_Item : in Element_Type)
+ with Pre => (if Tampering_With_Cursors_Prohibited (Container)
+ then raise Program_Error) and then
+ (if Length (Container) + 1 > Maximum_Length
+ then raise Constraint_Error),
+ Post => Length (Container)'Old + 1 = Length (Container) and then
+ Capacity (Container) >= Length (Container);
+175.2/5
+Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item, 1).
+
176/2+
procedure Insert_Space (Container : in out Vector;
Before : in Extended_Index;
@@ -910,7 +888,7 @@
then raise Program_Error) and then
(if Before not in First_Index (Container) .. Last_Index (Container) + 1
then raise Constraint_Error),
- (if Length (Container) + Count > Index_Type'Last
+ (if Length (Container) + Count > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -932,8 +910,8 @@
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 Program_Error) and then
+ (if Length (Container) + Count > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then
@@ -950,6 +928,8 @@
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Index not in First_Index (Container) .. Last_Index (Container) + 1
+ then raise Constraint_Error) and then
+ (if Length (Container) + Count > Maximum_Length
then raise Constraint_Error),
Post => Length (Container)'Old - Count <= Length (Container);
182/3+
@@ -1036,7 +1016,10 @@
function First (Container : Vector) return Cursor
with Post => (if not Is_Empty (Container)
then Has_Element (Container, First'Result)
- else First'Result = No_Element);
+ else First'Result = No_Element),
+ Global => null,
+ Nonblocking => True;
+
198/2
If Container is empty, First returns No_Element. Otherwise, it returns a cursor
that designates the first element in Container.
@@ -1061,7 +1044,9 @@
function Last (Container : Vector) return Cursor;
with Post => (if not Is_Empty (Container)
then Has_Element (Container, Last'Result)
- else Last'Result = No_Element);
+ else Last'Result = No_Element),
+ Global => null,
+ Nonblocking => True;
204/2
If Container is empty, Last returns No_Element. Otherwise, it returns a cursor
that designates the last element in Container.
@@ -1396,10 +1381,10 @@
* For procedures Insert, Insert_Space, Prepend, and Append, the part of the
precondition reading:
- (if <some length expression> > Index_Type'Last
+ (if <some length expression> > Maximum_Length
then raise Constraint_Error)
is replaced by:
- (if <some length expression> > Index_Type'Last
+ (if <some length expression> > Maximum_Length
then raise Constraint_Error) and then
(if <some length expression> > Container.Capacity
then raise Capacity_Error)
@@ -1419,8 +1404,7 @@
Nonblocking => Equal_Element'Nonblocking,
Global => Equal_Element'Global &
Element_Type'Global &
- in out synchronized Ada.Containers.Indefinite_Holders &
- in out synchronized <<some impl-defed helper packages>> is
+ in out synchronized Ada.Containers.Indefinite_Holders is
6/3+
type Holder is tagged private
@@ -1585,7 +1569,7 @@
-----------------------------------------
-Added after 11.4.2(23.5/5):
+Add after 11.4.2(23.5/5):
Any precondition expression occurring in the specification of a
language-defined unit is enabled (see 6.1.1) unless suppressed (see 11.5).
@@ -1595,15 +1579,15 @@
AARM Reason: This allows the Standard to express runtime requirements on the
client of a language-defined unit as preconditions or predicates (which are
invariably clearer than English prose would be). Some such requirements can be
-Suppressed. Previous versions of Ada did not provide a mechanism to suppress
+Suppressed. Ada 2012 and before did not provide a mechanism to suppress
such code.
Add after 11.5(23):
Redundant[The following check corresponds to situations in which the exception
-Assertion_Error is raised upon failure.]
+Assertion_Error is raised upon failure of a language-defined check.]
-Container_Check
+Containers_Assertion_Check
Check the precondition of a routine declared in a descendant unit of Containers
or in an instance of a generic unit that is declared in, or is, a
@@ -1745,6 +1729,9 @@
be listed), and so on. This provides a bit more granularity (although that
only matters if we define many more routines with preconditions).
+Note: This topic is now split out into AI12-0311-1 so we can define this
+consistently for the entire set of language-defined units.
+
---
AI12-0189-1 defines procedural iterators and the Allows_Exit aspect to be
@@ -1760,6 +1747,75 @@
hopefully the new aspect will trigger implementers to inspect their
implementations for issues.
+---
+
+For the pre- and postconditions, we used Pre and Post rather than Pre'Class
+and Post'Class, since these mostly belong to the specific routine rather than
+any routine matching the profile. This way, they can be eliminated for a
+derived type if desired. (The usual rules mean that any delegation to the
+original routine will check the original Pre/Post.) This does mean that they
+won't necessarily follow LSP for a dispatching call, but that seems
+unnecessary for the containers (extensions seem unusual, and using multiple
+versions of a single container simultaenously more so). By using Pre, an
+implementation can generate the precondition as part of the subprogram body
+if it wishes (or it can generate it at the call
+site to support optimization and suppressibility).
+
+---
+
+We override the usual Nonblocking and Global status for the various
+predicate routines, to essentially mark these as Pure. If Nonblocking => True
+is used, this would prevent calling the formal subprograms in the associated
+routines. But that shouldn't be necessary to implement these (they usually
+are direct queries on the container state).
+
+Similarly, we require the container navigation routines to be "pure" in this
+sense; no access to the formal subprograms or elements is needed to move
+around in a container.
+
+---
+
+The global setting "Access subtype_mark" says that it applies to all of
+the "(aliased)" objects of subtype_mark. For a tagged type (like Vector), it
+needs to apply to all objects of the type, since 'Access can be used inside
+of the package, and has to for the containers packages in order to create the
+needed cursor semantics.
+
+---
+
+We use prefixed notation in some pre- and postconditions, as the function that
+needs to be called has the same name as a parameter of the routine (see
+To_Vector and Reserve_Capacity for examples). The direct name is hidden in
+that case, so prefixed notation seems like the best way to call the function.
+In other cases, we have used conventional notation for subprogram calls.
+
+---
+
+Note that we duplicate contracts in the complete specification and in the
+individual descriptions of entities. This simplifies reading of the contracts
+-- constantly looking at the full specification is not needed. This seems
+important for routines that have part of their semantics defined by contracts,
+and is done for all routines for consistency.
+
+---
+
+Not everything can be handled with the existing contracts.
+
+For instance, we can't provide a precondition for anonymous
+access-to-subprogram parameters. Thus we can't specify in the contract that
+Tampering_With_Cursors_Prohibited is True for
+Query_Element/Update_Element/subprogram iterators.
+
+It also would be nice to be able to indicate that
+Tampering_With_Cursors_Prohibited is True during the lifetime of an iterator
+or reference object. This doesn't correspond to any of the "traditional"
+contracts.
+
+The lack of these specifications is not critical. It just prevents tools and
+compilers from detecting failing tampering checks (and optimizing away
+unnecessary checks) based on these properties alone.
+
+
!corrigendum 11.4.2(23.1/3)
@dinsa
@@ -1785,8 +1841,8 @@
or subprogram has not been exceeded.>
@dinss
@xbullet<The following check corresponds to situations in which the exception
-Assertion_Error is raised upon failure.>
-@xhang<@xterm<Container_Check>
+Assertion_Error is raised upon failure of a language-defined check.>
+@xhang<@xterm<Containers_Assertion_Check>
Check the precondition of a routine declared in a descendant unit of Containers
or in an instance of a generic unit that is declared in, or is, a
descendant unit of Containers.>
@@ -1813,6 +1869,28 @@
implementation-defined packages to the global specification (see 6.1.2) for
any language-defined entity that is not declared pure or has a global
specification of @b<null>.
+
+
+!corrigendum A.18(11/5)
+
+@dinsa
+For an indefinite container (one whose type is defined in an instance of a
+child package of Containers whose @fa<defining_identifier> contains "Indefinite"),
+each element of the container shall be created when it is inserted into the
+container and finalized when it is deleted from the container (or when the
+container object is finalized if the element has not been deleted). For a
+bounded container (one whose type is defined in an instance of a child
+package of Containers whose @fa<defining_identifier> starts with "Bounded") that
+is not an indefinite container, all of the elements of the capacity of the
+container shall be created and default initialized when the container object
+is created; the elements shall be finalized when the container object is
+finalized. For other kinds of containers, when elements are created
+and finalized is unspecified.
+@dinst
+If an instance of an Ada.Containers generic package is nonblocking, then the
+specific type of the object returned from a function that returns an object
+of an iterator interface, as well as the primitive operations of that specific
+type, shall be nonblocking.
!ASIS
Questions? Ask the ACAA Technical Agent