CVS difference for ai12s/ai12-0112-1.txt
--- ai12s/ai12-0112-1.txt 2019/02/14 05:25:23 1.14
+++ ai12s/ai12-0112-1.txt 2019/02/21 05:29:33 1.15
@@ -110,9 +110,9 @@
Assign_Indexed => Replace_Element),
Stable_Properties => (Length, Capacity, Tampering_With_Cursors_Prohibited,
Tampering_With_Elements_Prohibited),
- Default_Initial_Condition => Length(Vector) = 0 and then
- (not Tampering_With_Cursors_Prohibited(Vector)) and then
- (not Tampering_With_Elements_Prohibited(Vector));
+ 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;
@@ -169,7 +169,8 @@
raised during evaluation of element equality is propagated.
New
-function Tampering_With_Cursors_Prohibited (Container : Vector) return Boolean
+function Tampering_With_Cursors_Prohibited
+ (Container : Vector) return Boolean
with Nonblocking => True,
Global => null;
New
@@ -179,7 +180,8 @@
cursors, so we have this function reflect that.
New
-function Tampering_With_Elements_Prohibited (Container : Vector) return Boolean
+function Tampering_With_Elements_Prohibited
+ (Container : Vector) return Boolean
with Nonblocking => True,
Global => null;
New
@@ -187,7 +189,9 @@
and returns False otherwise.
New
-function Maximum_Length return Count_Type;
+function Maximum_Length return Count_Type
+ with Nonblocking => True,
+ Global => null;
New
Returns the maximum Length of a Vector, based on the index type.
@@ -202,8 +206,9 @@
preconditions defined below (on "&" and Insert) will raise Constraint_Error if
the length of the container exceeds Count_Type'Last, while that would raise
Capacity_Error in Ada 2005/2012. This seems exceedingly unlikely to actually
-happen, such that it isn't worth having two conditions to avoid changing the
-exception.]
+happen, as Count_Type'Last is likely to be 2**31-1, and such a vector probably
+would overflow memory long before this problem occurred. As such, it isn't
+worth having two conditions to avoid changing the exception.]
100/2+
function To_Vector (Length : Count_Type) return Vector
@@ -230,16 +235,13 @@
104/2+
function "&" (Left, Right : Vector) return Vector
- with Pre => (if Length (Left) + Length (Right) > Maximum_Length
+ with Pre => (if Length (Left) > Maximum_Length - Length (Right)
then raise Constraint_Error),
Post => Length (Vectors."&"'Result) = Length (Left) + Length (Right) and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
not Tampering_With_Cursors_Prohibited (Vectors."&"'Result) and then
Vectors."&"'Result.Capacity >= Length (Left) + Length (Right);
-[Author's note: The precondition can overflow, but if that happens
-Constraint_Error would be raised just as we want anyway.]
-
105/2
Returns a vector comprising the elements of Left followed by the elements of
Right.
@@ -247,7 +249,7 @@
106/2+
function "&" (Left : Vector;
Right : Element_Type) return Vector
- with Pre => (if Length (Left) + 1 > Maximum_Length
+ with Pre => (if Length (Left) > Maximum_Length - 1
then raise Constraint_Error),
Post => Vectors."&"'Result.Length = Length (Left) + 1 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
@@ -259,7 +261,7 @@
108/2+
function "&" (Left : Element_Type;
Right : Vector) return Vector
- with Pre => (if Length (Right) + 1 > Maximum_Length
+ with Pre => (if Length (Right) > Maximum_Length - 1
then raise Constraint_Error),
Post => Length (Vectors."&"'Result) = Length (Right) + 1 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then
@@ -529,10 +531,12 @@
type Constant_Reference_Type
(Element : not null access constant Element_Type) is private
with Implicit_Dereference => Element,
+ Global => in out access Vector,
Default_Initial_Condition => (raise Program_Error);
147.2/3
type Reference_Type (Element : not null access Element_Type) is private
with Implicit_Dereference => Element,
+ Global => in out access Vector,
Default_Initial_Condition => (raise Program_Error);
147.3/3
The types Constant_Reference_Type and Reference_Type need finalization.
@@ -543,9 +547,15 @@
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),
+ with Pre => (if Index not in First_Index (Container) .. Last_Index (Container)
+ then raise Constraint_Error),
+ Post => Tampering_With_Cursors_Prohibited (Container),
Global => null;
+
+[Author's note: We have to use Tampering_With_Cursors_Prohibited here, as
+Tampering_With_Elements_Prohibited is always False. We'll use the right function in
+the indefinite containers.]
+
147.6/3
This function (combined with the Constant_Indexing and Implicit_Dereference
aspects) provides a convenient way to gain read access to an individual element
@@ -560,8 +570,10 @@
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);
+ with Pre => (if Index not in First_Index (Container) .. Last_Index (Container)
+ then raise Constraint_Error),
+ Post => Tampering_With_Cursors_Prohibited (Container),
+ Global => null;
147.9/3
This function (combined with the Variable_Indexing and Implicit_Dereference
aspects) provides a convenient way to gain read and write access to an
@@ -579,9 +591,10 @@
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),
+ with Pre => (if Position = No_Element then raise Constraint_Error) and then
+ (if not Has_Element (Container, Position)
+ then raise Program_Error),
+ Post => Tampering_With_Cursors_Prohibited (Container),
Global => null;
147.13/3
This function (combined with the Constant_Indexing and Implicit_Dereference
@@ -597,9 +610,11 @@
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);
+ with Pre => (if Position = No_Element then raise Constraint_Error) and then
+ (if not Has_Element (Container, Position)
+ then raise Program_Error);
+ Post => Tampering_With_Cursors_Prohibited (Container),
+ Global => null;
147.16/3
This function (combined with the Variable_Indexing and Implicit_Dereference
aspects) provides a convenient way to gain read and write access to an
@@ -616,7 +631,7 @@
147.19/3+
procedure Assign (Target : in out Vector; Source : in Vector)
with Pre => (if Tampering_With_Cursors_Prohibited (Target)
- then raise Program_Error),
+ then raise Program_Error),
Post => Length (Source) = Length (Target),
Capacity (Target) >= Length (Target);
147.20/3
@@ -666,7 +681,7 @@
then raise Program_Error) and then
(if Before not in First_Index (Container) .. Last_Index (Container) + 1
then raise Constraint_Error) and then
- (if Length (Container) + Length (New_Item) > Maximum_Length
+ (if Length (Container) > Maximum_Length - Length (New_Item)
then raise Constraint_Error),
[Note: This length calculation might overflow, but if it does, that's OK, as the rules
require Constraint_Error to be raised in this case.]
@@ -692,7 +707,7 @@
Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error) and then
- (if Length (Container) + Length (New_Item) > Maximum_Length
+ (if Length (Container) > Maximum_Length - Length (New_Item)
then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container),
Capacity (Container) >= Length (Container);
@@ -712,7 +727,7 @@
(if Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error) and then
- (if Length (Container) + Length (New_Item) > Maximum_Length
+ (if Length (Container) > Maximum_Length - Length (New_Item)
then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Has_Element (Container, Position) and then
@@ -731,7 +746,7 @@
then raise Program_Error) and then
(if Before not in First_Index (Container) .. Last_Index (Container) + 1
then raise Constraint_Error) and then
- (if Length (Container) + Count > Maximum_Length
+ (if Length (Container) > Maximum_Length - Count
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -749,7 +764,7 @@
Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error) and then
- (if Length (Container) + Count > Maximum_Length
+ (if Length (Container) > Maximum_Length - Count
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -767,7 +782,7 @@
(if Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error) and then
- (if Length (Container) + Count > Maximum_Length
+ (if Length (Container) > Maximum_Length - Count
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then
@@ -783,7 +798,7 @@
then raise Program_Error) and then
(if Before not in First_Index (Container) .. Last_Index (Container) + 1
then raise Constraint_Error) and then
- (if Length (Container) + Count > Maximum_Length
+ (if Length (Container) > Maximum_Length - Count
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -807,7 +822,7 @@
(if Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error) and
- (if Length (Container) + Count > Maximum_Length
+ (if Length (Container) > Maximum_Length - Count
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then
@@ -822,7 +837,7 @@
New_Item : in Vector)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
- (if Length (Container) + Length (New_Item) > Maximum_Length
+ (if Length (Container) > Maximum_Length - Length (New_Item)
then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -835,7 +850,7 @@
Count : in Count_Type := 1)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
- (if Length (Container) + Count > Maximum_Length
+ (if Length (Container) > Maximum_Length - Count
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -847,7 +862,7 @@
New_Item : in Vector)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
- (if Length (Container) + Length (New_Item) > Maximum_Length
+ (if Length (Container) > Maximum_Length - Length (New_Item)
then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -860,7 +875,7 @@
Count : in Count_Type := 1)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
- (if Length (Container) + Count > Maximum_Length
+ (if Length (Container) > Maximum_Length - Count
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -873,7 +888,7 @@
New_Item : in Element_Type)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
- (if Length (Container) + 1 > Maximum_Length
+ (if Length (Container) > Maximum_Length - 1
then raise Constraint_Error),
Post => Length (Container)'Old + 1 = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -888,7 +903,7 @@
then raise Program_Error) and then
(if Before not in First_Index (Container) .. Last_Index (Container) + 1
then raise Constraint_Error),
- (if Length (Container) + Count > Maximum_Length
+ (if Length (Container) > Maximum_Length - Count
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
@@ -911,7 +926,7 @@
(if Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error) and then
- (if Length (Container) + Count > Maximum_Length
+ (if Length (Container) > Maximum_Length - Count
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then
@@ -1244,7 +1259,9 @@
230.1/3
function Iterate (Container : in Vector)
- return Vector_Iterator_Interfaces.Reversible_Iterator'Class;
+ return Vector_Iterator_Interfaces.Reversible_Iterator'Class
+ with Post => Tampering_With_Cursors_Prohibited (Container);
+
230.2/3
Iterate returns a reversible iterator object (see 5.5.1) that will generate a
value for a loop parameter (see 5.5.2) designating each node in Container,
@@ -1259,8 +1276,9 @@
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);
+ with Pre => (if Start = No_Element then raise Constraint_Error) and then
+ (if not Has_Element (Start, Position) then raise Program_Error),
+ Post => Tampering_With_Cursors_Prohibited (Container);
230.4/3+
Iterate returns a reversible iterator object (see 5.5.1)
that will generate a value for a loop parameter (see 5.5.2) designating each
@@ -1289,10 +1307,9 @@
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.]
+ with Pre => (if Tampering_With_Elements_Prohibited (Container)
+ then raise Program_Error);
+[Checking whether these are sorted is too expensive, so we won't try.]
235/2
Reorders the elements of Container such that the elements are sorted smallest
first as determined by the generic formal "<" operator provided. Any exception
@@ -1301,16 +1318,18 @@
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;
+ with Pre => (if Tampering_With_Elements_Prohibited (Target)
+ then raise Program_Error) and then
+ (if Tampering_With_Elements_Prohibited (Source)
+ then raise Program_Error) and then
+ (if Length (Target) > Maximum_Length - Length (Source)
+ then raise Constraint_Error),
+ Post => (if Target = Source then True
+ else Length (Source) = 0 and then
+ Length (Target) =
+ Length (Source)'Old + Length (Target)'Old and then
+ Capacity (Target) >=
+ Length (Source)'Old + Length (Target)'Old;
[Checking whether these are sorted is too expensive, so we won't try;
especially as we don't specify what happens if they're not.]
237/3
@@ -1327,10 +1346,12 @@
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.]
+Add after A.18.11(9/4):
+Tampering_With_Cursors_Prohibited is replaced by
+Tampering_With_Elements_Prohibited in the postcondition for the operations
+Reference and Constant_Reference.
+
-----------------------------------------
A.18.19 The Generic Package Containers.Bounded_Vectors
@@ -1410,7 +1431,6 @@
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;
@@ -1439,14 +1459,14 @@
38/3+
function To_Holder (New_Item : Element_Type) return Holder
- with Post => not Is_Empty (To_Holder'Result);
+ 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;
+ with Global => null;
41/3
Returns True if Container is empty, and False if it contains an element.
@@ -1503,10 +1523,12 @@
type Constant_Reference_Type
(Element : not null access constant Element_Type) is private
with Implicit_Dereference => Element,
+ Global => in out access Holder,
Default_Initial_Condition => (raise Program_Error);
53/3+
type Reference_Type (Element : not null access Element_Type) is private
with Implicit_Dereference => Element,
+ Global => in out access Holder,
Default_Initial_Condition => (raise Program_Error);
54/3
The types Constant_Reference_Type and Reference_Type need finalization.
@@ -1516,27 +1538,31 @@
56/3+
function Constant_Reference (Container : aliased in Holder)
return Constant_Reference_Type
- with Pre => (if Is_Empty (Container) then raise Constraint_Error);
+ with Pre => (if Is_Empty (Container) then raise Constraint_Error),
+ Post => Tampering_With_The_Element_Prohibited (Container),
+ Global => null;
57/3
This function (combined with the Implicit_Dereference aspect) provides a
convenient way to gain read access to the contained element of a holder
container.
58/3+
Constant_Reference returns an object whose discriminant is an access value
- that designates the contained element. Tampering with the elements of
+ that designates the contained element. Tampering with the element of
Container is prohibited while the object returned by Constant_Reference
exists and has not been finalized.
59/3+
function Reference (Container : aliased in out Holder) return Reference_Type
- with Pre => (if Is_Empty (Container) then raise Constraint_Error);
+ with Pre => (if Is_Empty (Container) then raise Constraint_Error),
+ Post => Tampering_With_The_Element_Prohibited (Container),
+ Global => null;
60/3
This function (combined with the Implicit_Dereference aspects) provides
a convenient way to gain read and write access to the contained element
of a holder container.
61/3+
Reference returns an object whose discriminant is an access value that
- designates the contained element. Tampering with the elements of Container
+ designates the contained element. Tampering with the element of Container
is prohibited while the object returned by Reference exists and has not
been finalized.
@@ -1891,6 +1917,98 @@
specific type of the object returned from a function that returns an object
of an iterator interface, as well as the primitive operations of that specific
type, shall be nonblocking.
+
+!comment For the actual container's definitions (A.18.2-A.18.36), we only
+!comment provide Corrigendum sections for those that conflict with other
+!comment AI changes.
+
+!corrigendum A.18.2(8/3)
+
+@drepl
+@xcode< @b<type> Vector @b<is tagged private>
+ @b<with> Constant_Indexing =@> Constant_Reference,
+ Variable_Indexing =@> Reference,
+ Default_Iterator =@> Iterate,
+ Iterator_Element =@> Element_Type;
+ @b<pragma> Preelaborable_Initialization(Vector);>
+@dby
+See the conflict file!!
+
+
+!corrigendum A.18.3(6/3)
+
+@drepl
+@xcode< @b<type> List @b<is tagged private>
+ @b<with> Constant_Indexing =@> Constant_Reference,
+ Variable_Indexing =@> Reference,
+ Default_Iterator =@> Iterate,
+ Iterator_Element =@> Element_Type;
+ @b<pragma> Preelaborable_Initialization(List);>
+@dby
+See the conflict file!!
+
+
+!corrigendum A.18.5(3/2)
+
+@drepl
+@xcode< @b<type> Map @b<is tagged private>
+ @b<with> Constant_Indexing =@> Constant_Reference,
+ Variable_Indexing =@> Reference,
+ Default_Iterator =@> Iterate,
+ Iterator_Element =@> Element_Type;
+ @b<pragma> Preelaborable_Initialization(Map);>
+@dby
+See the conflict file!!
+
+
+!corrigendum A.18.6(4/3)
+
+@drepl
+@xcode< @b<type> Map @b<is tagged private>
+ @b<with> Constant_Indexing =@> Constant_Reference,
+ Variable_Indexing =@> Reference,
+ Default_Iterator =@> Iterate,
+ Iterator_Element =@> Element_Type;
+ @b<pragma> Preelaborable_Initialization(Map);>
+@dby
+See the conflict file!!
+
+
+!corrigendum A.18.8(3/3)
+
+@drepl
+@xcode< @b<type> Set @b<is tagged private>
+ @b<with> Constant_Indexing =@> Constant_Reference,
+ Default_Iterator =@> Iterate,
+ Iterator_Element =@> Element_Type;
+ @b<pragma> Preelaborable_Initialization(Set);>
+@dby
+See the conflict file!!
+
+
+!corrigendum A.18.9(4/3)
+
+@drepl
+@xcode< @b<type> Set @b<is tagged private>
+ @b<with> Constant_Indexing =@> Constant_Reference,
+ Default_Iterator =@> Iterate,
+ Iterator_Element =@> Element_Type;
+ @b<pragma> Preelaborable_Initialization(Set);>
+@dby
+See the conflict file!!
+
+
+!corrigendum A.18.10(8/3)
+
+@drepl
+@xcode< @b<type> Tree @b<is tagged private>
+ @b<with> Constant_Indexing =@> Constant_Reference,
+ Variable_Indexing =@> Reference,
+ Default_Iterator =@> Iterate,
+ Iterator_Element =@> Element_Type;
+ @b<pragma> Preelaborable_Initialization(Tree);>
+@dby
+See the conflict file!!
!ASIS
Questions? Ask the ACAA Technical Agent