------------------------------------------------------------------------------
--                                                                          --
--                         GNAT RUN-TIME COMPONENTS                         --
--                                                                          --
--                  A D A . S T R I N G S . B O U N D E D                   --
--                                                                          --
--                                 S p e c                                  --
--                                                                          --
--          Copyright (C) 1992-2023, Free Software Foundation, Inc.         --
--                                                                          --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. The copyright notice above, and the license provisions that follow --
-- apply solely to the  contents of the part following the private keyword. --
--                                                                          --
-- GNAT is free software;  you can  redistribute it  and/or modify it under --
-- terms of the  GNU General Public License as published  by the Free Soft- --
-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
--                                                                          --
-- As a special exception under Section 7 of GPL version 3, you are granted --
-- additional permissions described in the GCC Runtime Library Exception,   --
-- version 3.1, as published by the Free Software Foundation.               --
--                                                                          --
-- You should have received a copy of the GNU General Public License and    --
-- a copy of the GCC Runtime Library Exception along with this program;     --
-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
-- <http://www.gnu.org/licenses/>.                                          --
--                                                                          --
-- GNAT was originally developed  by the GNAT team at  New York University. --
-- Extensive contributions were provided by Ada Core Technologies Inc.      --
--                                                                          --
------------------------------------------------------------------------------

--  The language-defined package Strings.Bounded provides a generic package
--  each of whose instances yields a private type Bounded_String and a set
--  of operations. An object of a particular Bounded_String type represents
--  a String whose low bound is 1 and whose length can vary conceptually
--  between 0 and a maximum size established at the generic instantiation. The
--  subprograms for fixed-length string handling are either overloaded directly
--  for Bounded_String, or are modified as needed to reflect the variability in
--  length. Additionally, since the Bounded_String type is private, appropriate
--  constructor and selector operations are provided.

with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
with Ada.Strings.Superbounded;
with Ada.Strings.Search;

package Ada.Strings.Bounded with
  SPARK_Mode,
  Always_Terminates
