------------------------------------------------------------------------------
--                                                                          --
--                         GNAT RUN-TIME COMPONENTS                         --
--                                                                          --
--             A D A . S T R I N G S . S U P E R B O U N D E D              --
--                                                                          --
--                                 S p e c                                  --
--                                                                          --
--          Copyright (C) 2003-2023, Free Software Foundation, Inc.         --
--                                                                          --
-- 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.      --
--                                                                          --
------------------------------------------------------------------------------

--  This non generic package contains most of the implementation of the
--  generic package Ada.Strings.Bounded.Generic_Bounded_Length.

--  It defines type Super_String as a discriminated record with the maximum
--  length as the discriminant. Individual instantiations of Strings.Bounded
--  use this type with an appropriate discriminant value set.

--  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;
with Ada.Strings.Text_Buffers;

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

   --  Type Bounded_String in Ada.Strings.Bounded.Generic_Bounded_Length is
   --  derived from Super_String, with the constraint of the maximum length.

   type Super_String_Data is new String with Relaxed_Initialization;

   type Super_String (Max_Length : Positive) is record
      Current_Length : Natural := 0;
      Data           : Super_String_Data (1 .. Max_Length);
      --  A previous version had a default initial value for Data, which is
      --  no longer necessary, because we now special-case this type in the
      --  compiler, so "=" composes properly for descendants of this type.
      --  Leaving it out is more efficient.
   end record
   with
     Ghost_Predicate =>
       Current_Length <= Max_Length
         and then Data (1 .. Current_Length)'Initialized,
     Put_Image => Put_Image;

   --  The subprograms defined for Super_String are similar to those
   --  defined for Bounded_String, except that they have different names, so
   --  that they can be renamed in Ada.Strings.Bounded.Generic_Bounded_Length.

   function Super_Length (Source : Super_String) return Natural
   is (Source.Current_Length)
   with Global => null;

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

   function To_Super_String
     (Source     : String;
      Max_Length : Positive;
      Drop       : Truncation := Error) return Super_String
   with
     Pre            => (if Source'Length > Max_Length then Drop /= Error),
     Post           => To_Super_String'Result.Max_Length = Max_Length,
     Contract_Cases =>
       (Source'Length <= Max_Length
        =>
          Super_To_String (To_Super_String'Result) = Source,

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

        others  --  Drop = Right
        =>
          Super_To_String (To_Super_String'Result) =
            Source (Source'First .. Source'First - 1 + Max_Length)),
     Global         => null;
   --  Note the additional parameter Max_Length, which specifies the maximum
   --  length setting of the resulting Super_String value.

   --  The following procedures have declarations (and semantics) that are
   --  exactly analogous to those declared in Ada.Strings.Bounded.

   function Super_To_String (Source : Super_String) return String
   is (String (Source.Data (1 .. Source.Current_Length)));

   procedure Set_Super_String
     (Target : out Super_String;
      Source : String;
      Drop   : Truncation := Error)
   with
     Pre            =>
       (if Source'Length > Target.Max_Length then Drop /= Error),
     Contract_Cases =>
       (Source'Length <= Target.Max_Length
        =>
          Super_To_String (Target) = Source,

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

        others  --  Drop = Right
        =>
          Super_To_String (Target) =
            Source (Source'First .. Source'First - 1 + Target.Max_Length)),
     Global         => null;

   function Super_Append
     (Left  : Super_String;
      Right : Super_String;
      Drop  : Truncation  := Error) return Super_String
   with
     Pre            =>
       Left.Max_Length = Right.Max_Length
         and then
           (if Super_Length (Left) > Left.Max_Length - Super_Length (Right)
            then Drop /= Error),
     Post           => Super_Append'Result.Max_Length = Left.Max_Length,
     Contract_Cases =>
       (Super_Length (Left) <= Left.Max_Length - Super_Length (Right)
        =>
          Super_Length (Super_Append'Result) =
            Super_Length (Left) + Super_Length (Right)
            and then
              Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
                Super_To_String (Left)
            and then
              (if Super_Length (Right) > 0 then
                 Super_Slice (Super_Append'Result,
                   Super_Length (Left) + 1,
                   Super_Length (Super_Append'Result)) =
                     Super_To_String (Right)),

        Super_Length (Left) > Left.Max_Length - Super_Length (Right)
          and then Drop = Strings.Left
        =>
          Super_Length (Super_Append'Result) = Left.Max_Length
            and then
              (if Super_Length (Right) < Left.Max_Length then
                 String'(Super_Slice (Super_Append'Result,
                   1, Left.Max_Length - Super_Length (Right))) =
                     Super_Slice (Left,
                       Super_Length (Left) - Left.Max_Length
                         + Super_Length (Right) + 1,
                       Super_Length (Left)))
            and then
              Super_Slice (Super_Append'Result,
                Left.Max_Length - Super_Length (Right) + 1, Left.Max_Length) =
                  Super_To_String (Right),

        others  --  Drop = Right
        =>
          Super_Length (Super_Append'Result) = Left.Max_Length
            and then
              Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
                Super_To_String (Left)
            and then
              (if Super_Length (Left) < Left.Max_Length then
                 String'(Super_Slice (Super_Append'Result,
                   Super_Length (Left) + 1, Left.Max_Length)) =
                     Super_Slice (Right,
                       1, Left.Max_Length - Super_Length (Left)))),
     Global         => null;

   function Super_Append
     (Left  : Super_String;
      Right : String;
      Drop  : Truncation := Error) return Super_String
   with
     Pre            =>
       (if Right'Length > Left.Max_Length - Super_Length (Left)
        then Drop /= Error),
     Post           => Super_Append'Result.Max_Length = Left.Max_Length,
     Contract_Cases =>
       (Super_Length (Left) <= Left.Max_Length - Right'Length
        =>
          Super_Length (Super_Append'Result) =
            Super_Length (Left) + Right'Length
            and then
              Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
                Super_To_String (Left)
            and then
              (if Right'Length > 0 then
                 Super_Slice (Super_Append'Result,
                   Super_Length (Left) + 1,
                   Super_Length (Super_Append'Result)) =
                     Right),

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

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

                 String'(Super_Slice (Super_Append'Result,
                   1, Left.Max_Length - Right'Length)) =
                     Super_Slice (Left,
                       Super_Length (Left) - Left.Max_Length + Right'Length
                         + 1,
                       Super_Length (Left))
                   and then
                     Super_Slice (Super_Append'Result,
                       Left.Max_Length - Right'Length + 1, Left.Max_Length) =
                         Right
               else
                 --  The result is the last Max_Length characters of Right

                 Super_To_String (Super_Append'Result) =
                   Right (Right'Last - Left.Max_Length + 1 .. Right'Last)),

        others  --  Drop = Right
        =>
          Super_Length (Super_Append'Result) = Left.Max_Length
            and then
              Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
                Super_To_String (Left)
            and then
              (if Super_Length (Left) < Left.Max_Length then
                 Super_Slice (Super_Append'Result,
                   Super_Length (Left) + 1, Left.Max_Length) =
                     Right (Right'First
                       .. Left.Max_Length - Super_Length (Left)
                            - 1 + Right'First))),
     Global         => null;

   function Super_Append
     (Left  : String;
      Right : Super_String;
      Drop  : Truncation := Error) return Super_String
   with
     Pre            =>
       (if Left'Length > Right.Max_Length - Super_Length (Right)
        then Drop /= Error),
     Post           => Super_Append'Result.Max_Length = Right.Max_Length,
     Contract_Cases =>
       (Left'Length <= Right.Max_Length - Super_Length (Right)
        =>
          Super_Length (Super_Append'Result) =
            Left'Length + Super_Length (Right)
            and then Super_Slice (Super_Append'Result, 1, Left'Length) = Left
            and then
              (if Super_Length (Right) > 0 then
                 Super_Slice (Super_Append'Result,
                   Left'Length + 1, Super_Length (Super_Append'Result)) =
                     Super_To_String (Right)),

        Left'Length > Right.Max_Length - Super_Length (Right)
          and then Drop = Strings.Left
        =>
          Super_Length (Super_Append'Result) = Right.Max_Length
            and then
              (if Super_Length (Right) < Right.Max_Length then
                 Super_Slice (Super_Append'Result,
                   1, Right.Max_Length - Super_Length (Right)) =
                     Left
                       (Left'Last - Right.Max_Length + Super_Length (Right) + 1
                        .. Left'Last))
            and then
              Super_Slice (Super_Append'Result,
                Right.Max_Length - Super_Length (Right) + 1,
                Right.Max_Length) =
                  Super_To_String (Right),

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

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

                 Super_Slice (Super_Append'Result, 1, Left'Length) = Left
                   and then
                     String'(Super_Slice (Super_Append'Result,
                       Left'Length + 1, Right.Max_Length)) =
                         Super_Slice (Right, 1, Right.Max_Length - Left'Length)
               else
                 --  The result is the first Max_Length characters of Left

                 Super_To_String (Super_Append'Result) =
                   Left (Left'First .. Right.Max_Length - 1 + Left'First))),
     Global         => null;

   function Super_Append
     (Left  : Super_String;
      Right : Character;
      Drop  : Truncation := Error) return Super_String
   with
     Pre            =>
       (if Super_Length (Left) = Left.Max_Length then Drop /= Error),
     Post           => Super_Append'Result.Max_Length = Left.Max_Length,
     Contract_Cases =>
       (Super_Length (Left) < Left.Max_Length
        =>
          Super_Length (Super_Append'Result) = Super_Length (Left) + 1
            and then
              Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
                Super_To_String (Left)
            and then
              Super_Element (Super_Append'Result, Super_Length (Left) + 1) =
                Right,

        Super_Length (Left) = Left.Max_Length and then Drop = Strings.Right
        =>
          Super_Length (Super_Append'Result) = Left.Max_Length
            and then
              Super_To_String (Super_Append'Result) = Super_To_String (Left),

        others  --  Drop = Left
        =>
          Super_Length (Super_Append'Result) = Left.Max_Length
            and then
              String'(Super_Slice (Super_Append'Result,
                1, Left.Max_Length - 1)) =
                  Super_Slice (Left, 2, Left.Max_Length)
            and then
              Super_Element (Super_Append'Result, Left.Max_Length) = Right),
     Global         => null;

   function Super_Append
     (Left  : Character;
      Right : Super_String;
      Drop  : Truncation := Error) return Super_String
   with
     Pre            =>
       (if Super_Length (Right) = Right.Max_Length then Drop /= Error),
     Post           => Super_Append'Result.Max_Length = Right.Max_Length,
     Contract_Cases =>
       (Super_Length (Right) < Right.Max_Length
        =>
          Super_Length (Super_Append'Result) = Super_Length (Right) + 1
            and then
              Super_Slice (Super_Append'Result, 2, Super_Length (Right) + 1) =
                Super_To_String (Right)
            and then Super_Element (Super_Append'Result, 1) = Left,

        Super_Length (Right) = Right.Max_Length and then Drop = Strings.Left
        =>
          Super_Length (Super_Append'Result) = Right.Max_Length
            and then
              Super_To_String (Super_Append'Result) = Super_To_String (Right),

        others  --  Drop = Right
        =>
          Super_Length (Super_Append'Result) = Right.Max_Length
            and then
              String'(Super_Slice (Super_Append'Result, 2, Right.Max_Length)) =
                Super_Slice (Right, 1, Right.Max_Length - 1)
            and then Super_Element (Super_Append'Result, 1) = Left),
     Global         => null;

   procedure Super_Append
     (Source   : in out Super_String;
      New_Item : Super_String;
      Drop     : Truncation  := Error)
   with
     Pre            =>
       Source.Max_Length = New_Item.Max_Length
         and then
           (if Super_Length (Source) >
                 Source.Max_Length - Super_Length (New_Item)
            then Drop /= Error),
     Contract_Cases =>
       (Super_Length (Source) <= Source.Max_Length - Super_Length (New_Item)
        =>
          Super_Length (Source) =
            Super_Length (Source'Old) + Super_Length (New_Item)
            and then
              Super_Slice (Source, 1, Super_Length (Source'Old)) =
                Super_To_String (Source'Old)
            and then
              (if Super_Length (New_Item) > 0 then
                 Super_Slice (Source,
                   Super_Length (Source'Old) + 1, Super_Length (Source)) =
                     Super_To_String (New_Item)),

        Super_Length (Source) > Source.Max_Length - Super_Length (New_Item)
          and then Drop = Left
        =>
          Super_Length (Source) = Source.Max_Length
            and then
              (if Super_Length (New_Item) < Source.Max_Length then
                 String'(Super_Slice (Source,
                   1, Source.Max_Length - Super_Length (New_Item))) =
                     Super_Slice (Source'Old,
                       Super_Length (Source'Old) - Source.Max_Length
                         + Super_Length (New_Item) + 1,
                       Super_Length (Source'Old)))
            and then
              Super_Slice (Source,
                Source.Max_Length - Super_Length (New_Item) + 1,
                Source.Max_Length) =
                  Super_To_String (New_Item),

        others  --  Drop = Right
        =>
          Super_Length (Source) = Source.Max_Length
            and then
              Super_Slice (Source, 1, Super_Length (Source'Old)) =
                Super_To_String (Source'Old)
            and then
              (if Super_Length (Source'Old) < Source.Max_Length then
                 String'(Super_Slice (Source,
                   Super_Length (Source'Old) + 1, Source.Max_Length)) =
                     Super_Slice (New_Item,
                       1, Source.Max_Length - Super_Length (Source'Old)))),
     Global         => null;

   procedure Super_Append
     (Source   : in out Super_String;
      New_Item : String;
      Drop     : Truncation  := Error)
   with
     Pre            =>
       (if New_Item'Length > Source.Max_Length - Super_Length (Source)
        then Drop /= Error),
     Contract_Cases =>
       (Super_Length (Source) <= Source.Max_Length - New_Item'Length
        =>
          Super_Length (Source) = Super_Length (Source'Old) + New_Item'Length
            and then
              Super_Slice (Source, 1, Super_Length (Source'Old)) =
                Super_To_String (Source'Old)
            and then
              (if New_Item'Length > 0 then
                 Super_Slice (Source,
                   Super_Length (Source'Old) + 1, Super_Length (Source)) =
                     New_Item),

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

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

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

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

        others  --  Drop = Right
        =>
          Super_Length (Source) = Source.Max_Length
            and then
              Super_Slice (Source, 1, Super_Length (Source'Old)) =
                Super_To_String (Source'Old)
            and then
              (if Super_Length (Source'Old) < Source.Max_Length then
                 Super_Slice (Source,
                   Super_Length (Source'Old) + 1, Source.Max_Length) =
                     New_Item (New_Item'First
                       .. Source.Max_Length - Super_Length (Source'Old) - 1
                         + New_Item'First))),
     Global         => null;

   procedure Super_Append
     (Source   : in out Super_String;
      New_Item : Character;
      Drop     : Truncation  := Error)
   with
     Pre            =>
       (if Super_Length (Source) = Source.Max_Length then Drop /= Error),
     Contract_Cases =>
       (Super_Length (Source) < Source.Max_Length
        =>
          Super_Length (Source) = Super_Length (Source'Old) + 1
            and then
              Super_Slice (Source, 1, Super_Length (Source'Old)) =
                Super_To_String (Source'Old)
            and then
              Super_Element (Source, Super_Length (Source'Old) + 1) = New_Item,

        Super_Length (Source) = Source.Max_Length and then Drop = Right
        =>
          Super_Length (Source) = Source.Max_Length
            and then Super_To_String (Source) = Super_To_String (Source'Old),

        others  --  Drop = Left
        =>
          Super_Length (Source) = Source.Max_Length
            and then
              String'(Super_Slice (Source, 1, Source.Max_Length - 1)) =
                Super_Slice (Source'Old, 2, Source.Max_Length)
            and then Super_Element (Source, Source.Max_Length) = New_Item),
     Global         => null;

   function Concat
     (Left  : Super_String;
      Right : Super_String) return Super_String
   with
     Pre    => Left.Max_Length = Right.Max_Length
       and then Super_Length (Left) <= Left.Max_Length - Super_Length (Right),
     Post   => Concat'Result.Max_Length = Left.Max_Length
       and then
         Super_Length (Concat'Result) =
           Super_Length (Left) + Super_Length (Right)
       and then
         Super_Slice (Concat'Result, 1, Super_Length (Left)) =
           Super_To_String (Left)
       and then
         (if Super_Length (Right) > 0 then
            Super_Slice (Concat'Result,
              Super_Length (Left) + 1, Super_Length (Concat'Result)) =
              Super_To_String (Right)),
     Global => null;

   function Concat
     (Left  : Super_String;
      Right : String) return Super_String
   with
     Pre    => Right'Length <= Left.Max_Length - Super_Length (Left),
     Post   => Concat'Result.Max_Length = Left.Max_Length
       and then
         Super_Length (Concat'Result) = Super_Length (Left) + Right'Length
       and then
         Super_Slice (Concat'Result, 1, Super_Length (Left)) =
           Super_To_String (Left)
       and then
         (if Right'Length > 0 then
            Super_Slice (Concat'Result,
              Super_Length (Left) + 1, Super_Length (Concat'Result)) =
                Right),
     Global => null;

   function Concat
     (Left  : String;
      Right : Super_String) return Super_String
   with
     Pre    => Left'Length <= Right.Max_Length - Super_Length (Right),
     Post   => Concat'Result.Max_Length = Right.Max_Length
       and then
         Super_Length (Concat'Result) = Left'Length + Super_Length (Right)
       and then Super_Slice (Concat'Result, 1, Left'Length) = Left
       and then
         (if Super_Length (Right) > 0 then
            Super_Slice (Concat'Result,
              Left'Length + 1, Super_Length (Concat'Result)) =
                Super_To_String (Right)),
     Global => null;

   function Concat
     (Left  : Super_String;
      Right : Character) return Super_String
   with
     Pre    => Super_Length (Left) < Left.Max_Length,
     Post   => Concat'Result.Max_Length = Left.Max_Length
       and then Super_Length (Concat'Result) = Super_Length (Left) + 1
       and then
         Super_Slice (Concat'Result, 1, Super_Length (Left)) =
           Super_To_String (Left)
       and then Super_Element (Concat'Result, Super_Length (Left) + 1) = Right,
     Global => null;

   function Concat
     (Left  : Character;
      Right : Super_String) return Super_String
   with
     Pre    => Super_Length (Right) < Right.Max_Length,
     Post   => Concat'Result.Max_Length = Right.Max_Length
       and then Super_Length (Concat'Result) = 1 + Super_Length (Right)
       and then Super_Element (Concat'Result, 1) = Left
       and then
         Super_Slice (Concat'Result, 2, Super_Length (Concat'Result)) =
           Super_To_String (Right),
     Global => null;

   function Super_Element
     (Source : Super_String;
      Index  : Positive) return Character
   is (if Index <= Source.Current_Length
       then Source.Data (Index)
       else raise Index_Error)
   with Pre    => Index <= Super_Length (Source),
        Global => null;

   procedure Super_Replace_Element
     (Source : in out Super_String;
      Index  : Positive;
      By     : Character)
   with
     Pre    => Index <= Super_Length (Source),
     Post   => Super_Length (Source) = Super_Length (Source'Old)
       and then
         (for all K in 1 .. Super_Length (Source) =>
            Super_Element (Source, K) =
              (if K = Index then By else Super_Element (Source'Old, K))),
     Global => null;

   function Super_Slice
     (Source : Super_String;
      Low    : Positive;
      High   : Natural) return String
   is (if Low - 1 > Source.Current_Length or else High > Source.Current_Length

       --  Note: test of High > Length is in accordance with AI95-00128

       then raise Index_Error
       else
          --  Note: in this case, superflat bounds are not a problem, we just
          --  get the null string in accordance with normal Ada slice rules.

          String (Source.Data (Low .. High)))
   with Pre    => Low - 1 <= Super_Length (Source)
                    and then High <= Super_Length (Source),
        Global => null;

   function Super_Slice
     (Source : Super_String;
      Low    : Positive;
      High   : Natural) return Super_String
    with
     Pre    =>
       Low - 1 <= Super_Length (Source) and then High <= Super_Length (Source),
     Post   => Super_Slice'Result.Max_Length = Source.Max_Length
       and then
         Super_To_String (Super_Slice'Result) =
           Super_Slice (Source, Low, High),
     Global => null;

   procedure Super_Slice
     (Source : Super_String;
      Target : out Super_String;
      Low    : Positive;
      High   : Natural)
   with
     Pre    => Source.Max_Length = Target.Max_Length
       and then Low - 1 <= Super_Length (Source)
       and then High <= Super_Length (Source),
     Post   => Super_To_String (Target) = Super_Slice (Source, Low, High),
     Global => null;

   function "="
     (Left  : Super_String;
      Right : Super_String) return Boolean
   with
     Pre    => Left.Max_Length = Right.Max_Length,
     Post   => "="'Result = (Super_To_String (Left) = Super_To_String (Right)),
     Global => null;

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

   function Equal
     (Left  : Super_String;
      Right : String) return Boolean
   with
     Post   => Equal'Result = (Super_To_String (Left) = Right),
     Global => null;

   function Equal
     (Left  : String;
      Right : Super_String) return Boolean
   with
     Post   => Equal'Result = (Left = Super_To_String (Right)),
     Global => null;

   function Less
     (Left  : Super_String;
      Right : Super_String) return Boolean
   with
     Pre    => Left.Max_Length = Right.Max_Length,
     Post   =>
       Less'Result = (Super_To_String (Left) < Super_To_String (Right)),
     Global => null;

   function Less
     (Left  : Super_String;
      Right : String) return Boolean
   with
     Post   => Less'Result = (Super_To_String (Left) < Right),
     Global => null;

   function Less
     (Left  : String;
      Right : Super_String) return Boolean
   with
     Post   => Less'Result = (Left < Super_To_String (Right)),
     Global => null;

   function Less_Or_Equal
     (Left  : Super_String;
      Right : Super_String) return Boolean
   with
     Pre    => Left.Max_Length = Right.Max_Length,
     Post   =>
       Less_Or_Equal'Result =
         (Super_To_String (Left) <= Super_To_String (Right)),
     Global => null;

   function Less_Or_Equal
     (Left  : Super_String;
      Right : String) return Boolean
   with
     Post   => Less_Or_Equal'Result = (Super_To_String (Left) <= Right),
     Global => null;

   function Less_Or_Equal
     (Left  : String;
      Right : Super_String) return Boolean
   with
     Post   => Less_Or_Equal'Result = (Left <= Super_To_String (Right)),
     Global => null;

   function Greater
     (Left  : Super_String;
      Right : Super_String) return Boolean
   with
     Pre    => Left.Max_Length = Right.Max_Length,
     Post   =>
       Greater'Result = (Super_To_String (Left) > Super_To_String (Right)),
     Global => null;

   function Greater
     (Left  : Super_String;
      Right : String) return Boolean
   with
     Post   => Greater'Result = (Super_To_String (Left) > Right),
     Global => null;

   function Greater
     (Left  : String;
      Right : Super_String) return Boolean
   with
     Post   => Greater'Result = (Left > Super_To_String (Right)),
     Global => null;

   function Greater_Or_Equal
     (Left  : Super_String;
      Right : Super_String) return Boolean
   with
     Pre    => Left.Max_Length = Right.Max_Length,
     Post   =>
       Greater_Or_Equal'Result =
         (Super_To_String (Left) >= Super_To_String (Right)),
     Global => null;

   function Greater_Or_Equal
     (Left  : Super_String;
      Right : String) return Boolean
   with
     Post   => Greater_Or_Equal'Result = (Super_To_String (Left) >= Right),
     Global => null;

   function Greater_Or_Equal
     (Left  : String;
      Right : Super_String) return Boolean
   with
     Post   => Greater_Or_Equal'Result = (Left >= Super_To_String (Right)),
     Global => null;

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

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

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

       (Super_Length (Source) = 0
        =>
          Super_Index'Result = 0,

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

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

          Super_Index'Result in
            1 .. Super_Length (Source) - (Pattern'Length - 1)

            --  The slice beginning at the returned index matches Pattern

            and then Search.Match
              (Super_To_String (Source), Pattern, Mapping, Super_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 .. Super_Length (Source) =>
                 (if (if Going = Forward
                      then J <= Super_Index'Result - 1
                      else J - 1 in Super_Index'Result
                                    .. Super_Length (Source) - Pattern'Length)
                  then not (Search.Match
                    (Super_To_String (Source), Pattern, Mapping, J)))),

        --  Otherwise, 0 is returned

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

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

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

       (Super_Length (Source) = 0
        =>
          Super_Index'Result = 0,

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

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

          Super_Index'Result in
            1 .. Super_Length (Source) - (Pattern'Length - 1)

            --  The slice beginning at the returned index matches Pattern

            and then Search.Match
              (Super_To_String (Source), Pattern, Mapping, Super_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 .. Super_Length (Source) =>
                 (if (if Going = Forward
                      then J <= Super_Index'Result - 1
                      else J - 1 in Super_Index'Result
                                    .. Super_Length (Source) - Pattern'Length)
                  then not (Search.Match
                    (Super_To_String (Source), Pattern, Mapping, J)))),

        --  Otherwise, 0 is returned

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

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

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

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

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

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

          Super_Index'Result in 1 .. Super_Length (Source)

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

            and then
              (Test = Inside) =
                Maps.Is_In (Super_Element (Source, Super_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 .. Super_Length (Source) =>
                 (if J /= Super_Index'Result
                       and then (J < Super_Index'Result) = (Going = Forward)
                  then (Test = Inside)
                       /= Maps.Is_In (Super_Element (Source, J), Set)))),
     Global         => null;

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

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

       (Super_Length (Source) = 0
        =>
          Super_Index'Result = 0,

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

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

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

            --  The slice beginning at the returned index matches Pattern

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

        --  Otherwise, 0 is returned

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

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

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

       (Super_Length (Source) = 0
        =>
          Super_Index'Result = 0,

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

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

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

            --  The slice beginning at the returned index matches Pattern

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

        --  Otherwise, 0 is returned

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

   function Super_Index
     (Source : Super_String;
      Set    : Maps.Character_Set;
      From   : Positive;
      Test   : Membership := Inside;
      Going  : Direction := Forward) return Natural
   with
     Pre            =>
       (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
     Post           => Super_Index'Result <= Super_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.

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

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

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

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

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

            and then
              (Test = Inside) =
                Maps.Is_In (Super_Element (Source, Super_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 .. Super_Length (Source) =>
                 (if J /= Super_Index'Result
                    and then (J < Super_Index'Result) = (Going = Forward)
                    and then (J = From
                                or else (J > From) = (Going = Forward))
                  then (Test = Inside)
                       /= Maps.Is_In (Super_Element (Source, J), Set)))),
     Global         => null;

   function Super_Index_Non_Blank
     (Source : Super_String;
      Going  : Direction := Forward) return Natural
   with
     Post           => Super_Index_Non_Blank'Result <= Super_Length (Source),
     Contract_Cases =>

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

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

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

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

          Super_Index_Non_Blank'Result in 1 .. Super_Length (Source)

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

            and then
              Super_Element (Source, Super_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 .. Super_Length (Source) =>
                 (if J /= Super_Index_Non_Blank'Result
                       and then
                         (J < Super_Index_Non_Blank'Result) = (Going = Forward)
                  then Super_Element (Source, J) = ' '))),
     Global         => null;

   function Super_Index_Non_Blank
     (Source : Super_String;
      From   : Positive;
      Going  : Direction := Forward) return Natural
   with
     Pre            =>
       (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
     Post           => Super_Index_Non_Blank'Result <= Super_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.

       (Super_Length (Source) = 0
          or else
            (for all J in 1 .. Super_Length (Source) =>
               (if J = From or else (J > From) = (Going = Forward) then
                  Super_Element (Source, J) = ' '))
        =>
          Super_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

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

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

            and then
              Super_Element (Source, Super_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 .. Super_Length (Source) =>
                 (if J /= Super_Index_Non_Blank'Result
                    and then
                      (J < Super_Index_Non_Blank'Result) = (Going = Forward)
                    and then (J = From
                                or else (J > From) = (Going = Forward))
                  then Super_Element (Source, J) = ' '))),
     Global         => null;

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

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

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

   procedure Super_Find_Token
     (Source : Super_String;
      Set    : Maps.Character_Set;
      From   : Positive;
      Test   : Membership;
      First  : out Positive;
      Last   : out Natural)
   with
     Pre            =>
       (if Super_Length (Source) /= 0 then From <= Super_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.

       (Super_Length (Source) = 0
          or else
            (for all J in From .. Super_Length (Source) =>
               (Test = Inside) /= Maps.Is_In (Super_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 .. Super_Length (Source)
            and then Last in First .. Super_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 (Super_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 (Super_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 < Super_Length (Source)
               then
                 (Test = Inside) /=
                   Maps.Is_In (Super_Element (Source, Last + 1), Set))),
     Global         => null;

   procedure Super_Find_Token
     (Source : Super_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.

       (Super_Length (Source) = 0
          or else
            (for all J in 1 .. Super_Length (Source) =>
               (Test = Inside) /= Maps.Is_In (Super_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 .. Super_Length (Source)
            and then Last in First .. Super_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 (Super_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 (Super_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 < Super_Length (Source)
               then
                 (Test = Inside) /=
                   Maps.Is_In (Super_Element (Source, Last + 1), Set))),
     Global         => null;

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

   function Super_Translate
     (Source  : Super_String;
      Mapping : Maps.Character_Mapping) return Super_String
   with
     Post   => Super_Translate'Result.Max_Length = Source.Max_Length
       and then Super_Length (Super_Translate'Result) = Super_Length (Source)
       and then
         (for all K in 1 .. Super_Length (Source) =>
            Super_Element (Super_Translate'Result, K) =
              Ada.Strings.Maps.Value (Mapping, Super_Element (Source, K))),
     Global => null;

   procedure Super_Translate
     (Source   : in out Super_String;
      Mapping  : Maps.Character_Mapping)
   with
     Post   => Super_Length (Source) = Super_Length (Source'Old)
       and then
         (for all K in 1 .. Super_Length (Source) =>
            Super_Element (Source, K) =
              Ada.Strings.Maps.Value (Mapping, Super_Element (Source'Old, K))),
     Global => null;

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

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

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

   function Super_Replace_Slice
     (Source : Super_String;
      Low    : Positive;
      High   : Natural;
      By     : String;
      Drop   : Truncation := Error) return Super_String
   with
     Pre            =>
       Low - 1 <= Super_Length (Source)
         and then
           (if Drop = Error
              then (if High >= Low
                      then Low - 1
                        <= Source.Max_Length - By'Length
                         - Integer'Max (Super_Length (Source) - High, 0)
                      else Super_Length (Source) <=
                             Source.Max_Length - By'Length)),
     Post           =>
       Super_Replace_Slice'Result.Max_Length = Source.Max_Length,
     Contract_Cases =>
       (Low - 1 <= Source.Max_Length - By'Length - Integer'Max
          (Super_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).

          Super_Length (Super_Replace_Slice'Result) =
            Low - 1 + By'Length + Integer'Max
              (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
            and then
              String'(Super_Slice (Super_Replace_Slice'Result, 1, Low - 1)) =
                Super_Slice (Source, 1, Low - 1)
            and then
              Super_Slice (Super_Replace_Slice'Result,
                Low, Low - 1 + By'Length) = By
            and then
              (if Integer'Max (High, Low - 1) < Super_Length (Source) then
                 String'(Super_Slice (Super_Replace_Slice'Result,
                   Low + By'Length,
                   Super_Length (Super_Replace_Slice'Result))) =
                     Super_Slice (Source,
                       Integer'Max (High + 1, Low), Super_Length (Source))),

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

             Super_Length (Super_Replace_Slice'Result) = Source.Max_Length
               and then
                 (if Final_Super_Slice > 0 then
                    String'(Super_Slice (Super_Replace_Slice'Result,
                      Source.Max_Length - Final_Super_Slice + 1,
                      Source.Max_Length)) =
                        Super_Slice (Source,
                          Integer'Max (High + 1, Low), Super_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 Source.Max_Length - Final_Super_Slice - By'Length <= 0 then

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

                   (if Final_Super_Slice < Source.Max_Length then
                      Super_Slice (Super_Replace_Slice'Result,
                        1, Source.Max_Length - Final_Super_Slice) =
                          By (By'Last - Source.Max_Length + Final_Super_Slice
                                + 1
                              .. By'Last))

                 else  --  By is added to the result

                   Super_Slice (Super_Replace_Slice'Result,
                     Source.Max_Length - Final_Super_Slice - By'Length + 1,
                     Source.Max_Length - Final_Super_Slice) =
                       By

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

                     and then
                       String'(Super_Slice (Super_Replace_Slice'Result, 1,
                         Source.Max_Length - Final_Super_Slice - By'Length)) =
                           Super_Slice (Source,
                             Low - Source.Max_Length
                               + Final_Super_Slice + By'Length,
                             Low - 1))),

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

          Super_Length (Super_Replace_Slice'Result) = Source.Max_Length
            and then
              String'(Super_Slice (Super_Replace_Slice'Result, 1, Low - 1)) =
                Super_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 >= Source.Max_Length - By'Length then

                 --  The last characters of By are dropped

                 Super_Slice (Super_Replace_Slice'Result,
                   Low, Source.Max_Length) =
                     By (By'First .. Source.Max_Length - Low + By'First)

               else  --  By is fully added

                 Super_Slice (Super_Replace_Slice'Result,
                   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
                     String'(Super_Slice (Super_Replace_Slice'Result,
                       Low + By'Length, Source.Max_Length)) =
                         Super_Slice (Source, Integer'Max (High + 1, Low),
                           Integer'Max (High + 1, Low) +
                             (Source.Max_Length - Low - By'Length)))),
     Global         => null;

   procedure Super_Replace_Slice
     (Source  : in out Super_String;
      Low     : Positive;
      High    : Natural;
      By      : String;
      Drop    : Truncation := Error)
   with
     Pre            =>
       Low - 1 <= Super_Length (Source)
         and then
           (if Drop = Error
              then (if High >= Low
                      then Low - 1
                        <= Source.Max_Length - By'Length
                         - Natural'Max (Super_Length (Source) - High, 0)
                      else Super_Length (Source) <=
                             Source.Max_Length - By'Length)),
     Contract_Cases =>
       (Low - 1 <= Source.Max_Length - By'Length - Integer'Max
          (Super_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).

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

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

             Super_Length (Source) = Source.Max_Length
               and then
                 (if Final_Super_Slice > 0 then
                    String'(Super_Slice (Source,
                      Source.Max_Length - Final_Super_Slice + 1,
                      Source.Max_Length)) =
                        Super_Slice (Source'Old,
                          Integer'Max (High + 1, Low),
                          Super_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 Source.Max_Length - Final_Super_Slice - By'Length <= 0
                  then
                    --  The first characters of By are dropped

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

                  else  --  By is added to the result

                    Super_Slice (Source,
                      Source.Max_Length - Final_Super_Slice - By'Length + 1,
                      Source.Max_Length - Final_Super_Slice) = By

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

                      and then
                        String'(Super_Slice (Source, 1,
                          Source.Max_Length - Final_Super_Slice - By'Length)) =
                            Super_Slice (Source'Old,
                              Low - Source.Max_Length + Final_Super_Slice
                                + By'Length,
                              Low - 1))),

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

          Super_Length (Source) = Source.Max_Length
            and then
              String'(Super_Slice (Source, 1, Low - 1)) =
                Super_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 >= Source.Max_Length - By'Length then

                 --  The last characters of By are dropped

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

               else  --  By is fully added

                 Super_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
                     String'(Super_Slice (Source,
                       Low + By'Length, Source.Max_Length)) =
                         Super_Slice (Source'Old, Integer'Max (High + 1, Low),
                           Integer'Max (High + 1, Low) +
                             (Source.Max_Length - Low - By'Length)))),
     Global         => null;

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

          Super_Length (Super_Insert'Result) =
            Super_Length (Source) + New_Item'Length
            and then
              String'(Super_Slice (Super_Insert'Result, 1, Before - 1)) =
                Super_Slice (Source, 1, Before - 1)
            and then
              Super_Slice (Super_Insert'Result,
                Before, Before - 1 + New_Item'Length) =
                  New_Item
            and then
              (if Before <= Super_Length (Source) then
                 String'(Super_Slice (Super_Insert'Result,
                   Before + New_Item'Length,
                   Super_Length (Super_Insert'Result))) =
                     Super_Slice (Source, Before, Super_Length (Source))),

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

          Super_Length (Super_Insert'Result) = Source.Max_Length
            and then
              (if Before <= Super_Length (Source) then
                 String'(Super_Slice (Super_Insert'Result,
                   Source.Max_Length - Super_Length (Source) + Before,
                   Source.Max_Length)) =
                     Super_Slice (Source, Before, Super_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 Source.Max_Length - Super_Length (Source) - 1 + Before
                < New_Item'Length
               then
                 --  The first characters of New_Item are dropped

                 (if Super_Length (Source) - Before + 1 < Source.Max_Length
                  then
                    Super_Slice (Super_Insert'Result, 1,
                      Source.Max_Length - Super_Length (Source) - 1 + Before) =
                        New_Item
                          (New_Item'Last - Source.Max_Length
                            + Super_Length (Source) - Before + 2
                           .. New_Item'Last))

               else  --  New_Item is added to the result

                 Super_Slice (Super_Insert'Result,
                   Source.Max_Length - Super_Length (Source) - New_Item'Length
                     + Before,
                   Source.Max_Length - Super_Length (Source) - 1 + Before) =
                     New_Item

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

                   and then
                     String'(Super_Slice (Super_Insert'Result,
                       1, Source.Max_Length - Super_Length (Source)
                         - New_Item'Length - 1 + Before)) =
                           Super_Slice (Source,
                             Super_Length (Source) - 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.

          Super_Length (Super_Insert'Result) = Source.Max_Length
            and then
              String'(Super_Slice (Super_Insert'Result, 1, Before - 1)) =
                Super_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 >= Source.Max_Length - New_Item'Length then

                 --  The last characters of New_Item are dropped

                 Super_Slice (Super_Insert'Result, Before, Source.Max_Length) =
                   New_Item (New_Item'First
                     .. Source.Max_Length - Before + New_Item'First)

               else  --  New_Item is fully added

                 Super_Slice (Super_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
                     String'(Super_Slice (Super_Insert'Result,
                       Before + New_Item'Length, Source.Max_Length)) =
                         Super_Slice (Source,
                           Before, Source.Max_Length - New_Item'Length))),
     Global         => null;

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

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

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

          Super_Length (Source) = Source.Max_Length
            and then
              (if Before <= Super_Length (Source'Old) then
                 String'(Super_Slice (Source,
                   Source.Max_Length - Super_Length (Source'Old) + Before,
                   Source.Max_Length)) =
                     Super_Slice (Source'Old,
                       Before, Super_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 Source.Max_Length - Super_Length (Source'Old) - 1 + Before
                < New_Item'Length
               then
                 --  The first characters of New_Item are dropped

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

               else  --  New_Item is added to the result

                 Super_Slice (Source,
                   Source.Max_Length - Super_Length (Source'Old)
                     - New_Item'Length + Before,
                   Source.Max_Length - Super_Length (Source'Old) - 1 + Before)
                     = New_Item

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

                   and then
                     String'(Super_Slice (Source, 1,
                       Source.Max_Length - Super_Length (Source'Old)
                         - New_Item'Length - 1 + Before)) =
                           Super_Slice (Source'Old,
                             Super_Length (Source'Old)
                               - 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.

          Super_Length (Source) = Source.Max_Length
            and then
              String'(Super_Slice (Source, 1, Before - 1)) =
                Super_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 >= Source.Max_Length - New_Item'Length then

                 --  The last characters of New_Item are dropped

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

               else  --  New_Item is fully added

                 Super_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
                     String'(Super_Slice (Source,
                       Before + New_Item'Length, Source.Max_Length)) =
                         Super_Slice (Source'Old,
                           Before, Source.Max_Length - New_Item'Length))),
     Global         => null;

   function Super_Overwrite
     (Source   : Super_String;
      Position : Positive;
      New_Item : String;
      Drop     : Truncation := Error) return Super_String
   with
     Pre            =>
       Position - 1 <= Super_Length (Source)
         and then (if New_Item'Length > Source.Max_Length - (Position - 1)
                   then Drop /= Error),
     Post           => Super_Overwrite'Result.Max_Length = Source.Max_Length,
     Contract_Cases =>
       (Position - 1 <= Source.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.

          Super_Length (Super_Overwrite'Result) =
            Integer'Max (Super_Length (Source), Position - 1 + New_Item'Length)
            and then
              String'(Super_Slice (Super_Overwrite'Result, 1, Position - 1)) =
                Super_Slice (Source, 1, Position - 1)
            and then Super_Slice (Super_Overwrite'Result,
              Position, Position - 1 + New_Item'Length) =
                New_Item
            and then
              (if Position - 1 + New_Item'Length < Super_Length (Source) then

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

                 String'(Super_Slice (Super_Overwrite'Result,
                   Position + New_Item'Length, Super_Length (Source))) =
                     Super_Slice (Source,
                       Position + New_Item'Length, Super_Length (Source))),

        Position - 1 > Source.Max_Length - New_Item'Length and then Drop = Left
        =>
          Super_Length (Super_Overwrite'Result) = 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 >= Source.Max_Length then

                 --  New_Item covers all Max_Length characters

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

                 Super_Slice (Super_Overwrite'Result,
                   Source.Max_Length - New_Item'Length + 1,
                   Source.Max_Length) =
                     New_Item

                   --  The left of Source is cut

                   and then
                     String'(Super_Slice (Super_Overwrite'Result,
                       1, Source.Max_Length - New_Item'Length)) =
                         Super_Slice (Source,
                           Position - Source.Max_Length + New_Item'Length,
                           Position - 1)),

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

          Super_Length (Super_Overwrite'Result) = Source.Max_Length
            and then
              String'(Super_Slice (Super_Overwrite'Result, 1, Position - 1)) =
                Super_Slice (Source, 1, Position - 1)

            --  Then New_Item is written until Max_Length

            and then Super_Slice (Super_Overwrite'Result,
              Position, Source.Max_Length) =
                New_Item (New_Item'First
                          .. Source.Max_Length - Position + New_Item'First)),
     Global         => null;

   procedure Super_Overwrite
     (Source    : in out Super_String;
      Position  : Positive;
      New_Item  : String;
      Drop      : Truncation := Error)
   with
     Pre            =>
       Position - 1 <= Super_Length (Source)
         and then (if New_Item'Length > Source.Max_Length - (Position - 1)
                   then Drop /= Error),
     Contract_Cases =>
       (Position - 1 <= Source.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.

          Super_Length (Source) = Integer'Max
            (Super_Length (Source'Old), Position - 1 + New_Item'Length)
            and then
              String'(Super_Slice (Source, 1, Position - 1)) =
                Super_Slice (Source'Old, 1, Position - 1)
            and then Super_Slice (Source,
              Position, Position - 1 + New_Item'Length) =
                New_Item
            and then
              (if Position - 1 + New_Item'Length < Super_Length (Source'Old)
               then
                 --  There are some unchanged characters of Source remaining
                 --  after New_Item.

                 String'(Super_Slice (Source,
                   Position + New_Item'Length, Super_Length (Source'Old))) =
                     Super_Slice (Source'Old,
                       Position + New_Item'Length, Super_Length (Source'Old))),

        Position - 1 > Source.Max_Length - New_Item'Length and then Drop = Left
        =>
          Super_Length (Source) = 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 >= Source.Max_Length then

                 --  New_Item covers all Max_Length characters

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

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

                   --  The left of Source is cut

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

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

          Super_Length (Source) = Source.Max_Length
            and then
              String'(Super_Slice (Source, 1, Position - 1)) =
                Super_Slice (Source'Old, 1, Position - 1)

            --  New_Item is written until Max_Length

            and then Super_Slice (Source, Position, Source.Max_Length) =
              New_Item (New_Item'First
                        .. Source.Max_Length - Position + New_Item'First)),
     Global         => null;

   function Super_Delete
     (Source  : Super_String;
      From    : Positive;
      Through : Natural) return Super_String
   with
     Pre            =>
       (if Through >= From then From - 1 <= Super_Length (Source)),
     Post           => Super_Delete'Result.Max_Length = Source.Max_Length,
     Contract_Cases =>
       (Through >= From =>
          Super_Length (Super_Delete'Result) =
            From - 1 + Natural'Max (Super_Length (Source) - Through, 0)
            and then
              String'(Super_Slice (Super_Delete'Result, 1, From - 1)) =
                Super_Slice (Source, 1, From - 1)
            and then
              (if Through < Super_Length (Source) then
                 String'(Super_Slice (Super_Delete'Result,
                   From, Super_Length (Super_Delete'Result))) =
                     Super_Slice (Source, Through + 1, Super_Length (Source))),
        others          =>
          Super_Delete'Result = Source),
     Global         => null;

   procedure Super_Delete
     (Source  : in out Super_String;
      From    : Positive;
      Through : Natural)
   with
     Pre            =>
       (if Through >= From then From - 1 <= Super_Length (Source)),
     Contract_Cases =>
       (Through >= From =>
          Super_Length (Source) =
            From - 1 + Natural'Max (Super_Length (Source'Old) - Through, 0)
            and then
              String'(Super_Slice (Source, 1, From - 1)) =
                Super_Slice (Source'Old, 1, From - 1)
            and then
              (if Through < Super_Length (Source) then
                 String'(Super_Slice (Source, From, Super_Length (Source))) =
                   Super_Slice (Source'Old,
                     Through + 1, Super_Length (Source'Old))),
        others          =>
          Source = Source'Old),
     Global         => null;

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

   function Super_Trim
     (Source : Super_String;
      Side   : Trim_End) return Super_String
   with
     Post           => Super_Trim'Result.Max_Length = Source.Max_Length,
     Contract_Cases =>

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

       ((for all C of Super_To_String (Source) => C = ' ')
        =>
          Super_Length (Super_Trim'Result) = 0,

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

        others
        =>
          (declare
             Low  : constant Positive :=
               (if Side = Right then 1
                else Super_Index_Non_Blank (Source, Forward));
             High : constant Positive :=
               (if Side = Left then Super_Length (Source)
                else Super_Index_Non_Blank (Source, Backward));
           begin
             Super_To_String (Super_Trim'Result) =
               Super_Slice (Source, Low, High))),
     Global         => null;

   procedure Super_Trim
     (Source : in out Super_String;
      Side   : Trim_End)
   with
     Contract_Cases =>

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

       ((for all C of Super_To_String (Source) => C = ' ')
        =>
          Super_Length (Source) = 0,

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

        others
        =>
          (declare
             Low  : constant Positive :=
               (if Side = Right then 1
                else Super_Index_Non_Blank (Source'Old, Forward));
             High : constant Positive :=
               (if Side = Left then Super_Length (Source'Old)
                else Super_Index_Non_Blank (Source'Old, Backward));
           begin
             Super_To_String (Source) = Super_Slice (Source'Old, Low, High))),
     Global => null;

   function Super_Trim
     (Source : Super_String;
      Left   : Maps.Character_Set;
      Right  : Maps.Character_Set) return Super_String
   with
     Post           => Super_Trim'Result.Max_Length = Source.Max_Length,
     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 Super_To_String (Source) => Maps.Is_In (C, Left))
          or else
            (for all C of Super_To_String (Source) => Maps.Is_In (C, Right))
        =>
          Super_Length (Super_Trim'Result) = 0,

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

        others
        =>
          (declare
             Low  : constant Positive :=
               Super_Index (Source, Left, Outside, Forward);
             High : constant Positive :=
               Super_Index (Source, Right, Outside, Backward);
           begin
             Super_To_String (Super_Trim'Result) =
               Super_Slice (Source, Low, High))),
     Global         => null;

   procedure Super_Trim
     (Source : in out Super_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 Super_To_String (Source) => Maps.Is_In (C, Left))
          or else
            (for all C of Super_To_String (Source) => Maps.Is_In (C, Right))
        =>
          Super_Length (Source) = 0,

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

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

   function Super_Head
     (Source : Super_String;
      Count  : Natural;
      Pad    : Character := Space;
      Drop   : Truncation := Error) return Super_String
   with
     Pre            => (if Count > Source.Max_Length then Drop /= Error),
     Post           => Super_Head'Result.Max_Length = Source.Max_Length,
     Contract_Cases =>
       (Count <= Super_Length (Source)
        =>
          --  Source is cut

          Super_To_String (Super_Head'Result) = Super_Slice (Source, 1, Count),
        Count > Super_Length (Source) and then Count <= Source.Max_Length
        =>
          --  Source is followed by Pad characters

          Super_Length (Super_Head'Result) = Count
            and then
              Super_Slice (Super_Head'Result, 1, Super_Length (Source)) =
                Super_To_String (Source)
            and then
              String'(Super_Slice (Super_Head'Result,
                Super_Length (Source) + 1, Count)) =
                  [1 .. Count - Super_Length (Source) => Pad],
        Count > Source.Max_Length and then Drop = Right
        =>
          --  Source is followed by Pad characters

          Super_Length (Super_Head'Result) = Source.Max_Length
            and then
              Super_Slice (Super_Head'Result, 1, Super_Length (Source)) =
                Super_To_String (Source)
            and then
              String'(Super_Slice (Super_Head'Result,
                Super_Length (Source) + 1, Source.Max_Length)) =
                  [1 .. Source.Max_Length - Super_Length (Source) => Pad],
        Count - Super_Length (Source) > Source.Max_Length and then Drop = Left
        =>
          --  Source is fully dropped on the left

          Super_To_String (Super_Head'Result) =
            [1 .. Source.Max_Length => Pad],
        others
        =>
          --  Source is partly dropped on the left

          Super_Length (Super_Head'Result) = Source.Max_Length
            and then
              String'(Super_Slice (Super_Head'Result,
                1, Source.Max_Length - Count + Super_Length (Source))) =
                  Super_Slice (Source,
                    Count - Source.Max_Length + 1, Super_Length (Source))
            and then
              String'(Super_Slice (Super_Head'Result,
                Source.Max_Length - Count + Super_Length (Source) + 1,
                Source.Max_Length)) =
                  [1 .. Count - Super_Length (Source) => Pad]),
     Global         => null;

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

          Super_To_String (Source) = Super_Slice (Source'Old, 1, Count),
        Count > Super_Length (Source) and then Count <= Source.Max_Length
        =>
          --  Source is followed by Pad characters

          Super_Length (Source) = Count
            and then
              Super_Slice (Source, 1, Super_Length (Source'Old)) =
                Super_To_String (Source'Old)
            and then
              String'(Super_Slice (Source,
                Super_Length (Source'Old) + 1, Count)) =
                  [1 .. Count - Super_Length (Source'Old) => Pad],
        Count > Source.Max_Length and then Drop = Right
        =>
          --  Source is followed by Pad characters

          Super_Length (Source) = Source.Max_Length
            and then
              Super_Slice (Source, 1, Super_Length (Source'Old)) =
                Super_To_String (Source'Old)
            and then
              String'(Super_Slice (Source,
                Super_Length (Source'Old) + 1, Source.Max_Length)) =
                  [1 .. Source.Max_Length - Super_Length (Source'Old) => Pad],
        Count - Super_Length (Source) > Source.Max_Length and then Drop = Left
        =>
          --  Source is fully dropped on the left

          Super_To_String (Source) = [1 .. Source.Max_Length => Pad],
        others
        =>
          --  Source is partly dropped on the left

          Super_Length (Source) = Source.Max_Length
            and then
              String'(Super_Slice (Source,
                1, Source.Max_Length - Count + Super_Length (Source'Old))) =
                  Super_Slice (Source'Old,
                    Count - Source.Max_Length + 1, Super_Length (Source'Old))
            and then
              String'(Super_Slice (Source,
                Source.Max_Length - Count + Super_Length (Source'Old) + 1,
                Source.Max_Length)) =
                  [1 .. Count - Super_Length (Source'Old) => Pad]),
     Global         => null;

   function Super_Tail
     (Source : Super_String;
      Count  : Natural;
      Pad    : Character := Space;
      Drop   : Truncation := Error) return Super_String
   with
     Pre            => (if Count > Source.Max_Length then Drop /= Error),
     Post           => Super_Tail'Result.Max_Length = Source.Max_Length,
     Contract_Cases =>
       (Count < Super_Length (Source)
        =>
          --  Source is cut

          (if Count > 0 then
             Super_To_String (Super_Tail'Result) =
               Super_Slice (Source,
                 Super_Length (Source) - Count + 1, Super_Length (Source))
           else Super_Length (Super_Tail'Result) = 0),
        Count >= Super_Length (Source) and then Count < Source.Max_Length
        =>
          --  Source is preceded by Pad characters

          Super_Length (Super_Tail'Result) = Count
            and then
              String'(Super_Slice (Super_Tail'Result,
                1, Count - Super_Length (Source))) =
                  [1 .. Count - Super_Length (Source) => Pad]
            and then
              Super_Slice (Super_Tail'Result,
                Count - Super_Length (Source) + 1, Count) =
                  Super_To_String (Source),
        Count >= Source.Max_Length and then Drop = Left
        =>
          --  Source is preceded by Pad characters

          Super_Length (Super_Tail'Result) = Source.Max_Length
            and then
              String'(Super_Slice (Super_Tail'Result,
                1, Source.Max_Length - Super_Length (Source))) =
                  [1 .. Source.Max_Length - Super_Length (Source) => Pad]
            and then
              (if Super_Length (Source) > 0 then
                 Super_Slice (Super_Tail'Result,
                   Source.Max_Length - Super_Length (Source) + 1,
                   Source.Max_Length) =
                     Super_To_String (Source)),
        Count - Super_Length (Source) >= Source.Max_Length
          and then Drop /= Left
        =>
          --  Source is fully dropped on the right

          Super_To_String (Super_Tail'Result) =
            [1 .. Source.Max_Length => Pad],
        others
        =>
          --  Source is partly dropped on the right

          Super_Length (Super_Tail'Result) = Source.Max_Length
            and then
              String'(Super_Slice (Super_Tail'Result,
                1, Count - Super_Length (Source))) =
                  [1 .. Count - Super_Length (Source) => Pad]
            and then
              String'(Super_Slice (Super_Tail'Result,
                Count - Super_Length (Source) + 1, Source.Max_Length)) =
                  Super_Slice (Source,
                    1, Source.Max_Length - Count + Super_Length (Source))),
     Global         => null;

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

          (if Count > 0 then
             Super_To_String (Source) =
               Super_Slice (Source'Old,
                 Super_Length (Source'Old) - Count + 1,
                 Super_Length (Source'Old))
           else Super_Length (Source) = 0),
        Count >= Super_Length (Source) and then Count < Source.Max_Length
        =>
          --  Source is preceded by Pad characters

          Super_Length (Source) = Count
            and then
              String'(Super_Slice (Source,
                1, Count - Super_Length (Source'Old))) =
                  [1 .. Count - Super_Length (Source'Old) => Pad]
            and then
              Super_Slice (Source,
                Count - Super_Length (Source'Old) + 1, Count) =
                  Super_To_String (Source'Old),
        Count >= Source.Max_Length and then Drop = Left
        =>
          --  Source is preceded by Pad characters

          Super_Length (Source) = Source.Max_Length
            and then
              String'(Super_Slice (Source,
                1, Source.Max_Length - Super_Length (Source'Old))) =
                  [1 .. Source.Max_Length - Super_Length (Source'Old) => Pad]
            and then
              (if Super_Length (Source'Old) > 0 then
                 Super_Slice (Source,
                   Source.Max_Length - Super_Length (Source'Old) + 1,
                   Source.Max_Length) =
                     Super_To_String (Source'Old)),
        Count - Super_Length (Source) >= Source.Max_Length
          and then Drop /= Left
        =>
          --  Source is fully dropped on the right

          Super_To_String (Source) = [1 .. Source.Max_Length => Pad],
        others
        =>
          --  Source is partly dropped on the right

          Super_Length (Source) = Source.Max_Length
            and then
              String'(Super_Slice (Source,
                1, Count - Super_Length (Source'Old))) =
                  [1 .. Count - Super_Length (Source'Old) => Pad]
            and then
              String'(Super_Slice (Source,
                Count - Super_Length (Source'Old) + 1, Source.Max_Length)) =
                  Super_Slice (Source'Old,
                    1, Source.Max_Length - Count + Super_Length (Source'Old))),
     Global         => null;

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

   --  Note: in some of the following routines, there is an extra parameter
   --  Max_Length which specifies the value of the maximum length for the
   --  resulting Super_String value.

   function Times
     (Left       : Natural;
      Right      : Character;
      Max_Length : Positive) return Super_String
   with
     Pre    => Left <= Max_Length,
     Post   => Times'Result.Max_Length = Max_Length
       and then Super_To_String (Times'Result) = [1 .. Left => Right],
     Global => null;
   --  Note the additional parameter Max_Length

   function Times
     (Left       : Natural;
      Right      : String;
      Max_Length : Positive) return Super_String
   with
     Pre    => (if Left /= 0 then Right'Length <= Max_Length / Left),
     Post   => Times'Result.Max_Length = Max_Length
       and then Super_Length (Times'Result) = Left * Right'Length
       and then
         (if Right'Length > 0 then
            (for all K in 1 .. Left * Right'Length =>
               Super_Element (Times'Result, K) =
                 Right (Right'First + (K - 1) mod Right'Length))),
     Global => null;
   --  Note the additional parameter Max_Length

   function Times
     (Left  : Natural;
      Right : Super_String) return Super_String
   with
     Pre    =>
       (if Left /= 0 then Super_Length (Right) <= Right.Max_Length / Left),
     Post   => Times'Result.Max_Length = Right.Max_Length
       and then Super_Length (Times'Result) = Left * Super_Length (Right)
       and then
         (if Super_Length (Right) > 0 then
            (for all K in 1 .. Left * Super_Length (Right) =>
               Super_Element (Times'Result, K) =
                 Super_Element (Right, 1 + (K - 1) mod Super_Length (Right)))),
     Global => null;

   function Super_Replicate
     (Count      : Natural;
      Item       : Character;
      Drop       : Truncation := Error;
      Max_Length : Positive) return Super_String
   with
     Pre    => (if Count > Max_Length then Drop /= Error),
     Post   => Super_Replicate'Result.Max_Length = Max_Length
       and then Super_To_String (Super_Replicate'Result) =
         [1 .. Natural'Min (Max_Length, Count) => Item],
     Global => null;
   --  Note the additional parameter Max_Length

   function Super_Replicate
     (Count      : Natural;
      Item       : String;
      Drop       : Truncation := Error;
      Max_Length : Positive) return Super_String
   with
     Pre            =>
       (if Count /= 0 and then Item'Length > Max_Length / Count
        then Drop /= Error),
     Post           => Super_Replicate'Result.Max_Length = Max_Length,
     Contract_Cases =>
       (Count = 0 or else Item'Length <= Max_Length / Count
        =>
          Super_Length (Super_Replicate'Result) = Count * Item'Length
            and then
              (if Item'Length > 0 then
                 (for all K in 1 .. Count * Item'Length =>
                    Super_Element (Super_Replicate'Result, K) =
                      Item (Item'First + (K - 1) mod Item'Length))),
        Count /= 0
          and then Item'Length > Max_Length / Count
          and then Drop = Right
        =>
          Super_Length (Super_Replicate'Result) = Max_Length
            and then
              (for all K in 1 .. Max_Length =>
                 Super_Element (Super_Replicate'Result, K) =
                   Item (Item'First + (K - 1) mod Item'Length)),
        others  --  Drop = Left
        =>
          Super_Length (Super_Replicate'Result) = Max_Length
            and then
              (for all K in 1 .. Max_Length =>
                 Super_Element (Super_Replicate'Result, K) =
                   Item (Item'Last - (Max_Length - K) mod Item'Length))),
     Global         => null;
   --  Note the additional parameter Max_Length

   function Super_Replicate
     (Count : Natural;
      Item  : Super_String;
      Drop  : Truncation := Error) return Super_String
   with
     Pre            =>
       (if Count /= 0
          and then Super_Length (Item) > Item.Max_Length / Count
        then Drop /= Error),
     Post           => Super_Replicate'Result.Max_Length = Item.Max_Length,
     Contract_Cases =>
       ((if Count /= 0 then Super_Length (Item) <= Item.Max_Length / Count)
        =>
          Super_Length (Super_Replicate'Result) = Count * Super_Length (Item)
            and then
              (if Super_Length (Item) > 0 then
                 (for all K in 1 .. Count * Super_Length (Item) =>
                    Super_Element (Super_Replicate'Result, K) =
                      Super_Element (Item,
                        1 + (K - 1) mod Super_Length (Item)))),
        Count /= 0
          and then Super_Length (Item) > Item.Max_Length / Count
          and then Drop = Right
        =>
          Super_Length (Super_Replicate'Result) = Item.Max_Length
            and then
              (for all K in 1 .. Item.Max_Length =>
                 Super_Element (Super_Replicate'Result, K) =
                   Super_Element (Item, 1 + (K - 1) mod Super_Length (Item))),
        others  --  Drop = Left
        =>
          Super_Length (Super_Replicate'Result) = Item.Max_Length
            and then
              (for all K in 1 .. Item.Max_Length =>
                 Super_Element (Super_Replicate'Result, K) =
                   Super_Element (Item,
                     Super_Length (Item)
                       - (Item.Max_Length - K) mod Super_Length (Item)))),
     Global         => null;

   procedure Put_Image
     (S      : in out Ada.Strings.Text_Buffers.Root_Buffer_Type'Class;
      Source : Super_String);

private
      --  Pragma Inline declarations

      pragma Inline ("=");
      pragma Inline (Less);
      pragma Inline (Less_Or_Equal);
      pragma Inline (Greater);
      pragma Inline (Greater_Or_Equal);
      pragma Inline (Concat);
      pragma Inline (Super_Count);
      pragma Inline (Super_Element);
      pragma Inline (Super_Find_Token);
      pragma Inline (Super_Index);
      pragma Inline (Super_Index_Non_Blank);
      pragma Inline (Super_Length);
      pragma Inline (Super_Replace_Element);
      pragma Inline (Super_Slice);
      pragma Inline (Super_To_String);

end Ada.Strings.Superbounded;