gnat_riscv64_elf_13.2.1_938f208c/riscv64-elf/lib/gnat/light-rv32imac/gnat/a-strfix.ads

------------------------------------------------------------------------------
--                                                                          --
--                         GNAT RUN-TIME COMPONENTS                         --
--                                                                          --
--                    A D A . S T R I N G S . F I X E D                     --
--                                                                          --
--                                 S p e c                                  --
--                                                                          --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT.  In accordance with the copyright of that document, you can freely --
-- copy and modify this specification,  provided that if you redistribute a --
-- modified version,  any changes that you have made are clearly indicated. --
--                                                                          --
------------------------------------------------------------------------------

--  The language-defined package Strings.Fixed provides string-handling
--  subprograms for fixed-length strings; that is, for values of type
--  Standard.String. Several of these subprograms are procedures that modify
--  the contents of a String that is passed as an out or an in out parameter;
--  each has additional parameters to control the effect when the logical
--  length of the result differs from the parameter's length.
--
--  For each function that returns a String, the lower bound of the returned
--  value is 1.
--
--  The basic model embodied in the package is that a fixed-length string
--  comprises significant characters and possibly padding (with space
--  characters) on either or both ends. When a shorter string is copied to a
--  longer string, padding is inserted, and when a longer string is copied to a
--  shorter one, padding is stripped. The Move procedure in Strings.Fixed,
--  which takes a String as an out parameter, allows the programmer to control
--  these effects. Similar control is provided by the string transformation
--  procedures.

--  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);

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