is
   pragma Preelaborate;

   generic
      Max : Positive;
      --  Maximum length of a Bounded_String

   package Generic_Bounded_Length with SPARK_Mode,
     Initial_Condition => Length (Null_Bounded_String) = 0,
     Abstract_State    => null,
     Always_Terminates
   is
      --  Preconditions in this unit are meant for analysis only, not for
      --  run-time checking, so that the expected exceptions are raised. This
      --  is enforced by setting the corresponding assertion policy to Ignore.
      --  Postconditions and contract cases should not be executed at runtime
      --  as well, in order not to slow down the execution of these functions.

      pragma Assertion_Policy (Pre            => Ignore,
                               Post           => Ignore,
                               Contract_Cases => Ignore,
                               Ghost          => Ignore);

      Max_Length : constant Positive := Max;

      type Bounded_String is private;
      pragma Preelaborable_Initialization (Bounded_String);

      Null_Bounded_String : constant Bounded_String;
      --  Null_Bounded_String represents the null string. If an object of type
      --  Bounded_String is not otherwise initialized, it will be initialized
      --  to the same value as Null_Bounded_String.

      subtype Length_Range is Natural range 0 .. Max_Length;

      function Length (Source : Bounded_String) return Length_Range with
        Global => null;
      --  The Length function returns the length of the string represented by
      --  Source.

      --------------------------------------------------------
      -- Conversion, Concatenation, and Selection Functions --
      --------------------------------------------------------

      function To_Bounded_String
        (Source : String;
         Drop   : Truncation := Error) return Bounded_String
      with
        Pre            => (if Source'Length > Max_Length then Drop /= Error),
        Contract_Cases =>
          (Source'Length <= Max_Length
           =>
             To_String (To_Bounded_String'Result) = Source,

           Source'Length > Max_Length and then Drop = Left
           =>
             To_String (To_Bounded_String'Result) =
               Source (Source'Last - Max_Length + 1 .. Source'Last),

           others  --  Drop = Right
           =>
             To_String (To_Bounded_String'Result) =
               Source (Source'First .. Source'First - 1 + Max_Length));
      --  If Source'Length <= Max_Length, then this function returns a
      --  Bounded_String that represents Source. Otherwise, the effect
      --  depends on the value of Drop:
      --
      --  * If Drop=Left, then the result is a Bounded_String that represents
      --    the string comprising the rightmost Max_Length characters of
      --    Source.
      --
      --  * If Drop=Right, then the result is a Bounded_String that represents
      --    the string comprising the leftmost Max_Length characters of Source.
      --
      --  * If Drop=Error, then Strings.Length_Error is propagated.

      function To_String (Source : Bounded_String) return String with
        Global => null;
      --  To_String returns the String value with lower bound 1
      --  represented by Source. If B is a Bounded_String, then
      --  B = To_Bounded_String(To_String(B)).

      procedure Set_Bounded_String
        (Target : out Bounded_String;
         Source : String;
         Drop   : Truncation := Error)
      with
        Pre            => (if Source'Length > Max_Length then Drop /= Error),
        Contract_Cases =>
          (Source'Length <= Max_Length
           =>
             To_String (Target) = Source,

           Source'Length > Max_Length and then Drop = Left
           =>
             To_String (Target) =
               Source (Source'Last - Max_Length + 1 .. Source'Last),

           others  --  Drop = Right
           =>
             To_String (Target) =
               Source (Source'First .. Source'First - 1 + Max_Length));
      pragma Ada_05 (Set_Bounded_String);
      --  Equivalent to Target := To_Bounded_String (Source, Drop);

      --  Each of the Append functions returns a Bounded_String obtained by
      --  concatenating the string or character given or represented by one
      --  of the parameters, with the string or character given or represented
      --  by the other parameter, and applying To_Bounded_String to the
      --  concatenation result string, with Drop as provided to the Append
      --  function.

      function Append
        (Left  : Bounded_String;
         Right : Bounded_String;
         Drop  : Truncation  := Error) return Bounded_String
      with
        Pre            =>
          (if Length (Left) > Max_Length - Length (Right)
           then Drop /= Error),
        Contract_Cases =>
          (Length (Left) <= Max_Length - Length (Right)
           =>
             Length (Append'Result) = Length (Left) + Length (Right)
               and then
                 Slice (Append'Result, 1, Length (Left)) = To_String (Left)
               and then
                 (if Length (Right) > 0 then
                    Slice (Append'Result,
                      Length (Left) + 1, Length (Append'Result)) =
                        To_String (Right)),

           Length (Left) > Max_Length - Length (Right)
             and then Drop = Strings.Left
           =>
             Length (Append'Result) = Max_Length
               and then
                 (if Length (Right) < Max_Length then
                    Slice (Append'Result, 1, Max_Length - Length (Right)) =
                      Slice (Left,
                        Length (Left) - Max_Length + Length (Right) + 1,
                        Length (Left)))
               and then
                 Slice (Append'Result,
                   Max_Length - Length (Right) + 1, Max_Length) =
                     To_String (Right),

           others  --  Drop = Right
           =>
             Length (Append'Result) = Max_Length
               and then
                 Slice (Append'Result, 1, Length (Left)) = To_String (Left)
               and then
                 (if Length (Left) < Max_Length then
                    Slice (Append'Result, Length (Left) + 1, Max_Length) =
                      Slice (Right, 1, Max_Length - Length (Left))));

      function Append
        (Left  : Bounded_String;
         Right : String;
         Drop  : Truncation := Error) return Bounded_String
      with
        Pre            =>
          (if Right'Length > Max_Length - Length (Left)
           then Drop /= Error),
        Contract_Cases =>
          (Length (Left) <= Max_Length - Right'Length
           =>
             Length (Append'Result) = Length (Left) + Right'Length
               and then
                 Slice (Append'Result, 1, Length (Left)) = To_String (Left)
               and then
                 (if Right'Length > 0 then
                    Slice (Append'Result,
                      Length (Left) + 1, Length (Append'Result)) =
                        Right),

           Length (Left) > Max_Length - Right'Length
             and then Drop = Strings.Left
           =>
             Length (Append'Result) = Max_Length
               and then
                 (if Right'Length < Max_Length then

                    --  The result is the end of Left followed by Right

                    Slice (Append'Result, 1, Max_Length - Right'Length) =
                      Slice (Left,
                        Length (Left) - Max_Length + Right'Length + 1,
                        Length (Left))
                      and then
                        Slice (Append'Result,
                          Max_Length - Right'Length + 1, Max_Length) =
                            Right
                  else
                    --  The result is the last Max_Length characters of Right

                    To_String (Append'Result) =
                      Right (Right'Last - Max_Length + 1 .. Right'Last)),

           others  --  Drop = Right
           =>
             Length (Append'Result) = Max_Length
               and then
                 Slice (Append'Result, 1, Length (Left)) = To_String (Left)
               and then
                 (if Length (Left) < Max_Length then
                    Slice (Append'Result, Length (Left) + 1, Max_Length) =
                      Right (Right'First
                        .. Max_Length - Length (Left) - 1 + Right'First)));
      function Append
        (Left  : String;
         Right : Bounded_String;
         Drop  : Truncation := Error) return Bounded_String
      with
        Pre            =>
          (if Left'Length > Max_Length - Length (Right)
           then Drop /= Error),
        Contract_Cases =>
          (Left'Length <= Max_Length - Length (Right)
           =>
             Length (Append'Result) = Left'Length + Length (Right)
               and then Slice (Append'Result, 1, Left'Length) = Left
               and then
                 (if Length (Right) > 0 then
                    Slice (Append'Result,
                      Left'Length + 1, Length (Append'Result)) =
                        To_String (Right)),

           Left'Length > Max_Length - Length (Right)
             and then Drop = Strings.Left
           =>
             Length (Append'Result) = Max_Length
               and then
                 (if Length (Right) < Max_Length then
                    Slice (Append'Result, 1, Max_Length - Length (Right)) =
                      Left (Left'Last - Max_Length + Length (Right) + 1
                            .. Left'Last))
               and then
                 Slice (Append'Result,
                   Max_Length - Length (Right) + 1, Max_Length) =
                     To_String (Right),

           others  --  Drop = Right
           =>
             Length (Append'Result) = Max_Length
               and then
                 (if Left'Length < Max_Length then

                    --  The result is Left followed by the beginning of Right

                    Slice (Append'Result, 1, Left'Length) = Left
                      and then
                        Slice (Append'Result, Left'Length + 1, Max_Length) =
                          Slice (Right, 1, Max_Length - Left'Length)
                  else
                    --  The result is the first Max_Length characters of Left

                    To_String (Append'Result) =
                      Left (Left'First .. Max_Length - 1 + Left'First)));

      function Append
        (Left  : Bounded_String;
         Right : Character;
         Drop  : Truncation := Error) return Bounded_String
      with
        Pre            => (if Length (Left) = Max_Length then Drop /= Error),
        Contract_Cases =>
          (Length (Left) < Max_Length
           =>
             Length (Append'Result) = Length (Left) + 1
               and then
                 Slice (Append'Result, 1, Length (Left)) = To_String (Left)
               and then Element (Append'Result, Length (Left) + 1) = Right,

           Length (Left) = Max_Length and then Drop = Strings.Right
           =>
             Length (Append'Result) = Max_Length
               and then To_String (Append'Result) = To_String (Left),

           others  --  Drop = Left
           =>
             Length (Append'Result) = Max_Length
               and then
                 Slice (Append'Result, 1, Max_Length - 1) =
                   Slice (Left, 2, Max_Length)
               and then Element (Append'Result, Max_Length) = Right);

      function Append
        (Left  : Character;
         Right : Bounded_String;
         Drop  : Truncation := Error) return Bounded_String
      with
        Pre            => (if Length (Right) = Max_Length then Drop /= Error),
        Contract_Cases =>
          (Length (Right) < Max_Length
           =>
             Length (Append'Result) = Length (Right) + 1
               and then
                 Slice (Append'Result, 2, Length (Right) + 1) =
                   To_String (Right)
               and then Element (Append'Result, 1) = Left,

           Length (Right) = Max_Length and then Drop = Strings.Left
           =>
             Length (Append'Result) = Max_Length
               and then To_String (Append'Result) = To_String (Right),

           others  --  Drop = Right
           =>
             Length (Append'Result) = Max_Length
               and then
                 Slice (Append'Result, 2, Max_Length) =
                   Slice (Right, 1, Max_Length - 1)
               and then Element (Append'Result, 1) = Left);

      --  Each of the procedures Append(Source, New_Item, Drop) has the same
      --  effect as the corresponding assignment
      --  Source := Append(Source, New_Item, Drop).

      procedure Append
        (Source   : in out Bounded_String;
         New_Item : Bounded_String;
         Drop     : Truncation  := Error)
      with
        Pre            =>
          (if Length (Source) > Max_Length - Length (New_Item)
           then Drop /= Error),
        Contract_Cases =>
          (Length (Source) <= Max_Length - Length (New_Item)
           =>
             Length (Source) = Length (Source'Old) + Length (New_Item)
               and then
                 Slice (Source, 1, Length (Source'Old)) =
                   To_String (Source'Old)
               and then
                 (if Length (New_Item) > 0 then
                    Slice (Source, Length (Source'Old) + 1, Length (Source)) =
                      To_String (New_Item)),

           Length (Source) > Max_Length - Length (New_Item)
             and then Drop = Left
           =>
             Length (Source) = Max_Length
               and then
                 (if Length (New_Item) < Max_Length then
                    Slice (Source, 1, Max_Length - Length (New_Item)) =
                      Slice (Source'Old,
                        Length (Source'Old) - Max_Length + Length (New_Item)
                          + 1,
                        Length (Source'Old)))
               and then
                 Slice (Source, Max_Length - Length (New_Item) + 1, Max_Length)
                   = To_String (New_Item),

           others  --  Drop = Right
           =>
             Length (Source) = Max_Length
               and then
                 Slice (Source, 1, Length (Source'Old)) =
                   To_String (Source'Old)
               and then
                 (if Length (Source'Old) < Max_Length then
                    Slice (Source, Length (Source'Old) + 1, Max_Length) =
                      Slice (New_Item, 1, Max_Length - Length (Source'Old))));

      procedure Append
        (Source   : in out Bounded_String;
         New_Item : String;
         Drop     : Truncation  := Error)
      with
        Pre            =>
          (if New_Item'Length > Max_Length - Length (Source)
           then Drop /= Error),
        Contract_Cases =>
          (Length (Source) <= Max_Length - New_Item'Length
           =>
             Length (Source) = Length (Source'Old) + New_Item'Length
               and then
                 Slice (Source, 1, Length (Source'Old)) =
                   To_String (Source'Old)
               and then
                 (if New_Item'Length > 0 then
                    Slice (Source, Length (Source'Old) + 1, Length (Source)) =
                      New_Item),

           Length (Source) > Max_Length - New_Item'Length
             and then Drop = Left
           =>
             Length (Source) = Max_Length
               and then
                 (if New_Item'Length < Max_Length then

                    --  The result is the end of Source followed by New_Item

                    Slice (Source, 1, Max_Length - New_Item'Length) =
                      Slice (Source'Old,
                        Length (Source'Old) - Max_Length + New_Item'Length + 1,
                        Length (Source'Old))
                    and then
                      Slice (Source,
                        Max_Length - New_Item'Length + 1, Max_Length) =
                          New_Item
                  else
                    --  The result is the last Max_Length characters of
                    --  New_Item.

                    To_String (Source) = New_Item
                      (New_Item'Last - Max_Length + 1 .. New_Item'Last)),

           others  --  Drop = Right
           =>
             Length (Source) = Max_Length
               and then
                 Slice (Source, 1, Length (Source'Old)) =
                   To_String (Source'Old)
               and then
                 (if Length (Source'Old) < Max_Length then
                    Slice (Source, Length (Source'Old) + 1, Max_Length) =
                      New_Item (New_Item'First
                        .. Max_Length - Length (Source'Old) - 1
                          + New_Item'First)));

      procedure Append
        (Source   : in out Bounded_String;
         New_Item : Character;
         Drop     : Truncation  := Error)
      with
        Pre            => (if Length (Source) = Max_Length then Drop /= Error),
        Contract_Cases =>
          (Length (Source) < Max_Length
           =>
             Length (Source) = Length (Source'Old) + 1
               and then
                 Slice (Source, 1, Length (Source'Old)) =
                   To_String (Source'Old)
               and then Element (Source, Length (Source'Old) + 1) = New_Item,

           Length (Source) = Max_Length and then Drop = Right
           =>
             Length (Source) = Max_Length
               and then To_String (Source) = To_String (Source'Old),

           others  --  Drop = Left
           =>
             Length (Source) = Max_Length
               and then
                 Slice (Source, 1, Max_Length - 1) =
                   Slice (Source'Old, 2, Max_Length)
               and then Element (Source, Max_Length) = New_Item);

      --  Each of the "&" functions has the same effect as the corresponding
      --  Append function, with Error as the Drop parameter.

      function "&"
        (Left  : Bounded_String;
         Right : Bounded_String) return Bounded_String
      with
        Pre  => Length (Left) <= Max_Length - Length (Right),
        Post => Length ("&"'Result) = Length (Left) + Length (Right)
          and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
          and then
            (if Length (Right) > 0 then
               Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) =
                 To_String (Right));

      function "&"
        (Left  : Bounded_String;
         Right : String) return Bounded_String
      with
        Pre  => Right'Length <= Max_Length - Length (Left),
        Post => Length ("&"'Result) = Length (Left) + Right'Length
          and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
          and then
            (if Right'Length > 0 then
               Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) =
                 Right);

      function "&"
        (Left  : String;
         Right : Bounded_String) return Bounded_String
      with
        Pre  => Left'Length <= Max_Length - Length (Right),
        Post => Length ("&"'Result) = Left'Length + Length (Right)
          and then Slice ("&"'Result, 1, Left'Length) = Left
          and then
            (if Length (Right) > 0 then
               Slice ("&"'Result, Left'Length + 1, Length ("&"'Result)) =
                 To_String (Right));

      function "&"
        (Left  : Bounded_String;
         Right : Character) return Bounded_String
      with
        Pre  => Length (Left) < Max_Length,
        Post => Length ("&"'Result) = Length (Left) + 1
          and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
          and then Element ("&"'Result, Length (Left) + 1) = Right;

      function "&"
        (Left  : Character;
         Right : Bounded_String) return Bounded_String
      with
        Pre  => Length (Right) < Max_Length,
        Post => Length ("&"'Result) = 1 + Length (Right)
          and then Element ("&"'Result, 1) = Left
          and then
            Slice ("&"'Result, 2, Length ("&"'Result)) = To_String (Right);

      function Element
        (Source : Bounded_String;
         Index  : Positive) return Character
      with
        Pre    => Index <= Length (Source),
        Global => null;
      --  Returns the character at position Index in the string represented by
      --  Source; propagates Index_Error if Index > Length(Source).

      procedure Replace_Element
        (Source : in out Bounded_String;
         Index  : Positive;
         By     : Character)
      with
        Pre    => Index <= Length (Source),
        Post   => Length (Source) = Length (Source'Old)
          and then (for all K in 1 .. Length (Source) =>
                      Element (Source, K) =
                        (if K = Index then By else Element (Source'Old, K))),
        Global => null;
      --  Updates Source such that the character at position Index in the
      --  string represented by Source is By; propagates Index_Error if
      --  Index > Length(Source).

      function Slice
        (Source : Bounded_String;
         Low    : Positive;
         High   : Natural) return String
      with
        Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
        Global => null;
      --  Returns the slice at positions Low through High in the
      --  string represented by Source; propagates Index_Error if
      --  Low > Length(Source)+1 or High > Length(Source).
      --  The bounds of the returned string are Low and High.

      function Bounded_Slice
        (Source : Bounded_String;
         Low    : Positive;
         High   : Natural) return Bounded_String
       with
        Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
        Post   => To_String (Bounded_Slice'Result) = Slice (Source, Low, High),
        Global => null;
      pragma Ada_05 (Bounded_Slice);
      --  Returns the slice at positions Low through High in the string
      --  represented by Source as a bounded string; propagates Index_Error
      --  if Low > Length(Source)+1 or High > Length(Source).

      procedure Bounded_Slice
        (Source : Bounded_String;
         Target : out Bounded_String;
         Low    : Positive;
         High   : Natural)
      with
        Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
        Post   => To_String (Target) = Slice (Source, Low, High),
        Global => null;
      pragma Ada_05 (Bounded_Slice);
      --  Equivalent to Target := Bounded_Slice (Source, Low, High);

      --  Each of the functions "=", "<", ">", "<=", and ">=" returns the same
      --  result as the corresponding String operation applied to the String
      --  values given or represented by the two parameters.

      function "="
        (Left  : Bounded_String;
         Right : Bounded_String) return Boolean
      with
        Post   => "="'Result = (To_String (Left) = To_String (Right)),
        Global => null;

      function "="
        (Left  : Bounded_String;
         Right : String) return Boolean
      with
        Post   => "="'Result = (To_String (Left) = Right),
        Global => null;

      function "="
        (Left  : String;
         Right : Bounded_String) return Boolean
      with
        Post   => "="'Result = (Left = To_String (Right)),
        Global => null;

      function "<"
        (Left  : Bounded_String;
         Right : Bounded_String) return Boolean
      with
        Post   => "<"'Result = (To_String (Left) < To_String (Right)),
        Global => null;

      function "<"
        (Left  : Bounded_String;
         Right : String) return Boolean
      with
        Post   => "<"'Result = (To_String (Left) < Right),
        Global => null;

      function "<"
        (Left  : String;
         Right : Bounded_String) return Boolean
      with
        Post   => "<"'Result = (Left < To_String (Right)),
        Global => null;

      function "<="
        (Left  : Bounded_String;
         Right : Bounded_String) return Boolean
      with
        Post   => "<="'Result = (To_String (Left) <= To_String (Right)),
        Global => null;

      function "<="
        (Left  : Bounded_String;
         Right : String) return Boolean
      with
        Post   => "<="'Result = (To_String (Left) <= Right),
        Global => null;

      function "<="
        (Left  : String;
         Right : Bounded_String) return Boolean
      with
        Post   => "<="'Result = (Left <= To_String (Right)),
        Global => null;

      function ">"
        (Left  : Bounded_String;
         Right : Bounded_String) return Boolean
      with
        Post   => ">"'Result = (To_String (Left) > To_String (Right)),
        Global => null;

      function ">"
        (Left  : Bounded_String;
         Right : String) return Boolean
      with
        Post   => ">"'Result = (To_String (Left) > Right),
        Global => null;

      function ">"
        (Left  : String;
         Right : Bounded_String) return Boolean
      with
        Post   => ">"'Result = (Left > To_String (Right)),
        Global => null;

      function ">="
        (Left  : Bounded_String;
         Right : Bounded_String) return Boolean
      with
        Post   => ">="'Result = (To_String (Left) >= To_String (Right)),
        Global => null;

      function ">="
        (Left  : Bounded_String;
         Right : String) return Boolean
      with
        Post   => ">="'Result = (To_String (Left) >= Right),
        Global => null;

      function ">="
        (Left  : String;
         Right : Bounded_String) return Boolean
      with
        Post   => ">="'Result = (Left >= To_String (Right)),
        Global => null;

      ----------------------
      -- Search Functions --
      ----------------------

      --  Each of the search subprograms (Index, Index_Non_Blank, Count,
      --  Find_Token) has the same effect as the corresponding subprogram in
      --  Strings.Fixed applied to the string represented by the Bounded_String
      --  parameter.

      function Index
        (Source  : Bounded_String;
         Pattern : String;
         Going   : Direction := Forward;
         Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
      with
        Pre            => Pattern'Length > 0,
        Post           => Index'Result <= Length (Source),
        Contract_Cases =>

          --  If Source is the empty string, then 0 is returned

          (Length (Source) = 0
           =>
             Index'Result = 0,

           --  If some slice of Source matches Pattern, then a valid index is
           --  returned.

           Length (Source) > 0
             and then
               (for some J in 1 .. Length (Source) - (Pattern'Length - 1) =>
                  Search.Match (To_String (Source), Pattern, Mapping, J))
           =>
             --  The result is in the considered range of Source

             Index'Result in 1 .. Length (Source) - (Pattern'Length - 1)

               --  The slice beginning at the returned index matches Pattern

               and then Search.Match
                 (To_String (Source), Pattern, Mapping, Index'Result)

               --  The result is the smallest or largest index which satisfies
               --  the matching, respectively when Going = Forward and Going =
               --  Backward.

               and then
                 (for all J in 1 .. Length (Source) =>
                    (if (if Going = Forward
                         then J <= Index'Result - 1
                         else J - 1 in Index'Result
                                       .. Length (Source) - Pattern'Length)
                     then not (Search.Match
                       (To_String (Source), Pattern, Mapping, J)))),

           --  Otherwise, 0 is returned

           others
           =>
             Index'Result = 0),
        Global         => null;

      function Index
        (Source  : Bounded_String;
         Pattern : String;
         Going   : Direction := Forward;
         Mapping : Maps.Character_Mapping_Function) return Natural
      with
        Pre            => Pattern'Length /= 0 and then Mapping /= null,
        Post           => Index'Result <= Length (Source),
        Contract_Cases =>

          --  If Source is the empty string, then 0 is returned

          (Length (Source) = 0
           =>
             Index'Result = 0,

           --  If some slice of Source matches Pattern, then a valid index is
           --  returned.

           Length (Source) > 0
             and then
               (for some J in 1 .. Length (Source) - (Pattern'Length - 1) =>
                  Search.Match (To_String (Source), Pattern, Mapping, J))
           =>
             --  The result is in the considered range of Source

             Index'Result in 1 .. Length (Source) - (Pattern'Length - 1)

               --  The slice beginning at the returned index matches Pattern

               and then Search.Match
                 (To_String (Source), Pattern, Mapping, Index'Result)

               --  The result is the smallest or largest index which satisfies
               --  the matching, respectively when Going = Forward and Going =
               --  Backward.

               and then
                 (for all J in 1 .. Length (Source) =>
                    (if (if Going = Forward
                         then J <= Index'Result - 1
                         else J - 1 in Index'Result
                                       .. Length (Source) - Pattern'Length)
                     then not (Search.Match
                       (To_String (Source), Pattern, Mapping, J)))),

           --  Otherwise, 0 is returned

           others
           =>
             Index'Result = 0),
        Global         => null;

      function Index
        (Source : Bounded_String;
         Set    : Maps.Character_Set;
         Test   : Membership := Inside;
         Going  : Direction  := Forward) return Natural
      with
        Post           => Index'Result <= Length (Source),
        Contract_Cases =>

           --  If no character of Source satisfies the property Test on Set,
           --  then 0 is returned.

          ((for all C of To_String (Source) =>
              (Test = Inside) /= Maps.Is_In (C, Set))
           =>
             Index'Result = 0,

           --  Otherwise, an index in the range of Source is returned

           others
           =>
             --  The result is in the range of Source

             Index'Result in 1 .. Length (Source)

               --  The character at the returned index satisfies the property
               --  Test on Set.

               and then
                 (Test = Inside) =
                   Maps.Is_In (Element (Source, Index'Result), Set)

               --  The result is the smallest or largest index which satisfies
               --  the property, respectively when Going = Forward and Going =
               --  Backward.

               and then
                 (for all J in 1 .. Length (Source) =>
                    (if J /= Index'Result
                          and then (J < Index'Result) = (Going = Forward)
                     then (Test = Inside)
                          /= Maps.Is_In (Element (Source, J), Set)))),
        Global         => null;

      function Index
        (Source  : Bounded_String;
         Pattern : String;
         From    : Positive;
         Going   : Direction := Forward;
         Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
      with
        Pre            =>
          (if Length (Source) /= 0 then From <= Length (Source))
            and then Pattern'Length /= 0,
        Post           => Index'Result <= Length (Source),
        Contract_Cases =>

          --  If Source is the empty string, then 0 is returned

          (Length (Source) = 0
           =>
             Index'Result = 0,

           --  If some slice of Source matches Pattern, then a valid index is
           --  returned.

           Length (Source) > 0
             and then
               (for some J in
                 (if Going = Forward then From else 1)
                  .. (if Going = Forward then Length (Source) else From)
                   - (Pattern'Length - 1) =>
                 Search.Match (To_String (Source), Pattern, Mapping, J))
           =>
             --  The result is in the considered range of Source

             Index'Result in
               (if Going = Forward then From else 1)
               .. (if Going = Forward then Length (Source) else From)
                - (Pattern'Length - 1)

               --  The slice beginning at the returned index matches Pattern

               and then Search.Match
                 (To_String (Source), Pattern, Mapping, Index'Result)

               --  The result is the smallest or largest index which satisfies
               --  the matching, respectively when Going = Forward and Going =
               --  Backward.

               and then
                 (for all J in 1 .. Length (Source) =>
                    (if (if Going = Forward
                         then J in From .. Index'Result - 1
                         else J - 1 in Index'Result
                                       .. From - Pattern'Length)
                     then not (Search.Match
                       (To_String (Source), Pattern, Mapping, J)))),

           --  Otherwise, 0 is returned

           others
           =>
             Index'Result = 0),
        Global         => null;
      pragma Ada_05 (Index);

      function Index
        (Source  : Bounded_String;
         Pattern : String;
         From    : Positive;
         Going   : Direction := Forward;
         Mapping : Maps.Character_Mapping_Function) return Natural
      with
        Pre            =>
          (if Length (Source) /= 0 then From <= Length (Source))
            and then Pattern'Length /= 0
            and then Mapping /= null,
        Post           => Index'Result <= Length (Source),
        Contract_Cases =>

          --  If Source is the empty string, then 0 is returned

          (Length (Source) = 0
           =>
             Index'Result = 0,

           --  If some slice of Source matches Pattern, then a valid index is
           --  returned.

           Length (Source) > 0
             and then
               (for some J in
                 (if Going = Forward then From else 1)
                  .. (if Going = Forward then Length (Source) else From)
                   - (Pattern'Length - 1) =>
                 Search.Match (To_String (Source), Pattern, Mapping, J))
           =>
             --  The result is in the considered range of Source

             Index'Result in
               (if Going = Forward then From else 1)
               .. (if Going = Forward then Length (Source) else From)
                - (Pattern'Length - 1)

               --  The slice beginning at the returned index matches Pattern

               and then Search.Match
                 (To_String (Source), Pattern, Mapping, Index'Result)

               --  The result is the smallest or largest index which satisfies
               --  the matching, respectively when Going = Forward and Going =
               --  Backward.

               and then
                 (for all J in 1 .. Length (Source) =>
                    (if (if Going = Forward
                         then J in From .. Index'Result - 1
                         else J - 1 in Index'Result
                                       .. From - Pattern'Length)
                     then not (Search.Match
                       (To_String (Source), Pattern, Mapping, J)))),

           --  Otherwise, 0 is returned

           others
           =>
             Index'Result = 0),
        Global         => null;
      pragma Ada_05 (Index);

      function Index
        (Source  : Bounded_String;
         Set     : Maps.Character_Set;
         From    : Positive;
         Test    : Membership := Inside;
         Going   : Direction := Forward) return Natural
      with
        Pre            =>
          (if Length (Source) /= 0 then From <= Length (Source)),
        Post           => Index'Result <= Length (Source),
        Contract_Cases =>

           --  If Source is the empty string, or no character of the considered
           --  slice of Source satisfies the property Test on Set, then 0 is
           --  returned.

          (Length (Source) = 0
             or else
               (for all J in 1 .. Length (Source) =>
                  (if J = From or else (J > From) = (Going = Forward) then
                     (Test = Inside) /= Maps.Is_In (Element (Source, J), Set)))
           =>
             Index'Result = 0,

           --  Otherwise, an index in the considered range of Source is
           --  returned.

           others
           =>
             --  The result is in the considered range of Source

             Index'Result in 1 .. Length (Source)
               and then
                 (Index'Result = From
                    or else (Index'Result > From) = (Going = Forward))

               --  The character at the returned index satisfies the property
               --  Test on Set.

               and then
                 (Test = Inside) =
                   Maps.Is_In (Element (Source, Index'Result), Set)

               --  The result is the smallest or largest index which satisfies
               --  the property, respectively when Going = Forward and Going =
               --  Backward.

               and then
                 (for all J in 1 .. Length (Source) =>
                    (if J /= Index'Result
                       and then (J < Index'Result) = (Going = Forward)
                       and then (J = From
                                   or else (J > From) = (Going = Forward))
                     then (Test = Inside)
                          /= Maps.Is_In (Element (Source, J), Set)))),
        Global         => null;
      pragma Ada_05 (Index);

      function Index_Non_Blank
        (Source : Bounded_String;
         Going  : Direction := Forward) return Natural
      with
        Post           => Index_Non_Blank'Result <= Length (Source),
        Contract_Cases =>

           --  If all characters of Source are Space characters, then 0 is
           --  returned.

          ((for all C of To_String (Source) => C = ' ')
           =>
             Index_Non_Blank'Result = 0,

           --  Otherwise, an index in the range of Source is returned

           others
           =>
             --  The result is in the range of Source

             Index_Non_Blank'Result in 1 .. Length (Source)

               --  The character at the returned index is not a Space character

               and then Element (Source, Index_Non_Blank'Result) /= ' '

               --  The result is the smallest or largest index which is not a
               --  Space character, respectively when Going = Forward and Going
               --  = Backward.

               and then
                 (for all J in 1 .. Length (Source) =>
                    (if J /= Index_Non_Blank'Result
                          and then
                            (J < Index_Non_Blank'Result) = (Going = Forward)
                     then Element (Source, J) = ' '))),
        Global         => null;

      function Index_Non_Blank
        (Source : Bounded_String;
         From   : Positive;
         Going  : Direction := Forward) return Natural
      with
        Pre            =>
          (if Length (Source) /= 0 then From <= Length (Source)),
        Post           => Index_Non_Blank'Result <= Length (Source),
        Contract_Cases =>

           --  If Source is the empty string, or all characters of the
           --  considered slice of Source are Space characters, then 0
           --  is returned.

          (Length (Source) = 0
             or else
               (for all J in 1 .. Length (Source) =>
                  (if J = From or else (J > From) = (Going = Forward) then
                     Element (Source, J) = ' '))
           =>
             Index_Non_Blank'Result = 0,

           --  Otherwise, an index in the considered range of Source is
           --  returned.

           others
           =>
             --  The result is in the considered range of Source

             Index_Non_Blank'Result in 1 .. Length (Source)
               and then
                 (Index_Non_Blank'Result = From
                    or else
                      (Index_Non_Blank'Result > From) = (Going = Forward))

               --  The character at the returned index is not a Space character

               and then Element (Source, Index_Non_Blank'Result) /= ' '

               --  The result is the smallest or largest index which isn't a
               --  Space character, respectively when Going = Forward and Going
               --  = Backward.

               and then
                 (for all J in 1 .. Length (Source) =>
                    (if J /= Index_Non_Blank'Result
                       and then
                         (J < Index_Non_Blank'Result) = (Going = Forward)
                       and then (J = From
                                   or else (J > From) = (Going = Forward))
                     then Element (Source, J) = ' '))),
        Global         => null;
      pragma Ada_05 (Index_Non_Blank);

      function Count
        (Source  : Bounded_String;
         Pattern : String;
         Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
      with
        Pre    => Pattern'Length /= 0,
        Global => null;

      function Count
        (Source  : Bounded_String;
         Pattern : String;
         Mapping : Maps.Character_Mapping_Function) return Natural
      with
        Pre    => Pattern'Length /= 0 and then Mapping /= null,
        Global => null;

      function Count
        (Source : Bounded_String;
         Set    : Maps.Character_Set) return Natural
      with
        Global => null;

      procedure Find_Token
        (Source : Bounded_String;
         Set    : Maps.Character_Set;
         From   : Positive;
         Test   : Membership;
         First  : out Positive;
         Last   : out Natural)
      with
        Pre            =>
          (if Length (Source) /= 0 then From <= Length (Source)),
        Contract_Cases =>

           --  If Source is the empty string, or if no character of the
           --  considered slice of Source satisfies the property Test on
           --  Set, then First is set to From and Last is set to 0.

          (Length (Source) = 0
             or else
               (for all J in From .. Length (Source) =>
                  (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
           =>
             First = From and then Last = 0,

           --  Otherwise, First and Last are set to valid indexes

           others
           =>
             --  First and Last are in the considered range of Source

             First in From .. Length (Source)
               and then Last in First .. Length (Source)

               --  No character between From and First satisfies the property
               --  Test on Set.

               and then
                 (for all J in From .. First - 1 =>
                    (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))

               --  All characters between First and Last satisfy the property
               --  Test on Set.

               and then
                 (for all J in First .. Last =>
                    (Test = Inside) = Maps.Is_In (Element (Source, J), Set))

               --  If Last is not Source'Last, then the character at position
               --  Last + 1 does not satify the property Test on Set.

               and then
                 (if Last < Length (Source)
                  then
                    (Test = Inside)
                    /= Maps.Is_In (Element (Source, Last + 1), Set))),
        Global         => null;
      pragma Ada_2012 (Find_Token);

      procedure Find_Token
        (Source : Bounded_String;
         Set    : Maps.Character_Set;
         Test   : Membership;
         First  : out Positive;
         Last   : out Natural)
      with
        Contract_Cases =>

           --  If Source is the empty string, or if no character of the
           --  considered slice of Source satisfies the property Test on
           --  Set, then First is set to 1 and Last is set to 0.

          (Length (Source) = 0
             or else
               (for all J in 1 .. Length (Source) =>
                  (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
           =>
             First = 1 and then Last = 0,

           --  Otherwise, First and Last are set to valid indexes

           others
           =>
             --  First and Last are in the considered range of Source

             First in 1 .. Length (Source)
               and then Last in First .. Length (Source)

               --  No character between 1 and First satisfies the property Test
               --  on Set.

               and then
                 (for all J in 1 .. First - 1 =>
                    (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))

               --  All characters between First and Last satisfy the property
               --  Test on Set.

               and then
                 (for all J in First .. Last =>
                    (Test = Inside) = Maps.Is_In (Element (Source, J), Set))

               --  If Last is not Source'Last, then the character at position
               --  Last + 1 does not satify the property Test on Set.

               and then
                 (if Last < Length (Source)
                  then
                    (Test = Inside)
                    /= Maps.Is_In (Element (Source, Last + 1), Set))),
        Global         => null;

      ------------------------------------
      -- String Translation Subprograms --
      ------------------------------------

      --  Each of the Translate subprograms, when applied to a Bounded_String,
      --  has an analogous effect to the corresponding subprogram in
      --  Strings.Fixed. For the Translate function, the translation is applied
      --  to the string represented by the Bounded_String parameter, and the
      --  result is converted (via To_Bounded_String) to a Bounded_String. For
      --  the Translate procedure, the string represented by the Bounded_String
      --  parameter after the translation is given by the Translate function
      --  for fixed-length strings applied to the string represented by the
      --  original value of the parameter.

      function Translate
        (Source  : Bounded_String;
         Mapping : Maps.Character_Mapping) return Bounded_String
      with
        Post   => Length (Translate'Result) = Length (Source)
          and then
            (for all K in 1 .. Length (Source) =>
               Element (Translate'Result, K) =
                 Ada.Strings.Maps.Value (Mapping, Element (Source, K))),
        Global => null;

      procedure Translate
        (Source   : in out Bounded_String;
         Mapping  : Maps.Character_Mapping)
      with
        Post   => Length (Source) = Length (Source'Old)
          and then
            (for all K in 1 .. Length (Source) =>
               Element (Source, K) =
                 Ada.Strings.Maps.Value (Mapping, Element (Source'Old, K))),
        Global => null;

      function Translate
        (Source  : Bounded_String;
         Mapping : Maps.Character_Mapping_Function) return Bounded_String
      with
        Pre    => Mapping /= null,
        Post   => Length (Translate'Result) = Length (Source)
          and then
            (for all K in 1 .. Length (Source) =>
               Element (Translate'Result, K) = Mapping (Element (Source, K))),
        Global => null;
      pragma Annotate (GNATprove, False_Positive,
                       "call via access-to-subprogram",
                       "function Mapping must always terminate");

      procedure Translate
        (Source  : in out Bounded_String;
         Mapping : Maps.Character_Mapping_Function)
      with
        Pre    => Mapping /= null,
        Post   => Length (Source) = Length (Source'Old)
          and then
            (for all K in 1 .. Length (Source) =>
               Element (Source, K) = Mapping (Element (Source'Old, K))),
        Global => null;
      pragma Annotate (GNATprove, False_Positive,
                       "call via access-to-subprogram",
                       "function Mapping must always terminate");

      ---------------------------------------
      -- String Transformation Subprograms --
      ---------------------------------------

      --  Each of the transformation subprograms (Replace_Slice, Insert,
      --  Overwrite, Delete), selector subprograms (Trim, Head, Tail), and
      --  constructor functions ("*") has an effect based on its corresponding
      --  subprogram in Strings.Fixed, and Replicate is based on Fixed."*".
      --  In the case of a function, the corresponding fixed-length string
      --  subprogram is applied to the string represented by the Bounded_String
      --  parameter. To_Bounded_String is applied the result string, with Drop
      --  (or Error in the case of Generic_Bounded_Length."*") determining
      --  the effect when the string length exceeds Max_Length. In
      --  the case of a procedure, the corresponding function in
      --  Strings.Bounded.Generic_Bounded_Length is applied, with the
      --  result assigned into the Source parameter.

      function Replace_Slice
        (Source : Bounded_String;
         Low    : Positive;
         High   : Natural;
         By     : String;
         Drop   : Truncation := Error) return Bounded_String
      with
        Pre            =>
          Low - 1 <= Length (Source)
            and then
              (if Drop = Error
                 then (if High >= Low
                         then Low - 1
                           <= Max_Length - By'Length
                            - Integer'Max (Length (Source) - High, 0)
                         else Length (Source) <= Max_Length - By'Length)),
        Contract_Cases =>
          (Low - 1 <= Max_Length - By'Length
             - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
           =>
             --  Total length is lower than Max_Length: nothing is dropped

             --  Note that if High < Low, the insertion is done before Low,
             --  so in all cases the starting position of the slice of Source
             --  remaining after the replaced Slice is Integer'Max (High + 1,
             --  Low).

             Length (Replace_Slice'Result) = Low - 1 + By'Length
               + Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
               and then
                 Slice (Replace_Slice'Result, 1, Low - 1) =
                   Slice (Source, 1, Low - 1)
               and then
                 Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By
               and then
                 (if Integer'Max (High, Low - 1) < Length (Source) then
                    Slice (Replace_Slice'Result,
                      Low + By'Length, Length (Replace_Slice'Result)) =
                        Slice (Source,
                          Integer'Max (High + 1, Low), Length (Source))),

           Low - 1 > Max_Length - By'Length
             - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
             and then Drop = Left
           =>
             --  Final_Slice is the length of the slice of Source remaining
             --  after the replaced part.
             (declare
                Final_Slice : constant Natural :=
                  Integer'Max
                    (Length (Source) - Integer'Max (High, Low - 1), 0);
              begin
                --  The result is of maximal length and ends by the last
                --  Final_Slice characters of Source.

                Length (Replace_Slice'Result) = Max_Length
                  and then
                    (if Final_Slice > 0 then
                       Slice (Replace_Slice'Result,
                         Max_Length - Final_Slice + 1, Max_Length) =
                           Slice (Source,
                             Integer'Max (High + 1, Low), Length (Source)))

                  --  Depending on when we reach Max_Length, either the first
                  --  part of Source is fully dropped and By is partly dropped,
                  --  or By is fully added and the first part of Source is
                  --  partly dropped.

                  and then
                   (if Max_Length - Final_Slice - By'Length <= 0 then

                      --  The first (possibly zero) characters of By are
                      --  dropped.

                      (if Final_Slice < Max_Length then
                         Slice (Replace_Slice'Result,
                           1, Max_Length - Final_Slice) =
                             By (By'Last - Max_Length + Final_Slice + 1
                                 .. By'Last))

                    else  --  By is added to the result

                      Slice (Replace_Slice'Result,
                        Max_Length - Final_Slice - By'Length + 1,
                        Max_Length - Final_Slice) =
                          By

                        --  The first characters of Source (1 .. Low - 1) are
                        --  dropped.

                        and then Slice (Replace_Slice'Result, 1,
                          Max_Length - Final_Slice - By'Length) =
                            Slice (Source,
                              Low - Max_Length + Final_Slice + By'Length,
                              Low - 1))),

           others  --  Drop = Right
           =>
             --  The result is of maximal length and starts by the first Low -
             --  1 characters of Source.

             Length (Replace_Slice'Result) = Max_Length
               and then
                 Slice (Replace_Slice'Result, 1, Low - 1) =
                   Slice (Source, 1, Low - 1)

               --  Depending on when we reach Max_Length, either the last part
               --  of Source is fully dropped and By is partly dropped, or By
               --  is fully added and the last part of Source is partly
               --  dropped.

               and then
                 (if Low - 1 >= Max_Length - By'Length then

                    --  The last characters of By are dropped

                    Slice (Replace_Slice'Result, Low, Max_Length) =
                      By (By'First .. Max_Length - Low + By'First)

                  else  --  By is fully added

                    Slice (Replace_Slice'Result, Low, Low + By'Length - 1) = By

                      --  Then Source starting from Integer'Max (High + 1, Low)
                      --  is added but the last characters are dropped.

                      and then Slice (Replace_Slice'Result,
                        Low + By'Length, Max_Length) =
                          Slice (Source, Integer'Max (High + 1, Low),
                            Integer'Max (High + 1, Low) +
                              (Max_Length - Low - By'Length))));

      procedure Replace_Slice
        (Source   : in out Bounded_String;
         Low      : Positive;
         High     : Natural;
         By       : String;
         Drop     : Truncation := Error)
      with
        Pre            =>
          Low - 1 <= Length (Source)
            and then
              (if Drop = Error
                 then (if High >= Low
                         then Low - 1
                           <= Max_Length - By'Length
                            - Natural'Max (Length (Source) - High, 0)
                         else Length (Source) <= Max_Length - By'Length)),
        Contract_Cases =>
          (Low - 1 <= Max_Length - By'Length
             - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
           =>
             --  Total length is lower than Max_Length: nothing is dropped

             --  Note that if High < Low, the insertion is done before Low,
             --  so in all cases the starting position of the slice of Source
             --  remaining after the replaced Slice is Integer'Max (High + 1,
             --  Low).

             Length (Source) = Low - 1 + By'Length + Integer'Max
               (Length (Source'Old) - Integer'Max (High, Low - 1), 0)
               and then
                 Slice (Source, 1, Low - 1) = Slice (Source'Old, 1, Low - 1)
               and then Slice (Source, Low, Low - 1 + By'Length) = By
               and then
                 (if Integer'Max (High, Low - 1) < Length (Source'Old) then
                    Slice (Source, Low + By'Length, Length (Source)) =
                      Slice (Source'Old,
                        Integer'Max (High + 1, Low), Length (Source'Old))),

           Low - 1 > Max_Length - By'Length
             - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
             and then Drop = Left
           =>
             --  Final_Slice is the length of the slice of Source remaining
             --  after the replaced part.
             (declare
                Final_Slice : constant Integer :=
                  Integer'Max (0,
                    Length (Source'Old) - Integer'Max (High, Low - 1));
              begin
                --  The result is of maximal length and ends by the last
                --  Final_Slice characters of Source.

                Length (Source) = Max_Length
                  and then
                    (if Final_Slice > 0 then
                       Slice (Source,
                         Max_Length - Final_Slice + 1, Max_Length) =
                           Slice (Source'Old,
                             Integer'Max (High + 1, Low), Length (Source'Old)))

                  --  Depending on when we reach Max_Length, either the first
                  --  part of Source is fully dropped and By is partly dropped,
                  --  or By is fully added and the first part of Source is
                  --  partly dropped.

                  and then
                    (if Max_Length - Final_Slice - By'Length <= 0 then

                       --  The first characters of By are dropped

                       (if Final_Slice < Max_Length then
                          Slice (Source, 1, Max_Length - Final_Slice) =
                            By (By'Last - Max_Length + Final_Slice + 1
                                .. By'Last))

                     else  --  By is added to the result

                       Slice (Source,
                         Max_Length - Final_Slice - By'Length + 1,
                         Max_Length - Final_Slice) = By

                         --  The first characters of Source (1 .. Low - 1) are
                         --  dropped.

                         and then Slice (Source, 1,
                           Max_Length - Final_Slice - By'Length) =
                             Slice (Source'Old,
                               Low - Max_Length + Final_Slice + By'Length,
                               Low - 1))),

           others  --  Drop = Right
           =>
             --  The result is of maximal length and starts by the first Low -
             --  1 characters of Source.

             Length (Source) = Max_Length
               and then
                 Slice (Source, 1, Low - 1) = Slice (Source'Old, 1, Low - 1)

               --  Depending on when we reach Max_Length, either the last part
               --  of Source is fully dropped and By is partly dropped, or By
               --  is fully added and the last part of Source is partly
               --  dropped.

               and then
                 (if Low - 1 >= Max_Length - By'Length then

                    --  The last characters of By are dropped

                    Slice (Source, Low, Max_Length) =
                      By (By'First .. Max_Length - Low + By'First)

                  else  --  By is fully added

                    Slice (Source, Low, Low + By'Length - 1) = By

                      --  Then Source starting from Natural'Max (High + 1, Low)
                      --  is added but the last characters are dropped.

                      and then Slice (Source, Low + By'Length, Max_Length) =
                        Slice (Source'Old, Integer'Max (High + 1, Low),
                          Integer'Max (High + 1, Low) +
                            (Max_Length - Low - By'Length))));

      function Insert
        (Source   : Bounded_String;
         Before   : Positive;
         New_Item : String;
         Drop     : Truncation := Error) return Bounded_String
      with
        Pre            =>
          Before - 1 <= Length (Source)
            and then (if New_Item'Length > Max_Length - Length (Source)
                      then Drop /= Error),
        Contract_Cases =>
          (Length (Source) <= Max_Length - New_Item'Length
           =>
             --  Total length is lower than Max_Length: nothing is dropped

             Length (Insert'Result) = Length (Source) + New_Item'Length
               and then
                 Slice (Insert'Result, 1, Before - 1) =
                   Slice (Source, 1, Before - 1)
               and then
                 Slice (Insert'Result, Before, Before - 1 + New_Item'Length) =
                   New_Item
               and then
                 (if Before <= Length (Source) then
                    Slice (Insert'Result,
                      Before + New_Item'Length, Length (Insert'Result)) =
                        Slice (Source, Before, Length (Source))),

           Length (Source) > Max_Length - New_Item'Length and then Drop = Left
           =>
             --  The result is of maximal length and ends by the last
             --  characters of Source.

             Length (Insert'Result) = Max_Length
               and then
                 (if Before <= Length (Source) then
                    Slice (Insert'Result,
                      Max_Length - Length (Source) + Before, Max_Length) =
                        Slice (Source, Before, Length (Source)))

               --  Depending on when we reach Max_Length, either the first part
               --  of Source is fully dropped and New_Item is partly dropped,
               --  or New_Item is fully added and the first part of Source is
               --  partly dropped.

               and then
                 (if Max_Length - Length (Source) - 1 + Before
                   < New_Item'Length
                  then
                    --  The first characters of New_Item are dropped

                    (if Length (Source) - Before + 1 < Max_Length then
                       Slice (Insert'Result,
                         1, Max_Length - Length (Source) - 1 + Before) =
                           New_Item
                             (New_Item'Last - Max_Length + Length (Source)
                               - Before + 2
                              .. New_Item'Last))

                  else  --  New_Item is added to the result

                    Slice (Insert'Result,
                      Max_Length - Length (Source) - New_Item'Length + Before,
                      Max_Length - Length (Source) - 1 + Before) = New_Item

                      --  The first characters of Source (1 .. Before - 1) are
                      --  dropped.

                      and then Slice (Insert'Result,
                        1, Max_Length - Length (Source) - New_Item'Length
                          - 1 + Before) =
                            Slice (Source,
                              Length (Source) - Max_Length + New_Item'Length
                                + 1,
                              Before - 1)),

           others  --  Drop = Right
           =>
             --  The result is of maximal length and starts by the first
             --  characters of Source.

             Length (Insert'Result) = Max_Length
               and then
                 Slice (Insert'Result, 1, Before - 1) =
                   Slice (Source, 1, Before - 1)

               --  Depending on when we reach Max_Length, either the last part
               --  of Source is fully dropped and New_Item is partly dropped,
               --  or New_Item is fully added and the last part of Source is
               --  partly dropped.

               and then
                 (if Before - 1 >= Max_Length - New_Item'Length then

                    --  The last characters of New_Item are dropped

                    Slice (Insert'Result, Before, Max_Length) =
                      New_Item (New_Item'First
                        .. Max_Length - Before + New_Item'First)

                  else  --  New_Item is fully added

                    Slice (Insert'Result,
                      Before, Before + New_Item'Length - 1) =
                        New_Item

                      --  Then Source starting from Before is added but the
                      --  last characters are dropped.

                      and then Slice (Insert'Result,
                        Before + New_Item'Length, Max_Length) =
                          Slice (Source,
                            Before, Max_Length - New_Item'Length)));

      procedure Insert
        (Source   : in out Bounded_String;
         Before   : Positive;
         New_Item : String;
         Drop     : Truncation := Error)
      with
        Pre            =>
          Before - 1 <= Length (Source)
            and then (if New_Item'Length > Max_Length - Length (Source)
                      then Drop /= Error),
        Contract_Cases =>
          (Length (Source) <= Max_Length - New_Item'Length
           =>
             --  Total length is lower than Max_Length: nothing is dropped

             Length (Source) = Length (Source'Old) + New_Item'Length
               and then
                 Slice (Source, 1, Before - 1) =
                   Slice (Source'Old, 1, Before - 1)
               and then
                 Slice (Source, Before, Before - 1 + New_Item'Length) =
                   New_Item
               and then
                 (if Before <= Length (Source'Old) then
                    Slice (Source, Before + New_Item'Length, Length (Source)) =
                      Slice (Source'Old, Before, Length (Source'Old))),

           Length (Source) > Max_Length - New_Item'Length and then Drop = Left
           =>
             --  The result is of maximal length and ends by the last
             --  characters of Source.

             Length (Source) = Max_Length
               and then
                 (if Before <= Length (Source'Old) then
                    Slice (Source,
                      Max_Length - Length (Source'Old) + Before, Max_Length) =
                        Slice (Source'Old, Before, Length (Source'Old)))

               --  Depending on when we reach Max_Length, either the first part
               --  of Source is fully dropped and New_Item is partly dropped,
               --  or New_Item is fully added and the first part of Source is
               --  partly dropped.

               and then
                 (if Max_Length - Length (Source'Old) - 1 + Before
                   < New_Item'Length
                  then
                    --  The first characters of New_Item are dropped

                    (if Length (Source'Old) - Before + 1 < Max_Length then
                       Slice (Source,
                         1, Max_Length - Length (Source'Old) - 1 + Before) =
                           New_Item
                             (New_Item'Last - Max_Length + Length (Source'Old)
                               - Before + 2
                              .. New_Item'Last))

                  else  --  New_Item is added to the result

                    Slice (Source,
                      Max_Length - Length (Source'Old) - New_Item'Length
                        + Before,
                      Max_Length - Length (Source'Old) - 1 + Before) = New_Item

                      --  The first characters of Source (1 .. Before - 1) are
                      --  dropped.

                      and then Slice (Source, 1,
                        Max_Length - Length (Source'Old) - New_Item'Length
                          - 1 + Before) =
                            Slice (Source'Old,
                              Length (Source'Old)
                                - Max_Length + New_Item'Length + 1,
                              Before - 1)),

           others  --  Drop = Right
           =>
             --  The result is of maximal length and starts by the first
             --  characters of Source.

             Length (Source) = Max_Length
               and then
                 Slice (Source, 1, Before - 1) =
                   Slice (Source'Old, 1, Before - 1)

               --  Depending on when we reach Max_Length, either the last part
               --  of Source is fully dropped and New_Item is partly dropped,
               --  or New_Item is fully added and the last part of Source is
               --  partly dropped.

               and then
                 (if Before - 1 >= Max_Length - New_Item'Length then

                    --  The last characters of New_Item are dropped

                    Slice (Source, Before, Max_Length) =
                      New_Item (New_Item'First
                        .. Max_Length - Before + New_Item'First)

                  else  --  New_Item is fully added

                    Slice (Source, Before, Before + New_Item'Length - 1) =
                      New_Item

                      --  Then Source starting from Before is added but the
                      --  last characters are dropped.

                      and then
                        Slice (Source, Before + New_Item'Length, Max_Length) =
                          Slice (Source'Old,
                            Before, Max_Length - New_Item'Length)));

      function Overwrite
        (Source   : Bounded_String;
         Position : Positive;
         New_Item : String;
         Drop     : Truncation := Error) return Bounded_String
      with
        Pre            =>
          Position - 1 <= Length (Source)
            and then (if New_Item'Length > Max_Length - (Position - 1)
                      then Drop /= Error),
        Contract_Cases =>
          (Position - 1 <= Max_Length - New_Item'Length
           =>
             --  The length is unchanged, unless New_Item overwrites further
             --  than the end of Source. In this contract case, we suppose
             --  New_Item doesn't overwrite further than Max_Length.

             Length (Overwrite'Result) =
               Integer'Max (Length (Source), Position - 1 + New_Item'Length)
               and then
                 Slice (Overwrite'Result, 1, Position - 1) =
                   Slice (Source, 1, Position - 1)
               and then Slice (Overwrite'Result,
                 Position, Position - 1 + New_Item'Length) =
                   New_Item
               and then
                 (if Position - 1 + New_Item'Length < Length (Source) then

                    --  There are some unchanged characters of Source remaining
                    --  after New_Item.

                    Slice (Overwrite'Result,
                      Position + New_Item'Length, Length (Source)) =
                        Slice (Source,
                          Position + New_Item'Length, Length (Source))),

           Position - 1 > Max_Length - New_Item'Length and then Drop = Left
           =>
             Length (Overwrite'Result) = Max_Length

               --  If a part of the result has to be dropped, it means New_Item
               --  is overwriting further than the end of Source. Thus the
               --  result is necessarily ending by New_Item. However, we don't
               --  know whether New_Item covers all Max_Length characters or
               --  some characters of Source are remaining at the left.

               and then
                 (if New_Item'Length >= Max_Length then

                    --  New_Item covers all Max_Length characters

                    To_String (Overwrite'Result) =
                      New_Item
                        (New_Item'Last - Max_Length + 1 .. New_Item'Last)
                  else
                    --  New_Item fully appears at the end

                    Slice (Overwrite'Result,
                      Max_Length - New_Item'Length + 1, Max_Length) =
                        New_Item

                      --  The left of Source is cut

                      and then
                        Slice (Overwrite'Result,
                          1, Max_Length - New_Item'Length) =
                            Slice (Source,
                              Position - Max_Length + New_Item'Length,
                              Position - 1)),

           others  --  Drop = Right
           =>
             --  The result is of maximal length and starts by the first
             --  characters of Source.

             Length (Overwrite'Result) = Max_Length
               and then
                 Slice (Overwrite'Result, 1, Position - 1) =
                   Slice (Source, 1, Position - 1)

               --  Then New_Item is written until Max_Length

               and then Slice (Overwrite'Result, Position, Max_Length) =
                 New_Item
                   (New_Item'First .. Max_Length - Position + New_Item'First));

      procedure Overwrite
        (Source    : in out Bounded_String;
         Position  : Positive;
         New_Item  : String;
         Drop      : Truncation := Error)
      with
        Pre            =>
          Position - 1 <= Length (Source)
            and then (if New_Item'Length > Max_Length - (Position - 1)
                      then Drop /= Error),
        Contract_Cases =>
          (Position - 1 <= Max_Length - New_Item'Length
           =>
             --  The length of Source is unchanged, unless New_Item overwrites
             --  further than the end of Source. In this contract case, we
             --  suppose New_Item doesn't overwrite further than Max_Length.

             Length (Source) = Integer'Max
               (Length (Source'Old), Position - 1 + New_Item'Length)
               and then
                 Slice (Source, 1, Position - 1) =
                   Slice (Source'Old, 1, Position - 1)
               and then Slice (Source,
                 Position, Position - 1 + New_Item'Length) =
                   New_Item
               and then
                 (if Position - 1 + New_Item'Length < Length (Source'Old) then

                    --  There are some unchanged characters of Source remaining
                    --  after New_Item.

                    Slice (Source,
                      Position + New_Item'Length, Length (Source'Old)) =
                        Slice (Source'Old,
                          Position + New_Item'Length, Length (Source'Old))),

           Position - 1 > Max_Length - New_Item'Length and then Drop = Left
           =>
             Length (Source) = Max_Length

               --  If a part of the result has to be dropped, it means New_Item
               --  is overwriting further than the end of Source. Thus the
               --  result is necessarily ending by New_Item. However, we don't
               --  know whether New_Item covers all Max_Length characters or
               --  some characters of Source are remaining at the left.

               and then
                 (if New_Item'Length >= Max_Length then

                    --  New_Item covers all Max_Length characters

                    To_String (Source) =
                      New_Item
                        (New_Item'Last - Max_Length + 1 .. New_Item'Last)
                  else
                    --  New_Item fully appears at the end

                    Slice (Source,
                      Max_Length - New_Item'Length + 1, Max_Length) =
                        New_Item

                      --  The left of Source is cut

                      and then
                        Slice (Source, 1, Max_Length - New_Item'Length) =
                          Slice (Source'Old,
                            Position - Max_Length + New_Item'Length,
                            Position - 1)),

           others  --  Drop = Right
           =>
             --  The result is of maximal length and starts by the first
             --  characters of Source.

             Length (Source) = Max_Length
               and then
                 Slice (Source, 1, Position - 1) =
                   Slice (Source'Old, 1, Position - 1)

               --  New_Item is written until Max_Length

               and then Slice (Source, Position, Max_Length) =
                 New_Item
                   (New_Item'First .. Max_Length - Position + New_Item'First));

      function Delete
        (Source  : Bounded_String;
         From    : Positive;
         Through : Natural) return Bounded_String
      with
        Pre            =>
          (if Through >= From then From - 1 <= Length (Source)),
        Contract_Cases =>
          (Through >= From =>
             Length (Delete'Result) =
               From - 1 + Natural'Max (Length (Source) - Through, 0)
               and then
                 Slice (Delete'Result, 1, From - 1) =
                   Slice (Source, 1, From - 1)
               and then
                 (if Through < Length (Source) then
                    Slice (Delete'Result, From, Length (Delete'Result)) =
                      Slice (Source, Through + 1, Length (Source))),
           others          =>
             Delete'Result = Source),
        Global         => null;

      procedure Delete
        (Source  : in out Bounded_String;
         From    : Positive;
         Through : Natural)
      with
        Pre            =>
          (if Through >= From then From - 1 <= Length (Source)),
        Contract_Cases =>
          (Through >= From =>
             Length (Source) =
               From - 1 + Natural'Max (Length (Source'Old) - Through, 0)
               and then
                 Slice (Source, 1, From - 1) = Slice (Source'Old, 1, From - 1)
               and then
                 (if Through < Length (Source) then
                    Slice (Source, From, Length (Source)) =
                      Slice (Source'Old, Through + 1, Length (Source'Old))),
           others          =>
             Source = Source'Old),
        Global         => null;

      ---------------------------------
      -- String Selector Subprograms --
      ---------------------------------

      function Trim
        (Source : Bounded_String;
         Side   : Trim_End) return Bounded_String
      with
        Contract_Cases =>
          --  If all characters in Source are Space, the returned string is
          --  empty.

          ((for all C of To_String (Source) => C = ' ')
           =>
             Length (Trim'Result) = 0,

           --  Otherwise, the returned string is a slice of Source

           others
           =>
             (declare
                Low  : constant Positive :=
                  (if Side = Right then 1
                   else Index_Non_Blank (Source, Forward));
                High : constant Positive :=
                  (if Side = Left then Length (Source)
                   else Index_Non_Blank (Source, Backward));
              begin
                To_String (Trim'Result) = Slice (Source, Low, High))),
        Global         => null;

      procedure Trim
        (Source : in out Bounded_String;
         Side   : Trim_End)
      with
        Contract_Cases =>
          --  If all characters in Source are Space, the returned string is
          --  empty.

          ((for all C of To_String (Source) => C = ' ')
           =>
             Length (Source) = 0,

           --  Otherwise, the returned string is a slice of Source

           others
           =>
             (declare
                Low  : constant Positive :=
                  (if Side = Right then 1
                   else Index_Non_Blank (Source'Old, Forward));
                High : constant Positive :=
                  (if Side = Left then Length (Source'Old)
                   else Index_Non_Blank (Source'Old, Backward));
              begin
                To_String (Source) = Slice (Source'Old, Low, High))),
        Global         => null;

      function Trim
        (Source : Bounded_String;
         Left   : Maps.Character_Set;
         Right  : Maps.Character_Set) return Bounded_String
      with
        Contract_Cases =>
          --  If all characters in Source are contained in one of the sets Left
          --  or Right, then the returned string is empty.

          ((for all C of To_String (Source) => Maps.Is_In (C, Left))
             or else
               (for all C of To_String (Source) => Maps.Is_In (C, Right))
           =>
             Length (Trim'Result) = 0,

           --  Otherwise, the returned string is a slice of Source

           others
           =>
             (declare
                Low  : constant Positive :=
                  Index (Source, Left, Outside, Forward);
                High : constant Positive :=
                  Index (Source, Right, Outside, Backward);
              begin
                To_String (Trim'Result) = Slice (Source, Low, High))),
        Global         => null;

      procedure Trim
        (Source : in out Bounded_String;
         Left   : Maps.Character_Set;
         Right  : Maps.Character_Set)
      with
        Contract_Cases =>
          --  If all characters in Source are contained in one of the sets Left
          --  or Right, then the returned string is empty.

          ((for all C of To_String (Source) => Maps.Is_In (C, Left))
             or else
               (for all C of To_String (Source) => Maps.Is_In (C, Right))
           =>
             Length (Source) = 0,

           --  Otherwise, the returned string is a slice of Source

           others
           =>
             (declare
                Low  : constant Positive :=
                  Index (Source'Old, Left, Outside, Forward);
                High : constant Positive :=
                  Index (Source'Old, Right, Outside, Backward);
              begin
                To_String (Source) = Slice (Source'Old, Low, High))),
        Global         => null;

      function Head
        (Source : Bounded_String;
         Count  : Natural;
         Pad    : Character := Space;
         Drop   : Truncation := Error) return Bounded_String
      with
        Pre            => (if Count > Max_Length then Drop /= Error),
        Contract_Cases =>
          (Count <= Length (Source)
           =>
             --  Source is cut

             To_String (Head'Result) = Slice (Source, 1, Count),

           Count > Length (Source) and then Count <= Max_Length
           =>
             --  Source is followed by Pad characters

             Length (Head'Result) = Count
               and then
                 Slice (Head'Result, 1, Length (Source)) = To_String (Source)
               and then
                 Slice (Head'Result, Length (Source) + 1, Count) =
                   [1 .. Count - Length (Source) => Pad],

           Count > Max_Length and then Drop = Right
           =>
             --  Source is followed by Pad characters

             Length (Head'Result) = Max_Length
               and then
                 Slice (Head'Result, 1, Length (Source)) = To_String (Source)
               and then
                 Slice (Head'Result, Length (Source) + 1, Max_Length) =
                   [1 .. Max_Length - Length (Source) => Pad],

           Count - Length (Source) > Max_Length and then Drop = Left
           =>
             --  Source is fully dropped at the left

             To_String (Head'Result) = [1 .. Max_Length => Pad],

           others
           =>
             --  Source is partly dropped at the left

             Length (Head'Result) = Max_Length
               and then
                 Slice (Head'Result, 1, Max_Length - Count + Length (Source)) =
                   Slice (Source, Count - Max_Length + 1, Length (Source))
               and then
                 Slice (Head'Result,
                   Max_Length - Count + Length (Source) + 1, Max_Length) =
                     [1 .. Count - Length (Source) => Pad]);

      procedure Head
        (Source : in out Bounded_String;
         Count  : Natural;
         Pad    : Character  := Space;
         Drop   : Truncation := Error)
      with
        Pre            => (if Count > Max_Length then Drop /= Error),
        Contract_Cases =>
          (Count <= Length (Source)
           =>
             --  Source is cut

             To_String (Source) = Slice (Source'Old, 1, Count),

           Count > Length (Source) and then Count <= Max_Length
           =>
             --  Source is followed by Pad characters

             Length (Source) = Count
               and then
                 Slice (Source, 1, Length (Source'Old)) =
                   To_String (Source'Old)
               and then
                 Slice (Source, Length (Source'Old) + 1, Count) =
                   [1 .. Count - Length (Source'Old) => Pad],

           Count > Max_Length and then Drop = Right
           =>
             --  Source is followed by Pad characters

             Length (Source) = Max_Length
               and then
                 Slice (Source, 1, Length (Source'Old)) =
                   To_String (Source'Old)
               and then
                 Slice (Source, Length (Source'Old) + 1, Max_Length) =
                   [1 .. Max_Length - Length (Source'Old) => Pad],

           Count - Length (Source) > Max_Length and then Drop = Left
           =>
             --  Source is fully dropped on the left

             To_String (Source) = [1 .. Max_Length => Pad],

           others
           =>
             --  Source is partly dropped on the left

             Length (Source) = Max_Length
               and then
                 Slice (Source, 1, Max_Length - Count + Length (Source'Old)) =
                   Slice (Source'Old,
                     Count - Max_Length + 1, Length (Source'Old))
               and then
                 Slice (Source,
                   Max_Length - Count + Length (Source'Old) + 1, Max_Length) =
                     [1 .. Count - Length (Source'Old) => Pad]);

      function Tail
        (Source : Bounded_String;
         Count  : Natural;
         Pad    : Character  := Space;
         Drop   : Truncation := Error) return Bounded_String
      with
        Pre            => (if Count > Max_Length then Drop /= Error),
        Contract_Cases =>
          (Count < Length (Source)
           =>
             --  Source is cut

             (if Count > 0 then
                To_String (Tail'Result) =
                  Slice (Source, Length (Source) - Count + 1, Length (Source))
              else Length (Tail'Result) = 0),

           Count >= Length (Source) and then Count < Max_Length
           =>
             --  Source is preceded by Pad characters

             Length (Tail'Result) = Count
               and then
                 Slice (Tail'Result, 1, Count - Length (Source)) =
                   [1 .. Count - Length (Source) => Pad]
               and then
                 Slice (Tail'Result, Count - Length (Source) + 1, Count) =
                   To_String (Source),

           Count >= Max_Length and then Drop = Left
           =>
             --  Source is preceded by Pad characters

             Length (Tail'Result) = Max_Length
               and then
                 Slice (Tail'Result, 1, Max_Length - Length (Source)) =
                   [1 .. Max_Length - Length (Source) => Pad]
               and then
                 (if Length (Source) > 0 then
                    Slice (Tail'Result,
                      Max_Length - Length (Source) + 1, Max_Length) =
                        To_String (Source)),

           Count - Length (Source) >= Max_Length and then Drop /= Left
           =>
             --  Source is fully dropped on the right

             To_String (Tail'Result) = [1 .. Max_Length => Pad],

           others
           =>
             --  Source is partly dropped on the right

             Length (Tail'Result) = Max_Length
               and then
                 Slice (Tail'Result, 1, Count - Length (Source)) =
                   [1 .. Count - Length (Source) => Pad]
               and then
                 Slice (Tail'Result, Count - Length (Source) + 1, Max_Length) =
                   Slice (Source, 1, Max_Length - Count + Length (Source)));

      procedure Tail
        (Source : in out Bounded_String;
         Count  : Natural;
         Pad    : Character  := Space;
         Drop   : Truncation := Error)
      with
        Pre            => (if Count > Max_Length then Drop /= Error),
        Contract_Cases =>
          (Count < Length (Source)
           =>
             --  Source is cut

             (if Count > 0 then
                To_String (Source) =
                  Slice (Source'Old,
                    Length (Source'Old) - Count + 1, Length (Source'Old))
              else Length (Source) = 0),

           Count >= Length (Source) and then Count < Max_Length
           =>
             --  Source is preceded by Pad characters

             Length (Source) = Count
               and then
                 Slice (Source, 1, Count - Length (Source'Old)) =
                   [1 .. Count - Length (Source'Old) => Pad]
               and then
                 Slice (Source, Count - Length (Source'Old) + 1, Count) =
                   To_String (Source'Old),

           Count >= Max_Length and then Drop = Left
           =>
             --  Source is preceded by Pad characters

             Length (Source) = Max_Length
               and then
                 Slice (Source, 1, Max_Length - Length (Source'Old)) =
                   [1 .. Max_Length - Length (Source'Old) => Pad]
               and then
                 (if Length (Source'Old) > 0 then
                    Slice (Source,
                      Max_Length - Length (Source'Old) + 1, Max_Length) =
                        To_String (Source'Old)),

           Count - Length (Source) >= Max_Length and then Drop /= Left
           =>
             --  Source is fully dropped at the right

             To_String (Source) = [1 .. Max_Length => Pad],

           others
           =>
             --  Source is partly dropped at the right

             Length (Source) = Max_Length
               and then
                 Slice (Source, 1, Count - Length (Source'Old)) =
                   [1 .. Count - Length (Source'Old) => Pad]
               and then
                 Slice (Source, Count - Length (Source'Old) + 1, Max_Length) =
                   Slice (Source'Old,
                     1, Max_Length - Count + Length (Source'Old)));

      ------------------------------------
      -- String Constructor Subprograms --
      ------------------------------------

      function "*"
        (Left  : Natural;
         Right : Character) return Bounded_String
      with
        Pre  => Left <= Max_Length,
        Post => To_String ("*"'Result) = [1 .. Left => Right];

      function "*"
        (Left  : Natural;
         Right : String) return Bounded_String
      with
        Pre  => (if Left /= 0 then Right'Length <= Max_Length / Left),
        Post =>
          Length ("*"'Result) = Left * Right'Length
            and then
              (if Right'Length > 0 then
                 (for all K in 1 .. Left * Right'Length =>
                    Element ("*"'Result, K) =
                      Right (Right'First + (K - 1) mod Right'Length)));

      function "*"
        (Left  : Natural;
         Right : Bounded_String) return Bounded_String
      with
        Pre  => (if Left /= 0 then Length (Right) <= Max_Length / Left),
        Post =>
          Length ("*"'Result) = Left * Length (Right)
            and then
              (if Length (Right) > 0 then
                 (for all K in 1 .. Left * Length (Right) =>
                    Element ("*"'Result, K) =
                      Element (Right, 1 + (K - 1) mod Length (Right))));

      function Replicate
        (Count : Natural;
         Item  : Character;
         Drop  : Truncation := Error) return Bounded_String
      with
        Pre  => (if Count > Max_Length then Drop /= Error),
        Post =>
          To_String (Replicate'Result) =
            [1 .. Natural'Min (Max_Length, Count) => Item];

      function Replicate
        (Count : Natural;
         Item  : String;
         Drop  : Truncation := Error) return Bounded_String
      with
        Pre            =>
          (if Count /= 0 and then Item'Length > Max_Length / Count
           then Drop /= Error),
        Contract_Cases =>
          (Count = 0 or else Item'Length <= Max_Length / Count
           =>
             Length (Replicate'Result) = Count * Item'Length
               and then
                 (if Item'Length > 0 then
                    (for all K in 1 .. Count * Item'Length =>
                       Element (Replicate'Result, K) =
                         Item (Item'First + (K - 1) mod Item'Length))),
           Count /= 0
             and then Item'Length > Max_Length / Count
             and then Drop = Right
           =>
             Length (Replicate'Result) = Max_Length
               and then
                 (for all K in 1 .. Max_Length =>
                    Element (Replicate'Result, K) =
                      Item (Item'First + (K - 1) mod Item'Length)),
           others  --  Drop = Left
           =>
             Length (Replicate'Result) = Max_Length
               and then
                 (for all K in 1 .. Max_Length =>
                    Element (Replicate'Result, K) =
                      Item (Item'Last - (Max_Length - K) mod Item'Length)));

      function Replicate
        (Count : Natural;
         Item  : Bounded_String;
         Drop  : Truncation := Error) return Bounded_String
      with
        Pre            =>
          (if Count /= 0 and then Length (Item) > Max_Length / Count
           then Drop /= Error),
        Contract_Cases =>
          ((if Count /= 0 then Length (Item) <= Max_Length / Count)
           =>
             Length (Replicate'Result) = Count * Length (Item)
               and then
                 (if Length (Item) > 0 then
                    (for all K in 1 .. Count * Length (Item) =>
                       Element (Replicate'Result, K) =
                         Element (Item, 1 + (K - 1) mod Length (Item)))),
           Count /= 0
             and then Length (Item) > Max_Length / Count
             and then Drop = Right
           =>
             Length (Replicate'Result) = Max_Length
               and then
                 (for all K in 1 .. Max_Length =>
                    Element (Replicate'Result, K) =
                      Element (Item, 1 + (K - 1) mod Length (Item))),
           others  --  Drop = Left
           =>
             Length (Replicate'Result) = Max_Length
               and then
                 (for all K in 1 .. Max_Length =>
                    Element (Replicate'Result, K) =
                      Element (Item,
                        Length (Item) - (Max_Length - K) mod Length (Item))));

   private
      --  Most of the implementation is in the separate non generic package
      --  Ada.Strings.Superbounded. Type Bounded_String is derived from type
      --  Superbounded.Super_String with the maximum length constraint. In
      --  almost all cases, the routines in Superbounded can be called with
      --  no requirement to pass the maximum length explicitly, since there
      --  is at least one Bounded_String argument from which the maximum
      --  length can be obtained. For all such routines, the implementation
      --  in this private part is simply a renaming of the corresponding
      --  routine in the superbounded package.

      --  The five exceptions are the * and Replicate routines operating on
      --  character values. For these cases, we have a routine in the body
      --  that calls the superbounded routine passing the maximum length
      --  explicitly as an extra parameter.

      type Bounded_String is new Superbounded.Super_String (Max_Length);
      --  Deriving Bounded_String from Superbounded.Super_String is the
      --  real trick, it ensures that the type Bounded_String declared in
      --  the generic instantiation is compatible with the Super_String
      --  type declared in the Superbounded package.

      function From_String (Source : String) return Bounded_String
      with Pre => Source'Length <= Max_Length;
      --  Private routine used only by Stream_Convert

      pragma Stream_Convert (Bounded_String, From_String, To_String);
      --  Provide stream routines without dragging in Ada.Streams

      Null_Bounded_String : constant Bounded_String :=
                              (Max_Length     => Max_Length,
                               Current_Length => 0,
                               Data           =>
                                 [1 .. Max_Length => ASCII.NUL]);

      pragma Inline (To_Bounded_String);

      procedure Set_Bounded_String
        (Target : out Bounded_String;
         Source : String;
         Drop   : Truncation := Error)
         renames Set_Super_String;

      function Length
        (Source : Bounded_String) return Length_Range
         renames Super_Length;

      function To_String
        (Source : Bounded_String) return String
         renames Super_To_String;

      function Append
        (Left  : Bounded_String;
         Right : Bounded_String;
         Drop  : Truncation  := Error) return Bounded_String
         renames Super_Append;

      function Append
        (Left  : Bounded_String;
         Right : String;
         Drop  : Truncation := Error) return Bounded_String
         renames Super_Append;

      function Append
        (Left  : String;
         Right : Bounded_String;
         Drop  : Truncation := Error) return Bounded_String
         renames Super_Append;

      function Append
        (Left  : Bounded_String;
         Right : Character;
         Drop  : Truncation := Error) return Bounded_String
         renames Super_Append;

      function Append
        (Left  : Character;
         Right : Bounded_String;
         Drop  : Truncation := Error) return Bounded_String
         renames Super_Append;

      procedure Append
        (Source   : in out Bounded_String;
         New_Item : Bounded_String;
         Drop     : Truncation  := Error)
         renames Super_Append;

      procedure Append
        (Source   : in out Bounded_String;
         New_Item : String;
         Drop     : Truncation  := Error)
         renames Super_Append;

      procedure Append
        (Source   : in out Bounded_String;
         New_Item : Character;
         Drop     : Truncation  := Error)
         renames Super_Append;

      function "&"
        (Left  : Bounded_String;
         Right : Bounded_String) return Bounded_String
         renames Concat;

      function "&"
        (Left  : Bounded_String;
         Right : String) return Bounded_String
         renames Concat;

      function "&"
        (Left  : String;
         Right : Bounded_String) return Bounded_String
         renames Concat;

      function "&"
        (Left  : Bounded_String;
         Right : Character) return Bounded_String
         renames Concat;

      function "&"
        (Left  : Character;
         Right : Bounded_String) return Bounded_String
         renames Concat;

      function Element
        (Source : Bounded_String;
         Index  : Positive) return Character
         renames Super_Element;

      procedure Replace_Element
        (Source : in out Bounded_String;
         Index  : Positive;
         By     : Character)
         renames Super_Replace_Element;

      function Slice
        (Source : Bounded_String;
         Low    : Positive;
         High   : Natural) return String
         renames Super_Slice;

      function Bounded_Slice
        (Source : Bounded_String;
         Low    : Positive;
         High   : Natural) return Bounded_String
         renames Super_Slice;

      procedure Bounded_Slice
        (Source : Bounded_String;
         Target : out Bounded_String;
         Low    : Positive;
         High   : Natural)
         renames Super_Slice;

      overriding function "="
        (Left  : Bounded_String;
         Right : Bounded_String) return Boolean
         renames Equal;

      function "="
        (Left  : Bounded_String;
         Right : String) return Boolean
         renames Equal;

      function "="
        (Left  : String;
         Right : Bounded_String) return Boolean
         renames Equal;

      function "<"
        (Left  : Bounded_String;
         Right : Bounded_String) return Boolean
         renames Less;

      function "<"
        (Left  : Bounded_String;
         Right : String) return Boolean
         renames Less;

      function "<"
        (Left  : String;
         Right : Bounded_String) return Boolean
         renames Less;

      function "<="
        (Left  : Bounded_String;
         Right : Bounded_String) return Boolean
         renames Less_Or_Equal;

      function "<="
        (Left  : Bounded_String;
         Right : String) return Boolean
         renames Less_Or_Equal;

      function "<="
        (Left  : String;
         Right : Bounded_String) return Boolean
         renames Less_Or_Equal;

      function ">"
        (Left  : Bounded_String;
         Right : Bounded_String) return Boolean
         renames Greater;

      function ">"
        (Left  : Bounded_String;
         Right : String) return Boolean
         renames Greater;

      function ">"
        (Left  : String;
         Right : Bounded_String) return Boolean
         renames Greater;

      function ">="
        (Left  : Bounded_String;
         Right : Bounded_String) return Boolean
         renames Greater_Or_Equal;

      function ">="
        (Left  : Bounded_String;
         Right : String) return Boolean
         renames Greater_Or_Equal;

      function ">="
        (Left  : String;
         Right : Bounded_String) return Boolean
         renames Greater_Or_Equal;

      function Index
        (Source  : Bounded_String;
         Pattern : String;
         Going   : Direction := Forward;
         Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
         renames Super_Index;

      function Index
        (Source  : Bounded_String;
         Pattern : String;
         Going   : Direction := Forward;
         Mapping : Maps.Character_Mapping_Function) return Natural
         renames Super_Index;

      function Index
        (Source : Bounded_String;
         Set    : Maps.Character_Set;
         Test   : Membership := Inside;
         Going  : Direction  := Forward) return Natural
         renames Super_Index;

      function Index
        (Source  : Bounded_String;
         Pattern : String;
         From    : Positive;
         Going   : Direction := Forward;
         Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
         renames Super_Index;

      function Index
        (Source  : Bounded_String;
         Pattern : String;
         From    : Positive;
         Going   : Direction := Forward;
         Mapping : Maps.Character_Mapping_Function) return Natural
      renames Super_Index;

      function Index
        (Source  : Bounded_String;
         Set     : Maps.Character_Set;
         From    : Positive;
         Test    : Membership := Inside;
         Going   : Direction := Forward) return Natural
      renames Super_Index;

      function Index_Non_Blank
        (Source : Bounded_String;
         Going  : Direction := Forward) return Natural
         renames Super_Index_Non_Blank;

      function Index_Non_Blank
        (Source : Bounded_String;
         From   : Positive;
         Going  : Direction := Forward) return Natural
         renames Super_Index_Non_Blank;

      function Count
        (Source  : Bounded_String;
         Pattern : String;
         Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
         renames Super_Count;

      function Count
        (Source  : Bounded_String;
         Pattern : String;
         Mapping : Maps.Character_Mapping_Function) return Natural
         renames Super_Count;

      function Count
        (Source : Bounded_String;
         Set    : Maps.Character_Set) return Natural
         renames Super_Count;

      procedure Find_Token
        (Source : Bounded_String;
         Set    : Maps.Character_Set;
         From   : Positive;
         Test   : Membership;
         First  : out Positive;
         Last   : out Natural)
         renames Super_Find_Token;

      procedure Find_Token
        (Source : Bounded_String;
         Set    : Maps.Character_Set;
         Test   : Membership;
         First  : out Positive;
         Last   : out Natural)
         renames Super_Find_Token;

      function Translate
        (Source  : Bounded_String;
         Mapping : Maps.Character_Mapping) return Bounded_String
         renames Super_Translate;

      procedure Translate
        (Source   : in out Bounded_String;
         Mapping  : Maps.Character_Mapping)
         renames Super_Translate;

      function Translate
        (Source  : Bounded_String;
         Mapping : Maps.Character_Mapping_Function) return Bounded_String
         renames Super_Translate;

      procedure Translate
        (Source  : in out Bounded_String;
         Mapping : Maps.Character_Mapping_Function)
         renames Super_Translate;

      function Replace_Slice
        (Source : Bounded_String;
         Low    : Positive;
         High   : Natural;
         By     : String;
         Drop   : Truncation := Error) return Bounded_String
         renames Super_Replace_Slice;

      procedure Replace_Slice
        (Source   : in out Bounded_String;
         Low      : Positive;
         High     : Natural;
         By       : String;
         Drop     : Truncation := Error)
         renames Super_Replace_Slice;

      function Insert
        (Source   : Bounded_String;
         Before   : Positive;
         New_Item : String;
         Drop     : Truncation := Error) return Bounded_String
         renames Super_Insert;

      procedure Insert
        (Source   : in out Bounded_String;
         Before   : Positive;
         New_Item : String;
         Drop     : Truncation := Error)
         renames Super_Insert;

      function Overwrite
        (Source   : Bounded_String;
         Position : Positive;
         New_Item : String;
         Drop     : Truncation := Error) return Bounded_String
         renames Super_Overwrite;

      procedure Overwrite
        (Source    : in out Bounded_String;
         Position  : Positive;
         New_Item  : String;
         Drop      : Truncation := Error)
         renames Super_Overwrite;

      function Delete
        (Source  : Bounded_String;
         From    : Positive;
         Through : Natural) return Bounded_String
         renames Super_Delete;

      procedure Delete
        (Source  : in out Bounded_String;
         From    : Positive;
         Through : Natural)
         renames Super_Delete;

      function Trim
        (Source : Bounded_String;
         Side   : Trim_End) return Bounded_String
         renames Super_Trim;

      procedure Trim
        (Source : in out Bounded_String;
         Side   : Trim_End)
         renames Super_Trim;

      function Trim
        (Source : Bounded_String;
         Left   : Maps.Character_Set;
         Right  : Maps.Character_Set) return Bounded_String
         renames Super_Trim;

      procedure Trim
        (Source : in out Bounded_String;
         Left   : Maps.Character_Set;
         Right  : Maps.Character_Set)
         renames Super_Trim;

      function Head
        (Source : Bounded_String;
         Count  : Natural;
         Pad    : Character := Space;
         Drop   : Truncation := Error) return Bounded_String
         renames Super_Head;

      procedure Head
        (Source : in out Bounded_String;
         Count  : Natural;
         Pad    : Character  := Space;
         Drop   : Truncation := Error)
         renames Super_Head;

      function Tail
        (Source : Bounded_String;
         Count  : Natural;
         Pad    : Character  := Space;
         Drop   : Truncation := Error) return Bounded_String
         renames Super_Tail;

      procedure Tail
        (Source : in out Bounded_String;
         Count  : Natural;
         Pad    : Character  := Space;
         Drop   : Truncation := Error)
         renames Super_Tail;

      function "*"
        (Left  : Natural;
         Right : Bounded_String) return Bounded_String
         renames Times;

      function Replicate
        (Count : Natural;
         Item  : Bounded_String;
         Drop  : Truncation := Error) return Bounded_String
         renames Super_Replicate;

   end Generic_Bounded_Length;

end Ada.Strings.Bounded;