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