package Ada.Strings.Fixed with SPARK_Mode is
   pragma Preelaborate;

   --------------------------------------------------------------
   -- Copy Procedure for Strings of Possibly Different Lengths --
   --------------------------------------------------------------

   procedure Move
     (Source  : String;
      Target  : out String;
      Drop    : Truncation := Error;
      Justify : Alignment  := Left;
      Pad     : Character  := Space)
   with

     --  Incomplete contract

     Global   => null,
     Annotate => (GNATprove, Might_Not_Return);
   --  The Move procedure copies characters from Source to Target. If Source
   --  has the same length as Target, then the effect is to assign Source to
   --  Target. If Source is shorter than Target then:
   --
   --  * If Justify=Left, then Source is copied into the first Source'Length
   --    characters of Target.
   --
   --  * If Justify=Right, then Source is copied into the last Source'Length
   --    characters of Target.
   --
   --  * If Justify=Center, then Source is copied into the middle Source'Length
   --    characters of Target. In this case, if the difference in length
   --    between Target and Source is odd, then the extra Pad character is on
   --    the right.
   --
   --  * Pad is copied to each Target character not otherwise assigned.
   --
   --  If Source is longer than Target, then the effect is based on Drop.
   --
   --  * If Drop=Left, then the rightmost Target'Length characters of Source
   --    are copied into Target.
   --
   --  * If Drop=Right, then the leftmost Target'Length characters of Source
   --    are copied into Target.
   --
   --  * If Drop=Error, then the effect depends on the value of the Justify
   --    parameter and also on whether any characters in Source other than Pad
   --    would fail to be copied:
   --
   --    * If Justify=Left, and if each of the rightmost
   --      Source'Length-Target'Length characters in Source is Pad, then the
   --      leftmost Target'Length characters of Source are copied to Target.
   --
   --    * If Justify=Right, and if each of the leftmost
   --      Source'Length-Target'Length characters in Source is Pad, then the
   --      rightmost Target'Length characters of Source are copied to Target.
   --
   --    * Otherwise, Length_Error is propagated.

   ------------------------
   -- Search Subprograms --
   ------------------------

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

     Post           => Index'Result in 0 | Source'Range,
     Contract_Cases =>

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

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

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

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

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

            --  The slice beginning at the returned index matches Pattern

            and then
              Ada.Strings.Search.Match (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 Source'Range =>
                 (if (if Going = Forward
                      then J in From .. Index'Result - 1
                      else J - 1 in Index'Result
                                    .. From - Pattern'Length)
                  then not (Ada.Strings.Search.Match
                              (Source, Pattern, Mapping, J)))),

        --  Otherwise, 0 is returned

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

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

     Post           => Index'Result in 0 | Source'Range,
     Contract_Cases =>

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

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

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

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

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

          --  The slice beginning at the returned index matches Pattern

          and then
            Ada.Strings.Search.Match (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 Source'Range =>
                 (if (if Going = Forward
                      then J in From .. Index'Result - 1
                      else J - 1 in Index'Result
                                    .. From - Pattern'Length)
                  then not (Ada.Strings.Search.Match
                              (Source, Pattern, Mapping, J)))),

        --  Otherwise, 0 is returned

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

   --  Each Index function searches, starting from From, for a slice of
   --  Source, with length Pattern'Length, that matches Pattern with respect to
   --  Mapping; the parameter Going indicates the direction of the lookup. If
   --  Source is the null string, Index returns 0; otherwise, if From is not in
   --  Source'Range, then Index_Error is propagated. If Going = Forward, then
   --  Index returns the smallest index I which is greater than or equal to
   --  From such that the slice of Source starting at I matches Pattern. If
   --  Going = Backward, then Index returns the largest index I such that the
   --  slice of Source starting at I matches Pattern and has an upper bound
   --  less than or equal to From. If there is no such slice, then 0 is
   --  returned. If Pattern is the null string, then Pattern_Error is
   --  propagated.

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

     Post           => Index'Result in 0 | Source'Range,
     Contract_Cases =>

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

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

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

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

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

            --  The slice beginning at the returned index matches Pattern

            and then
              Ada.Strings.Search.Match (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 Source'Range =>
                 (if (if Going = Forward
                      then J <= Index'Result - 1
                      else J - 1 in Index'Result
                                    .. Source'Last - Pattern'Length)
                  then not (Ada.Strings.Search.Match
                              (Source, Pattern, Mapping, J)))),

        --  Otherwise, 0 is returned

        others
        =>
          Index'Result = 0),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);

   function Index
     (Source  : 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 in 0 | Source'Range,
     Contract_Cases =>

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

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

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

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

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

          --  The slice beginning at the returned index matches Pattern

          and then
            Ada.Strings.Search.Match (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 Source'Range =>
                 (if (if Going = Forward
                      then J <= Index'Result - 1
                      else J - 1 in Index'Result
                                    .. Source'Last - Pattern'Length)
                  then not (Ada.Strings.Search.Match
                              (Source, Pattern, Mapping, J)))),

        --  Otherwise, 0 is returned

        others
        =>
          Index'Result = 0),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);

   --  If Going = Forward, returns:
   --
   --     Index (Source, Pattern, Source'First, Forward, Mapping)
   --
   --  otherwise, returns:
   --
   --     Index (Source, Pattern, Source'Last, Backward, Mapping).

   function Index
     (Source : String;
      Set    : Maps.Character_Set;
      Test   : Membership := Inside;
      Going  : Direction  := Forward) return Natural
   with
     Post           => Index'Result in 0 | Source'Range,
     Contract_Cases =>

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

       ((for all C of Source =>
           (Test = Inside) /= Ada.Strings.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 Source'Range

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

            and then
              (Test = Inside)
              = Ada.Strings.Maps.Is_In (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 Source'Range =>
                 (if J /= Index'Result
                       and then (J < Index'Result) = (Going = Forward)
                  then (Test = Inside)
                       /= Ada.Strings.Maps.Is_In (Source (J), Set)))),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);

   function Index
     (Source  : String;
      Set     : Maps.Character_Set;
      From    : Positive;
      Test    : Membership := Inside;
      Going   : Direction := Forward) return Natural
   with
     Pre            => (if Source'Length > 0 then From in Source'Range),
     Post           => Index'Result in 0 | Source'Range,
     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.

        (Source'Length = 0
          or else
            (for all J in Source'Range =>
               (if J = From or else (J > From) = (Going = Forward) then
                  (Test = Inside) /= Ada.Strings.Maps.Is_In (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 Source'Range
            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)
              = Ada.Strings.Maps.Is_In (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 Source'Range =>
                 (if J /= Index'Result
                    and then (J < Index'Result) = (Going = Forward)
                    and then (J = From
                                or else (J > From) = (Going = Forward))
                  then (Test = Inside)
                       /= Ada.Strings.Maps.Is_In (Source (J), Set)))),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);
   pragma Ada_05 (Index);
   --  Index searches for the first or last occurrence of any of a set of
   --  characters (when Test=Inside), or any of the complement of a set of
   --  characters (when Test=Outside). If Source is the null string, Index
   --  returns 0; otherwise, if From is not in Source'Range, then Index_Error
   --  is propagated. Otherwise, it returns the smallest index I >= From (if
   --  Going=Forward) or the largest index I <= From (if Going=Backward) such
   --  that Source(I) satisfies the Test condition with respect to Set; it
   --  returns 0 if there is no such Character in Source.

   function Index_Non_Blank
     (Source : String;
      From   : Positive;
      Going  : Direction := Forward) return Natural
   with
     Pre            => (if Source'Length /= 0 then From in Source'Range),

     Post           => Index_Non_Blank'Result in 0 | Source'Range,
     Contract_Cases =>

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

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

        --  Otherwise, a valid index is returned

        others
        =>

          --  The result is in the considered range of Source

          Index_Non_Blank'Result in Source'Range
            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 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 Source'Range =>
                 (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 Source (J) = ' '))),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);
   pragma Ada_05 (Index_Non_Blank);
   --  Returns Index (Source, Maps.To_Set(Space), From, Outside, Going)

   function Index_Non_Blank
     (Source : String;
      Going  : Direction := Forward) return Natural
   with
     Post           => Index_Non_Blank'Result in 0 | Source'Range,
     Contract_Cases =>

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

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

        --  Otherwise, a valid index is returned

        others                           =>

          --  The result is in the range of Source

          Index_Non_Blank'Result in Source'Range

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

            and then 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 Source'Range =>
                 (if J /= Index_Non_Blank'Result
                       and then (J < Index_Non_Blank'Result)
                              = (Going = Forward)
                  then Source (J) = ' '))),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);
   --  Returns Index (Source, Maps.To_Set(Space), Outside, Going)

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

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

   --  Returns the maximum number of nonoverlapping slices of Source that match
   --  Pattern with respect to Mapping. If Pattern is the null string then
   --  Pattern_Error is propagated.

   function Count
     (Source : String;
      Set    : Maps.Character_Set) return Natural
   with
     Global   => null,
     Annotate => (GNATprove, Always_Return);
   --  Returns the number of occurrences in Source of characters that are in
   --  Set.

   procedure Find_Token
     (Source : String;
      Set    : Maps.Character_Set;
      From   : Positive;
      Test   : Membership;
      First  : out Positive;
      Last   : out Natural)
   with
     Pre            => (if Source'Length /= 0 then From in Source'Range),
     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.

       (Source'Length = 0
          or else
            (for all C of Source (From .. Source'Last) =>
               (Test = Inside) /= Ada.Strings.Maps.Is_In (C, 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 .. Source'Last
            and then Last in First .. Source'Last

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

            and then
              (for all C of Source (From .. First - 1) =>
                 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))

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

            and then
              (for all C of Source (First .. Last) =>
                 (Test = Inside) = Ada.Strings.Maps.Is_In (C, 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 < Source'Last
               then
                 (Test = Inside)
                 /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);
   pragma Ada_2012 (Find_Token);
   --  If Source is not the null string and From is not in Source'Range, then
   --  Index_Error is raised. Otherwise, First is set to the index of the first
   --  character in Source(From .. Source'Last) that satisfies the Test
   --  condition. Last is set to the largest index such that all characters in
   --  Source(First .. Last) satisfy the Test condition. If no characters in
   --  Source(From .. Source'Last) satisfy the Test condition, First is set to
   --  From, and Last is set to 0.

   procedure Find_Token
     (Source : String;
      Set    : Maps.Character_Set;
      Test   : Membership;
      First  : out Positive;
      Last   : out Natural)
   with
     Pre            => Source'First > 0,
     Contract_Cases =>

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

       (Source'Length = 0
          or else
            (for all C of Source =>
               (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))
        =>
          First = Source'First 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 Source'Range
            and then Last in First .. Source'Last

            --  No character before First satisfies the property Test on Set

            and then
              (for all C of Source (Source'First .. First - 1) =>
                 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set))

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

            and then
              (for all C of Source (First .. Last) =>
                 (Test = Inside) = Ada.Strings.Maps.Is_In (C, 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 < Source'Last
               then
                 (Test = Inside)
                 /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);
   --  Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last)

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

   function Translate
     (Source  : String;
      Mapping : Maps.Character_Mapping_Function) return String
   with
     Pre    => Mapping /= null,
     Post   =>

       --  Lower bound of the returned string is 1

       Translate'Result'First = 1

         --  The returned string has the same length as Source

         and then Translate'Result'Last = Source'Length

         --  Each character in the returned string is the translation of the
         --  character at the same position in Source through Mapping.

         and then
           (for all J in Source'Range =>
              Translate'Result (J - Source'First + 1)
              = Mapping (Source (J))),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);
   pragma Annotate (GNATprove, False_Positive,
                    "call via access-to-subprogram",
                    "function Mapping must always terminate");

   function Translate
     (Source  : String;
      Mapping : Maps.Character_Mapping) return String
   with
     Post   =>

       --  Lower bound of the returned string is 1

       Translate'Result'First = 1

         --  The returned string has the same length as Source

         and then Translate'Result'Last = Source'Length

         --  Each character in the returned string is the translation of the
         --  character at the same position in Source through Mapping.

         and then
           (for all J in Source'Range =>
              Translate'Result (J - Source'First + 1)
              = Ada.Strings.Maps.Value (Mapping, Source (J))),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);

   --  Returns the string S whose length is Source'Length and such that S (I)
   --  is the character to which Mapping maps the corresponding element of
   --  Source, for I in 1 .. Source'Length.

   procedure Translate
     (Source  : in out String;
      Mapping : Maps.Character_Mapping_Function)
   with
     Pre      => Mapping /= null,
     Post     =>

       --  Each character in Source after the call is the translation of the
       --  character at the same position before the call, through Mapping.

       (for all J in Source'Range => Source (J) = Mapping (Source'Old (J))),
     Global   => null,
     Annotate => (GNATprove, Always_Return);
   pragma Annotate (GNATprove, False_Positive,
                    "call via access-to-subprogram",
                    "function Mapping must always terminate");

   procedure Translate
     (Source  : in out String;
      Mapping : Maps.Character_Mapping)
   with
     Post     =>

       --  Each character in Source after the call is the translation of the
       --  character at the same position before the call, through Mapping.

       (for all J in Source'Range =>
          Source (J) = Ada.Strings.Maps.Value (Mapping, Source'Old (J))),
     Global   => null,
     Annotate => (GNATprove, Always_Return);

   --  Equivalent to Source := Translate(Source, Mapping)

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

   function Replace_Slice
     (Source : String;
      Low    : Positive;
      High   : Natural;
      By     : String) return String
   with
     Pre            =>
       Low - 1 <= Source'Last
         and then High >= Source'First - 1
         and then (if High >= Low
                   then Natural'Max (0, Low - Source'First)
                        <= Natural'Last
                           - By'Length
                           - Natural'Max (Source'Last - High, 0)
                   else Source'Length <= Natural'Last - By'Length),

     --  Lower bound of the returned string is 1

     Post           => Replace_Slice'Result'First = 1,
     Contract_Cases =>

        --  If High >= Low, then the returned string comprises
        --  Source (Source'First .. Low - 1) & By
        --  & Source(High + 1 .. Source'Last).

       (High >= Low =>

          --  Length of the returned string

          Replace_Slice'Result'Length
          = Integer'Max (0, Low - Source'First)
            + By'Length
            + Integer'Max (Source'Last - High, 0)

            --  Elements starting at Low are replaced by elements of By

            and then
              Replace_Slice'Result (1 .. Integer'Max (0, Low - Source'First))
              = Source (Source'First .. Low - 1)
            and then
              Replace_Slice'Result
                (Integer'Max (0, Low - Source'First) + 1
                 .. Integer'Max (0, Low - Source'First) + By'Length)
              = By

            --  When there are remaining characters after the replaced slice,
            --  they are appended to the result.

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

        --  If High < Low, then the returned string is
        --  Insert (Source, Before => Low, New_Item => By).

        others      =>

          --  Length of the returned string

          Replace_Slice'Result'Length = Source'Length + By'Length

            --  Elements of By are inserted after the element at Low

            and then
              Replace_Slice'Result (1 .. Low - Source'First)
              = Source (Source'First .. Low - 1)
            and then
              Replace_Slice'Result
                (Low - Source'First + 1 .. Low - Source'First + By'Length)
              = By

            --  When there are remaining characters after Low in Source, they
            --  are appended to the result.

            and then
              (if Low < Source'Last
               then
                Replace_Slice'Result
                  (Low - Source'First + By'Length + 1
                   .. Replace_Slice'Result'Last)
                = Source (Low .. Source'Last))),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);
   --  If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error
   --  is propagated. Otherwise:
   --
   --  * If High >= Low, then the returned string comprises
   --    Source (Source'First .. Low - 1)
   --    & By & Source(High + 1 .. Source'Last), but with lower bound 1.
   --
   --  * If High < Low, then the returned string is
   --    Insert (Source, Before => Low, New_Item => By).

   procedure Replace_Slice
     (Source  : in out String;
      Low     : Positive;
      High    : Natural;
      By      : String;
      Drop    : Truncation := Error;
      Justify : Alignment  := Left;
      Pad     : Character  := Space)
   with
     Pre      =>
       Low - 1 <= Source'Last
         and then High >= Source'First - 1
         and then (if High >= Low
                   then Natural'Max (0, Low - Source'First)
                        <= Natural'Last
                           - By'Length
                           - Natural'Max (Source'Last - High, 0)
                   else Source'Length <= Natural'Last - By'Length),

   --  Incomplete contract

     Global   => null,
     Annotate => (GNATprove, Might_Not_Return);
   --  Equivalent to:
   --
   --    Move (Replace_Slice (Source, Low, High, By),
   --          Source, Drop, Justify, Pad).

   function Insert
     (Source   : String;
      Before   : Positive;
      New_Item : String) return String
   with
     Pre    =>
       Before - 1 in Source'First - 1 .. Source'Last
         and then Source'Length <= Natural'Last - New_Item'Length,

     Post   =>

       --  Lower bound of the returned string is 1

       Insert'Result'First = 1

         --  Length of the returned string

         and then Insert'Result'Length = Source'Length + New_Item'Length

         --  Elements of New_Item are inserted after element at Before

         and then
           Insert'Result (1 .. Before - Source'First)
           = Source (Source'First .. Before - 1)
         and then
           Insert'Result
             (Before - Source'First + 1
              .. Before - Source'First + New_Item'Length)
           = New_Item

         --  When there are remaining characters after Before in Source, they
         --  are appended to the returned string.

         and then
           (if Before <= Source'Last
            then
              Insert'Result
                (Before - Source'First + New_Item'Length + 1
                 .. Insert'Result'Last)
              = Source (Before .. Source'Last)),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);
   --  Propagates Index_Error if Before is not in
   --  Source'First .. Source'Last + 1; otherwise, returns
   --  Source (Source'First .. Before - 1)
   --  & New_Item & Source(Before..Source'Last), but with lower bound 1.

   procedure Insert
     (Source   : in out String;
      Before   : Positive;
      New_Item : String;
      Drop     : Truncation := Error)
   with
     Pre      =>
       Before - 1 in Source'First - 1 .. Source'Last
         and then Source'Length <= Natural'Last - New_Item'Length,

     --  Incomplete contract

     Global   => null,
     Annotate => (GNATprove, Might_Not_Return);
   --  Equivalent to Move (Insert (Source, Before, New_Item), Source, Drop)

   function Overwrite
     (Source   : String;
      Position : Positive;
      New_Item : String) return String
   with
     Pre      =>
       Position - 1 in Source'First - 1 .. Source'Last
         and then
           (if Position - Source'First >= Source'Length - New_Item'Length
            then Position - Source'First <= Natural'Last - New_Item'Length),

     Post     =>

       --  Lower bound of the returned string is 1

       Overwrite'Result'First = 1

         --  Length of the returned string

         and then
           Overwrite'Result'Length
           = Integer'Max (Source'Length,
                          Position - Source'First + New_Item'Length)

         --  Elements after Position are replaced by elements of New_Item

         and then
           Overwrite'Result (1 .. Position - Source'First)
           = Source (Source'First .. Position - 1)
         and then
           Overwrite'Result
             (Position - Source'First + 1
              .. Position - Source'First + New_Item'Length)
           = New_Item

         --  If the end of Source is reached before the characters in New_Item
         --  are exhausted, the remaining characters from New_Item are appended
         --  to the string.

         and then
           (if Position <= Source'Last - New_Item'Length
            then
              Overwrite'Result
                (Position - Source'First + New_Item'Length + 1
                 .. Overwrite'Result'Last)
              = Source (Position + New_Item'Length .. Source'Last)),
     Global   => null,
     Annotate => (GNATprove, Always_Return);
   --  Propagates Index_Error if Position is not in
   --  Source'First .. Source'Last + 1; otherwise, returns the string obtained
   --  from Source by consecutively replacing characters starting at Position
   --  with corresponding characters from New_Item. If the end of Source is
   --  reached before the characters in New_Item are exhausted, the remaining
   --  characters from New_Item are appended to the string.

   procedure Overwrite
     (Source   : in out String;
      Position : Positive;
      New_Item : String;
      Drop     : Truncation := Right)
   with
     Pre      =>
       Position - 1 in Source'First - 1 .. Source'Last
         and then
           (if Position - Source'First >= Source'Length - New_Item'Length
            then Position - Source'First <= Natural'Last - New_Item'Length),

     --  Incomplete contract

     Global   => null,
     Annotate => (GNATprove, Might_Not_Return);
   --  Equivalent to Move(Overwrite(Source, Position, New_Item), Source, Drop)

   function Delete
     (Source  : String;
      From    : Positive;
      Through : Natural) return String
   with
     Pre            => (if From <= Through
                        then (From in Source'Range
                                and then Through <= Source'Last)),

     --  Lower bound of the returned string is 1

     Post           =>
       Delete'Result'First = 1,

     Contract_Cases =>

        --  If From <= Through, the characters between From and Through are
        --  removed.

       (From <= Through =>

          --  Length of the returned string

          Delete'Result'Length = Source'Length - (Through - From + 1)

            --  Elements before From are preserved

            and then
              Delete'Result (1 .. From - Source'First)
              = Source (Source'First .. From - 1)

            --  If there are remaining characters after Through, they are
            --  appended to the returned string.

            and then
              (if Through < Source'Last
               then Delete'Result
                      (From - Source'First + 1 .. Delete'Result'Last)
                    = Source (Through + 1 .. Source'Last)),

        --  Otherwise, the returned string is Source with lower bound 1

        others          =>
          Delete'Result'Length = Source'Length
            and then Delete'Result = Source),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);
   --  If From <= Through, the returned string is
   --  Replace_Slice(Source, From, Through, ""); otherwise, it is Source with
   --  lower bound 1.

   procedure Delete
     (Source  : in out String;
      From    : Positive;
      Through : Natural;
      Justify : Alignment := Left;
      Pad     : Character := Space)
   with
     Pre      => (if From <= Through
                  then (From in Source'Range
                          and then Through <= Source'Last)),

     --  Incomplete contract

     Global   => null,
     Annotate => (GNATprove, Might_Not_Return);
   --  Equivalent to:
   --
   --     Move (Delete (Source, From, Through),
   --           Source, Justify => Justify, Pad => Pad).

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

   function Trim
     (Source : String;
      Side   : Trim_End) return String
   with
     Post     =>

       --  Lower bound of the returned string is 1

       Trim'Result'First = 1

       --  If all characters in Source are Space, the returned string is
       --  empty.

         and then
           (if (for all J in Source'Range => Source (J) = ' ')
            then Trim'Result = ""

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

            else
              (declare
                 Low  : constant Positive :=
                   (if Side = Right then Source'First
                    else Index_Non_Blank (Source, Forward));
                 High : constant Positive :=
                   (if Side = Left then Source'Last
                    else Index_Non_Blank (Source, Backward));
               begin
                 Trim'Result = Source (Low .. High))),
     Global   => null,
     Annotate => (GNATprove, Always_Return);
   --  Returns the string obtained by removing from Source all leading Space
   --  characters (if Side = Left), all trailing Space characters (if
   --  Side = Right), or all leading and trailing Space characters (if
   --  Side = Both).

   procedure Trim
     (Source  : in out String;
      Side    : Trim_End;
      Justify : Alignment := Left;
      Pad     : Character := Space)
   with

     --  Incomplete contract

     Global   => null,
     Annotate => (GNATprove, Might_Not_Return);
   --  Equivalent to:
   --
   --     Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad).

   function Trim
     (Source : String;
      Left   : Maps.Character_Set;
      Right  : Maps.Character_Set) return String
   with
     Post   =>

       --  Lower bound of the returned string is 1

       Trim'Result'First = 1

         --  If all characters are contained in one of the sets Left and Right,
         --  then the returned string is empty.

         and then
           (if (for all K in Source'Range =>
                  Ada.Strings.Maps.Is_In (Source (K), Left))
                 or
                   (for all K in Source'Range =>
                      Ada.Strings.Maps.Is_In (Source (K), Right))
            then Trim'Result = ""

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

        else
           (declare
              Low  : constant Positive :=
                Index (Source, Left, Outside, Forward);
              High : constant Positive :=
                Index (Source, Right, Outside, Backward);
            begin
              Trim'Result = Source (Low .. High))),
     Global   => null,
     Annotate => (GNATprove, Always_Return);
   --  Returns the string obtained by removing from Source all leading
   --  characters in Left and all trailing characters in Right.

   procedure Trim
     (Source  : in out String;
      Left    : Maps.Character_Set;
      Right   : Maps.Character_Set;
      Justify : Alignment := Strings.Left;
      Pad     : Character := Space)
   with

     --  Incomplete contract

     Global   => null,
     Annotate => (GNATprove, Might_Not_Return);
   --  Equivalent to:
   --
   --     Move (Trim (Source, Left, Right),
   --           Source, Justify => Justify, Pad=>Pad).

   function Head
     (Source : String;
      Count  : Natural;
      Pad    : Character := Space) return String
   with
     Post           =>

       --  Lower bound of the returned string is 1

       Head'Result'First = 1

         --  Length of the returned string is Count.

         and then Head'Result'Length = Count,

     Contract_Cases =>

        --  If Count <= Source'Length, then the first Count characters of
        --  Source are returned.

       (Count <= Source'Length =>
          Head'Result = Source (Source'First .. Source'First - 1 + Count),

        --  Otherwise, the returned string is Source concatenated with
        --  Count - Source'Length Pad characters.

        others                 =>
          Head'Result (1 .. Source'Length) = Source
            and then
              Head'Result (Source'Length + 1 .. Count)
              = [1 .. Count - Source'Length => Pad]),
     Global         => null,
     Annotate       => (GNATprove, Always_Return);
   --  Returns a string of length Count. If Count <= Source'Length, the string
   --  comprises the first Count characters of Source. Otherwise, its contents
   --  are Source concatenated with Count - Source'Length Pad characters.

   procedure Head
     (Source  : in out String;
      Count   : Natural;
      Justify : Alignment := Left;
      Pad     : Character := Space)
   with

     --  Incomplete contract

     Global   => null,
     Annotate => (GNATprove, Might_Not_Return);
   --  Equivalent to:
   --
   --     Move (Head (Source, Count, Pad),
   --           Source, Drop => Error, Justify => Justify, Pad => Pad).

   function Tail
     (Source : String;
      Count  : Natural;
      Pad    : Character := Space) return String
   with
     Post   =>

       --  Lower bound of the returned string is 1

       Tail'Result'First = 1

         --  Length of the returned string is Count

         and then Tail'Result'Length = Count,
     Contract_Cases =>

       --  If Count is zero, then the returned string is empty

       (Count = 0                     =>
          Tail'Result = "",

        --  Otherwise, if Count <= Source'Length, then the last Count
        --  characters of Source are returned.

        (Count in 1 .. Source'Length) =>
          Tail'Result = Source (Source'Last - Count + 1 .. Source'Last),

        --  Otherwise, the returned string is Count - Source'Length Pad
        --  characters concatenated with Source.

        others                        =>

           --  If Source is empty, then the returned string is Count Pad
           --  characters.

          (if Source'Length = 0
           then Tail'Result = [1 .. Count => Pad]
           else
             Tail'Result (1 .. Count - Source'Length)
             = [1 .. Count - Source'Length => Pad]
               and then
                 Tail'Result (Count - Source'Length + 1 .. Tail'Result'Last)
                 = Source)),
     Global   => null,
     Annotate => (GNATprove, Always_Return);
   --  Returns a string of length Count. If Count <= Source'Length, the string
   --  comprises the last Count characters of Source. Otherwise, its contents
   --  are Count-Source'Length Pad characters concatenated with Source.

   procedure Tail
     (Source  : in out String;
      Count   : Natural;
      Justify : Alignment := Left;
      Pad     : Character := Space)
   with

     --  Incomplete contract

     Global   => null,
     Annotate => (GNATprove, Might_Not_Return);
   --  Equivalent to:
   --
   --     Move (Tail (Source, Count, Pad),
   --           Source, Drop => Error, Justify => Justify, Pad => Pad).

   ----------------------------------
   -- String Constructor Functions --
   ----------------------------------

   function "*"
     (Left  : Natural;
      Right : Character) return String
   with
     Post     =>

       --  Lower bound of the returned string is 1

       "*"'Result'First = 1

         --  Length of the returned string

         and then "*"'Result'Length = Left

         --  All characters of the returned string are Right

         and then (for all C of "*"'Result => C = Right),
     Global   => null,
     Annotate => (GNATprove, Always_Return);

   function "*"
     (Left  : Natural;
      Right : String) return String
   with
     Pre    => (if Right'Length /= 0 then Left <= Natural'Last / Right'Length),

     Post   =>

       --  Lower bound of the returned string is 1

       "*"'Result'First = 1

         --  Length of the returned string

         and then "*"'Result'Length = Left * Right'Length

         --  Content of the string is Right concatenated with itself Left times

         and then
           (for all K in "*"'Result'Range =>
              "*"'Result (K) = Right (Right'First + (K - 1) mod Right'Length)),
     Global   => null,
     Annotate => (GNATprove, Always_Return);

   --  These functions replicate a character or string a specified number of
   --  times. The first function returns a string whose length is Left and each
   --  of whose elements is Right. The second function returns a string whose
   --  length is Left * Right'Length and whose value is the null string if
   --  Left = 0 and otherwise is (Left - 1)*Right & Right with lower bound 1.

end Ada.Strings.Fixed;