AI22-0104-1

!standard A.18.2(53/5)                                    24-08-02  AI22-0104-1/04

!standard A.18.2(188/3)

!standard A.18.19(9.1/5)

!standard A.18.19(9.2/5)

!class Amendment 24-04-22

!status Amendment 1-2022  24-07-18

!status WG9 Approved 24-10-10

!status ARG Approved  8-0-0  24-07-18

!status work item 24-04-22

!status received 24-01-13

!submitter Pascal Pignard

!priority Low

!difficulty Easy

!subject Slicing of Vectors

!summary

Slice and Replace_Slice subprograms are added to the Vectors generic package.

!issue

Given a vector based on the Ada.Containers.Vectors generic package, it is natural to want to select or to update a slice of the vector.

Should operations to deal with slices of vectors be added to Ada.Containers.Vector? (Yes.)

!recommendation

The following subprograms should be added to Ada.Containers.Vector:

function Slice
  (Container : Vector;
   Low       : Index_Type;
   High      : Extended_Index) return Vector;
procedure Slice
  (Container : in out Vector;
   Low       : in     Index_Type;
   High      : in     Extended_Index);
function Replace_Slice
  (Container : Vector;
   Low       : Index_Type;
   High      : Extended_Index;
   By        : Vector) return Vector;
procedure Replace_Slice
  (Container : in out Vector;
   Low       : in Index_Type;
   High      : in Extended_Index;
   By        : in Vector);

!wording

Add after A.18.2(53/5):

function Slice (Container : Vector;
                Low       : Index_Type;
                High      : Extended_Index) return Vector
   with Pre  => High in Low - 1 .. Container.Last_Index
                   or else raise Constraint_Error,
        Post => Slice'Result.Length = High - Low + 1 and then
               not Tampering_With_Elements_Prohibited (Slice'Result)
                   and then
                not Tampering_With_Cursors_Prohibited (Slice'Result)
                   and then
               Slice'Result.Capacity >= Slice'Result.Length;

procedure Slice (Container : in out Vector;
                 Low       : in     Index_Type;
                 High      : in     Extended_Index)
   with Pre  => (not Tampering_With_Elements_Prohibited (Container)
                   or else raise Program_Error) and then
               (High in Low - 1 .. Container.Last_Index
                   or else raise Constraint_Error),
        Post => Container.Length = High - Low + 1 and then
               Container.Capacity >= Container.Length;

function Replace_Slice (Container : Vector;
                        Low       : Index_Type;
                        High      : Extended_Index;
                        By        : Vector) return Vector
   with Pre => (High in Low - 1 .. Container.Last_Index
                  or else raise Constraint_Error) and then
              (Container.Length - Count_Type (High - Low + 1) <=
                   Maximum_Length - By.Length
                   or else raise Constraint_Error),
        Post => Replace_Slice'Result.Length = Container.Length -
                   Count_Type (High - Low + 1) + By.Length and then

                not Tampering_With_Elements_Prohibited
                   (Replace_Slice'Result) and then
               not Tampering_With_Cursors_Prohibited
                   (Replace_Slice'Result) and then
               Replace_Slice'Result.Capacity >=
                   Replace_Slice.Length;

procedure Replace_Slice (Container : in out Vector;
                         Low       : in     Index_Type;
                         High      : in     Extended_Index;
                         By        : in     Vector)
   with Pre  => (not Tampering_With_Elements_Prohibited (Container)
                   or else raise Program_Error) and then
               (High in Low - 1 .. Container.Last_Index
                   or else raise Constraint_Error) and then
               (Container.Length - Count_Type (High - Low + 1) <=
                   Maximum_Length - By.Length
                   or else raise Constraint_Error),
        Post => Container.Length =
                   Container.Length'Old -
                   Count_Type (High - Low + 1) + By.Length and then
               Container.Capacity >= Container.Length;

Add after A.18.2(188/3):

function Slice (Container : Vector;
                Low       : Index_Type;
                High      : Extended_Index) return Vector
   with Pre  =>High in Low - 1 .. Container.Last_Index
                  or else raise Constraint_Error,
        Post => Slice'Result.Length = High - Low + 1 and then
               not Tampering_With_Elements_Prohibited (Slice'Result)
                   and then
               not Tampering_With_Cursors_Prohibited (Slice'Result)
                   and then
               Slice'Result.Capacity >= Slice'Result.Length;

 

This returns a slice of Container from Low to High.  If High = Low - 1, then the result is an empty vector.

procedure Slice (Container : in out Vector;
                 Low       : in     Index_Type;
                 High      : in     Extended_Index)
   with Pre  => (not Tampering_With_Elements_Prohibited (Container)
                   or else raise Program_Error) and then
               (High in Low - 1 .. Container.Last_Index
                   or else raise Constraint_Error),
        Post => Container.Length = High - Low + 1 and then
               Container.Capacity >= Container.Length;

 

Equivalent to Container := Slice (Container, Low, High);

function Replace_Slice (Container : Vector;
                        Low       : Index_Type;
                        High      : Extended_Index;
                        By        : Vector) return Vector

   with Pre  => (High in Low - 1 .. Container.Last_Index
                   or else raise Constraint_Error) and then
               (Container.Length - Count_Type (High - Low + 1) <=
                   Maximum_Length - By.Length
                   or else raise Constraint_Error),
        Post => Replace_Slice'Result.Length = Container.Length -
                   Count_Type (High - Low + 1) + By.Length and then
               not Tampering_With_Elements_Prohibited
                   (Replace_Slice'Result) and then
               not Tampering_With_Cursors_Prohibited
                   (Replace_Slice'Result) and then
               Replace_Slice'Result.Capacity >=
                    Replace_Slice'Result.Length;

 

This returns a copy of Container with the slice of elements from Low to High replaced with the vector By.

procedure Replace_Slice (Container : in out Vector;
                         Low       : in     Index_Type;
                         High      : in     Extended_Index;
                         By        : in     Vector)
   with Pre  => (not Tampering_With_Elements_Prohibited (Container)
                   or else raise Program_Error) and then
               (High in Low - 1 .. Container.Last_Index
                   or else raise Constraint_Error), and then
               (Container.Length - Count_Type (High - Low + 1) <=
                   Maximum_Length - By.Length
                   or else raise Constraint_Error),
        Post => Container.Length =
                   Container.Length'Old -
                   Count_Type (High - Low + 1) + By.Length and then
                Container.Capacity >= Container.Length;

 

Equivalent to Container := Replace_Slice (Container, Low, High, By);

If High = Low - 1, then this is equivalent to Insert_Vector (Container, Low, By);

Modify A.18.19(9.1/5):

The portion of the postcondition checking the capacity is omitted from subprograms Set_Length, Assign, Insert, Insert_Space, {Slice, Replace_Slice}, Prepend, Append, and Delete.

Modify A.18.19(9.2/5):

For procedures Insert, Insert_Space, {Replace_Slice}, Prepend, and Append, the part of the precondition reading:

!discussion

These operations were proposed in ARG GitHub issue #75. They correspond to similar operations in the package Ada.Strings.Unbounded (see A.4.5 in the RM).

We have not allowed arbitrary values for High when it is less than Low, but rather require it to be Low - 1 when specifying a null slice. This could be changed, but it adds complexity to the postcondition for no clear benefit. Similarly, we have not allowed arbitrary values for Low when it is greater than High, but require it to be no more than Container.Last_Index + 1 (because of the precondition which specifies that if Low were greater than Container.Last_Index + 1 there would be no allowed value for High).

These new operations are also included in the Indefinite_Vectors and Bounded_Vectors generic packages. The new operations added to Indefinite_Vectors do not perform indefinite insertion, because none of the parameters are of the Element_Type. The new Replace_Slice procedure added to Bounded_Vectors has its precondition and postcondition adjusted in the same way as Insert and other operations that might increase the number of elements in the Container.

Note: We should consider replacing all of the <vec>.Capacity >= <vec>.Length postconditions with a Type_Invariant (or a Type_Invariant'Class? Or a Stable_Property?).[a][b]

!example

Examples of use of Slice and Replace_Slice:

procedure Example is
   package Float_Vectors is new Containers.Vectors (Float, Positive);
   use Float_Vectors;

   FV : Float_Vector := [1.1, 2.2, 3.3, 4.4];
   FV_Slice : constant Float_Vector := FV.Slice (2, 3);
   pragma Assert (FV_Slice = [2.2, 3.3]);

   New_FV : constant Float_Vector :=
     FV_Slice.Replace_Slice (1, 0, By => [7.7, 8.8]);
   pragma Assert (New_FV = [7.7, 8.8, 2.2, 3.3]);
begin
   Replace_Slice (FV, 2, 3, By => [4.2]);
   pragma Assert (FV.Length = 3);
   pragma Assert (FV = [1.1, 4.2, 4.4]);
end Example;

!corrigendum A.18.2(53/5)

@dinsa

@xcode{   @b{procedure} Delete_Last (Container : @b{in out} Vector;

                          Count     : @b{in}     Count_Type := 1)

      @b{with} Pre  => @b{not} Tampering_With_Cursors_Prohibited (Container)

                       @b{or else raise} Program_Error,

           Post => Length (Container)'Old - Count <= Length (Container);}

@dinss

@xcode{   @b{function} Slice (Container : Vector;

                   Low       : Index_Type;

                   High      : Extended_Index) @b{return} Vector

      @b{with} Pre  => High @b{in} Low - 1 .. Container.Last_Index

                      @b{or else raise} Constraint_Error,

           Post => Slice'Result.Length = High - Low + 1 @b{and then}

                   @b{not} Tampering_With_Elements_Prohibited (Slice'Result)

                      @b{and then}

                   @b{not} Tampering_With_Cursors_Prohibited (Slice'Result)

                      @b{and then}

                   Slice'Result.Capacity >= Slice'Result.Length;}

@xcode{   @b{procedure} Slice (Container : @b{in out} Vector;

                    Low       : @b{in}     Index_Type;

                    High      : @b{in}     Extended_Index)

      @b{with} Pre  => (@b{not} Tampering_With_Elements_Prohibited (Container)

                      @b{or else raise} Program_Error) @b{and then}

                   (High @b{in} Low - 1 .. Container.Last_Index

                      @b{or else raise} Constraint_Error),

           Post => Container.Length = High - Low + 1 @b{and then}
                  Container.Capacity >= Container.Length;}

@xcode{   @b{function} Replace_Slice (Container : Vector;

                           Low       : Index_Type;

                           High      : Extended_Index;

                           By        : Vector) @b{return} Vector

      @b{with} Pre  => (High @b{in} Low - 1 .. Container.Last_Index

                      @b{or else raise} Constraint_Error) @b{and then}

                   (Container.Length - Count_Type (High - Low + 1) <=

                      Maximum_Length - By.Length

                      @b{or else raise} Constraint_Error),

           Post => Replace_Slice'Result.Length = Container.Length -

                      Count_Type (High - Low + 1) + By.Length @b{and then}

                   @b{not} Tampering_With_Elements_Prohibited

                      (Replace_Slice'Result) @b{and then}

                   @b{not} Tampering_With_Cursors_Prohibited

                      (Replace_Slice'Result) @b{and then}

                   Replace_Slice'Result.Capacity >= Replace_Slice.Length;}

@xcode{   @b{procedure} Replace_Slice (Container : @b{in out} Vector;

                            Low       : @b{in}     Index_Type;

                            High      : @b{in}     Extended_Index;

                            By        : @b{in}     Vector)

      @b{with} Pre  => (@b{not} Tampering_With_Elements_Prohibited (Container)

                      @b{or else raise} Program_Error) @b{and then}

                   (High @b{in} Low - 1 .. Container.Last_Index

                      @b{or else raise} Constraint_Error) @b{and then}

                   (Container.Length - Count_Type (High - Low + 1) <=

                      Maximum_Length - By.Length

                      @b{or else raise} Constraint_Error),

           Post => Container.Length = Container.Length'Old -

                      Count_Type (High - Low + 1) + By.Length @b{and then}

                   Container.Capacity >= Container.Length;}

!corrigendum A.18.2(188/3)

@dinsa

@xindent{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).}

@dinss

@xcode{@b{function} Slice (Container : Vector;

                Low       : Index_Type;

                High      : Extended_Index) @b{return} Vector

   @b{with} Pre  => High @b{in} Low - 1 .. Container.Last_Index

                   @b{or else raise} Constraint_Error,

        Post => Slice'Result.Length = High - Low + 1 @b{and then}

                @b{not} Tampering_With_Elements_Prohibited (Slice'Result)

                   @b{and then}

                @b{not} Tampering_With_Cursors_Prohibited (Slice'Result)

                   @b{and then}

                Slice'Result.Capacity >= Slice'Result.Length;}

@xindent{This returns a slice of Container from Low to High.  If High = Low - 1, then the result is an empty vector.}

@xcode{@b{procedure} Slice (Container : @b{in out} Vector;

                 Low       : @b{in}     Index_Type;

                 High      : @b{in}     Extended_Index)

   @b{with} Pre  => (@b{not} Tampering_With_Elements_Prohibited (Container)

                   @b{or else raise} Program_Error) @b{and then}

                (High @b{in} Low - 1 .. Container.Last_Index

                   @b{or else raise} Constraint_Error),

        Post => Container.Length = High - Low + 1 @b{and then}
               Container.Capacity >= Container.Length;}

@xindent{Equivalent to Container := Slice (Container, Low, High);}

@xcode{@b{function} Replace_Slice (Container : Vector;

                        Low       : Index_Type;

                        High      : Extended_Index;

                        By        : Vector) @b{return} Vector

   @b{with} Pre  => (High @b{in} Low - 1 .. Container.Last_Index

                   @b{or else raise} Constraint_Error) @b{and then}

                (Container.Length - Count_Type (High - Low + 1) <=

                   Maximum_Length - By.Length

                   @b{or else raise} Constraint_Error),

        Post => Replace_Slice'Result.Length = Container.Length -

                   Count_Type (High - Low + 1) + By.Length @b{and then}

                @b{not} Tampering_With_Elements_Prohibited

                   (Replace_Slice'Result) @b{and then}

                @b{not} Tampering_With_Cursors_Prohibited

                   (Replace_Slice'Result) @b{and then}

                Replace_Slice'Result.Capacity >= Replace_Slice.Length;}

@xindent{This returns a copy of Container with the slice of elements from Low to High replaced with the vector By.}

@xcode{@b{procedure} Replace_Slice (Container : @b{in out} Vector;

                         Low       : @b{in}     Index_Type;

                         High      : @b{in}     Extended_Index;

                         By        : @b{in}     Vector)

   @b{with} Pre  => (@b{not} Tampering_With_Elements_Prohibited (Container)

                   @b{or else raise} Program_Error) @b{and then}

                (High @b{in} Low - 1 .. Container.Last_Index

                   @b{or else raise} Constraint_Error) @b{and then}

                (Container.Length - Count_Type (High - Low + 1) <=

                   Maximum_Length - By.Length

                   @b{or else raise} Constraint_Error),

        Post => Container.Length = Container.Length'Old -

                   Count_Type (High - Low + 1) + By.Length @b{and then}

                Container.Capacity >= Container.Length;}

@xindent{Equivalent to Container := Replace_Slice (Container, Low, High, By);

If High = Low - 1, then this is equivalent to Insert_Vector (Container, Low, By);}

!corrigendum A.18.19(9.1/5)

@drepl

@xbullet{The portion of the postcondition checking the capacity is omitted from subprograms Set_Length, Assign, Insert, Insert_Space, Prepend, Append, and Delete.}

@dby

@xbullet{The portion of the postcondition checking the capacity is omitted from subprograms Set_Length, Assign, Insert, Insert_Space, Slice, Replace_Slice, Prepend, Append, and Delete.}

!corrigendum A.18.19(9.2/5)

@drepl

@xbullet{For procedures Insert, Insert_Space, Prepend, and Append, the part of the precondition reading:}

@dby

@xbullet{For procedures Insert, Insert_Space, Replace_Slice, Prepend, and Append, the part of the precondition reading:}

!ACATS test

It would be appropriate to have ACATS C-tests for each of the four subprograms, with Low and High that succeed and fail, and for a null slice.

!appendix

See issue #75 from the ARG GitHub issue list.

 

From: Randy Brukardt
Added: Friday, August 2, 2024

John Barnes noted in his Editorial Review that the specifications in the !recommendation were different than those in the !wording. He recommended making them the same by adding the modes. However, the usual RM style for subprograms is to omit the mode for functions and give it for procedures. I’ve corrected all of the subprograms to match this style (which looks a bit weird in this case).

John also notes that the description of the function Slice mentions that it returns a “zero-length vector”; he thought that was a poor way to say that. I noted that we generally call that an “empty vector”(see functions Empty and Is_Empty, and the object Empty_Vector). I’ve corrected the wording accordingly.

 

[a]This capacity check is only necessary for operations that might expand the container; those are not very common. The majority of the operations don't need it as they cannot make the container larger; we wouldn't want to pay for an unneeded check on many common operations.

[b]I guess I am not convinced.  Implementations can optimize, but when it comes to the specification, I believe a simpler specification is better.  As it is now, we have a significant amount of redundancy in postconditions, which hides the signal in the noise.