gcc/ada/libgnat/a-strunb.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                 A D A . S T R I N G S . U N B O U N D E D                --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-2020, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- This specification is derived from the Ada Reference Manual for use with --
  12 -- GNAT. The copyright notice above, and the license provisions that follow --
  13 -- apply solely to the  contents of the part following the private keyword. --
  14 --                                                                          --
  15 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  16 -- terms of the  GNU General Public License as published  by the Free Soft- --
  17 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  18 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  19 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  20 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  21 --                                                                          --
  22 -- As a special exception under Section 7 of GPL version 3, you are granted --
  23 -- additional permissions described in the GCC Runtime Library Exception,   --
  24 -- version 3.1, as published by the Free Software Foundation.               --
  25 --                                                                          --
  26 -- You should have received a copy of the GNU General Public License and    --
  27 -- a copy of the GCC Runtime Library Exception along with this program;     --
  28 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  29 -- <http://www.gnu.org/licenses/>.                                          --
  30 --                                                                          --
  31 -- GNAT was originally developed  by the GNAT team at  New York University. --
  32 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  33 --                                                                          --
  34 ------------------------------------------------------------------------------
  35
  36 --  Preconditions in this unit are meant for analysis only, not for run-time
  37 --  checking, so that the expected exceptions are raised. This is enforced by
  38 --  setting the corresponding assertion policy to Ignore.
  39
  40 pragma Assertion_Policy (Pre => Ignore);
  41
  42 with Ada.Strings.Maps;
  43 with Ada.Finalization;
  44
  45 --  The language-defined package Strings.Unbounded provides a private type
  46 --  Unbounded_String and a set of operations. An object of type
  47 --  Unbounded_String represents a String whose low bound is 1 and whose length
  48 --  can vary conceptually between 0 and Natural'Last. The subprograms for
  49 --  fixed-length string handling are either overloaded directly for
  50 --  Unbounded_String, or are modified as needed to reflect the flexibility in
  51 --  length. Since the Unbounded_String type is private, relevant constructor
  52 --  and selector operations are provided.
  53
  54 package Ada.Strings.Unbounded with
  55   Initial_Condition => Length (Null_Unbounded_String) = 0
  56 is
  57    pragma Preelaborate;
  58
  59    type Unbounded_String is private;
  60    pragma Preelaborable_Initialization (Unbounded_String);
  61
  62    Null_Unbounded_String : constant Unbounded_String;
  63    --  Represents the null String. If an object of type Unbounded_String is not
  64    --  otherwise initialized, it will be initialized to the same value as
  65    --  Null_Unbounded_String.
  66
  67    function Length (Source : Unbounded_String) return Natural with
  68      Global => null;
  69    --  Returns the length of the String represented by Source
  70
  71    type String_Access is access all String;
  72    --  Provides a (nonprivate) access type for explicit processing of
  73    --  unbounded-length strings.
  74
  75    procedure Free (X : in out String_Access);
  76    --  Performs an unchecked deallocation of an object of type String_Access
  77
  78    --------------------------------------------------------
  79    -- Conversion, Concatenation, and Selection Functions --
  80    --------------------------------------------------------
  81
  82    function To_Unbounded_String
  83      (Source : String) return Unbounded_String
  84    with
  85      Post   => Length (To_Unbounded_String'Result) = Source'Length,
  86      Global => null;
  87    --  Returns an Unbounded_String that represents Source
  88
  89    function To_Unbounded_String
  90      (Length : Natural) return Unbounded_String
  91    with
  92      Post   =>
  93        Ada.Strings.Unbounded.Length (To_Unbounded_String'Result)
  94      = Length,
  95      Global => null;
  96    --  Returns an Unbounded_String that represents an uninitialized String
  97    --  whose length is Length.
  98
  99    function To_String (Source : Unbounded_String) return String with
 100      Post   => To_String'Result'Length = Length (Source),
 101      Global => null;
 102    --  Returns the String with lower bound 1 represented by Source
 103
 104    --  To_String and To_Unbounded_String are related as follows:
 105    --
 106    --  * If S is a String, then To_String (To_Unbounded_String (S)) = S.
 107    --
 108    --  * If U is an Unbounded_String, then
 109    --    To_Unbounded_String (To_String (U)) = U.
 110
 111    procedure Set_Unbounded_String
 112      (Target : out Unbounded_String;
 113       Source : String)
 114    with
 115      Global => null;
 116    pragma Ada_05 (Set_Unbounded_String);
 117    --  Sets Target to an Unbounded_String that represents Source
 118
 119    procedure Append
 120      (Source   : in out Unbounded_String;
 121       New_Item : Unbounded_String)
 122    with
 123      Pre    => Length (New_Item) <= Natural'Last - Length (Source),
 124      Post   => Length (Source) = Length (Source)'Old + Length (New_Item),
 125      Global => null;
 126
 127    procedure Append
 128      (Source   : in out Unbounded_String;
 129       New_Item : String)
 130    with
 131      Pre    => New_Item'Length <= Natural'Last - Length (Source),
 132      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
 133      Global => null;
 134
 135    procedure Append
 136      (Source   : in out Unbounded_String;
 137       New_Item : Character)
 138    with
 139      Pre    => Length (Source) < Natural'Last,
 140      Post   => Length (Source) = Length (Source)'Old + 1,
 141      Global => null;
 142
 143    --  For each of the Append procedures, the resulting string represented by
 144    --  the Source parameter is given by the concatenation of the original value
 145    --  of Source and the value of New_Item.
 146
 147    function "&"
 148      (Left  : Unbounded_String;
 149       Right : Unbounded_String) return Unbounded_String
 150    with
 151      Pre    => Length (Right) <= Natural'Last - Length (Left),
 152      Post   => Length ("&"'Result) = Length (Left) + Length (Right),
 153      Global => null;
 154
 155    function "&"
 156      (Left  : Unbounded_String;
 157       Right : String) return Unbounded_String
 158    with
 159      Pre    => Right'Length <= Natural'Last - Length (Left),
 160      Post   => Length ("&"'Result) = Length (Left) + Right'Length,
 161      Global => null;
 162
 163    function "&"
 164      (Left  : String;
 165       Right : Unbounded_String) return Unbounded_String
 166    with
 167      Pre    => Left'Length <= Natural'Last - Length (Right),
 168      Post   => Length ("&"'Result) = Left'Length + Length (Right),
 169      Global => null;
 170
 171    function "&"
 172      (Left  : Unbounded_String;
 173       Right : Character) return Unbounded_String
 174    with
 175      Pre    => Length (Left) < Natural'Last,
 176      Post   => Length ("&"'Result) = Length (Left) + 1,
 177      Global => null;
 178
 179    function "&"
 180      (Left  : Character;
 181       Right : Unbounded_String) return Unbounded_String
 182    with
 183      Pre    => Length (Right) < Natural'Last,
 184      Post   => Length ("&"'Result) = Length (Right) + 1,
 185      Global => null;
 186
 187    --  Each of the "&" functions returns an Unbounded_String obtained by
 188    --  concatenating the string or character given or represented by one of the
 189    --  parameters, with the string or character given or represented by the
 190    --  other parameter, and applying To_Unbounded_String to the concatenation
 191    --  result string.
 192
 193    function Element
 194      (Source : Unbounded_String;
 195       Index  : Positive) return Character
 196    with
 197      Pre    => Index <= Length (Source),
 198      Global => null;
 199    --  Returns the character at position Index in the string represented by
 200    --  Source; propagates Index_Error if Index > Length (Source).
 201
 202    procedure Replace_Element
 203      (Source : in out Unbounded_String;
 204       Index  : Positive;
 205       By     : Character)
 206    with
 207      Pre    => Index <= Length (Source),
 208      Post   => Length (Source) = Length (Source)'Old,
 209      Global => null;
 210    --  Updates Source such that the character at position Index in the string
 211    --  represented by Source is By; propagates Index_Error if
 212    --  Index > Length (Source).
 213
 214    function Slice
 215      (Source : Unbounded_String;
 216       Low    : Positive;
 217       High   : Natural) return String
 218    with
 219      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
 220      Post   => Slice'Result'Length = Natural'Max (0, High - Low + 1),
 221      Global => null;
 222    --  Returns the slice at positions Low through High in the string
 223    --  represented by Source; propagates Index_Error if
 224    --  Low > Length (Source) + 1 or High > Length (Source). The bounds of the
 225    --  returned string are Low and High.
 226
 227    function Unbounded_Slice
 228      (Source : Unbounded_String;
 229       Low    : Positive;
 230       High   : Natural) return Unbounded_String
 231    with
 232      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
 233      Post   =>
 234        Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
 235      Global => null;
 236    pragma Ada_05 (Unbounded_Slice);
 237    --  Returns the slice at positions Low through High in the string
 238    --  represented by Source as an Unbounded_String. This propagates
 239    --  Index_Error if Low > Length(Source) + 1 or High > Length (Source).
 240
 241    procedure Unbounded_Slice
 242      (Source : Unbounded_String;
 243       Target : out Unbounded_String;
 244       Low    : Positive;
 245       High   : Natural)
 246    with
 247      Pre    => Low - 1 <= Length (Source) and then High <= Length (Source),
 248      Post   => Length (Target) = Natural'Max (0, High - Low + 1),
 249      Global => null;
 250    pragma Ada_05 (Unbounded_Slice);
 251    --  Sets Target to the Unbounded_String representing the slice at positions
 252    --  Low through High in the string represented by Source. This propagates
 253    --  Index_Error if Low > Length(Source) + 1 or High > Length (Source).
 254
 255    function "="
 256      (Left  : Unbounded_String;
 257       Right : Unbounded_String) return Boolean
 258    with
 259      Global => null;
 260
 261    function "="
 262      (Left  : Unbounded_String;
 263       Right : String) return Boolean
 264    with
 265      Global => null;
 266
 267    function "="
 268      (Left  : String;
 269       Right : Unbounded_String) return Boolean
 270    with
 271      Global => null;
 272
 273    function "<"
 274      (Left  : Unbounded_String;
 275       Right : Unbounded_String) return Boolean
 276    with
 277      Global => null;
 278
 279    function "<"
 280      (Left  : Unbounded_String;
 281       Right : String) return Boolean
 282    with
 283      Global => null;
 284
 285    function "<"
 286      (Left  : String;
 287       Right : Unbounded_String) return Boolean
 288    with
 289      Global => null;
 290
 291    function "<="
 292      (Left  : Unbounded_String;
 293       Right : Unbounded_String) return Boolean
 294    with
 295      Global => null;
 296
 297    function "<="
 298      (Left  : Unbounded_String;
 299       Right : String) return Boolean
 300    with
 301      Global => null;
 302
 303    function "<="
 304      (Left  : String;
 305       Right : Unbounded_String) return Boolean
 306    with
 307      Global => null;
 308
 309    function ">"
 310      (Left  : Unbounded_String;
 311       Right : Unbounded_String) return Boolean
 312    with
 313      Global => null;
 314
 315    function ">"
 316      (Left  : Unbounded_String;
 317       Right : String) return Boolean
 318    with
 319      Global => null;
 320
 321    function ">"
 322      (Left  : String;
 323       Right : Unbounded_String) return Boolean
 324    with
 325      Global => null;
 326
 327    function ">="
 328      (Left  : Unbounded_String;
 329       Right : Unbounded_String) return Boolean
 330    with
 331      Global => null;
 332
 333    function ">="
 334      (Left  : Unbounded_String;
 335       Right : String) return Boolean
 336    with
 337      Global => null;
 338
 339    function ">="
 340      (Left  : String;
 341       Right : Unbounded_String) return Boolean
 342    with
 343      Global => null;
 344
 345    --  Each of the functions "=", "<", ">", "<=", and ">=" returns the same
 346    --  result as the corresponding String operation applied to the String
 347    --  values given or represented by Left and Right.
 348
 349    ------------------------
 350    -- Search Subprograms --
 351    ------------------------
 352
 353    function Index
 354      (Source  : Unbounded_String;
 355       Pattern : String;
 356       Going   : Direction := Forward;
 357       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 358    with
 359      Pre    => Pattern'Length /= 0,
 360      Global => null;
 361
 362    function Index
 363      (Source  : Unbounded_String;
 364       Pattern : String;
 365       Going   : Direction := Forward;
 366       Mapping : Maps.Character_Mapping_Function) return Natural
 367    with
 368      Pre    => Pattern'Length /= 0,
 369      Global => null;
 370
 371    function Index
 372      (Source : Unbounded_String;
 373       Set    : Maps.Character_Set;
 374       Test   : Membership := Inside;
 375       Going  : Direction  := Forward) return Natural
 376    with
 377      Global => null;
 378
 379    function Index
 380      (Source  : Unbounded_String;
 381       Pattern : String;
 382       From    : Positive;
 383       Going   : Direction := Forward;
 384       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 385    with
 386      Pre    => (if Length (Source) /= 0 then From <= Length (Source))
 387                and then Pattern'Length /= 0,
 388      Global => null;
 389    pragma Ada_05 (Index);
 390
 391    function Index
 392      (Source  : Unbounded_String;
 393       Pattern : String;
 394       From    : Positive;
 395       Going   : Direction := Forward;
 396       Mapping : Maps.Character_Mapping_Function) return Natural
 397    with
 398      Pre    => (if Length (Source) /= 0 then From <= Length (Source))
 399                and then Pattern'Length /= 0,
 400      Global => null;
 401    pragma Ada_05 (Index);
 402
 403    function Index
 404      (Source  : Unbounded_String;
 405       Set     : Maps.Character_Set;
 406       From    : Positive;
 407       Test    : Membership := Inside;
 408       Going   : Direction := Forward) return Natural
 409    with
 410      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
 411      Global => null;
 412    pragma Ada_05 (Index);
 413
 414    function Index_Non_Blank
 415      (Source : Unbounded_String;
 416       Going  : Direction := Forward) return Natural
 417    with
 418      Global => null;
 419
 420    function Index_Non_Blank
 421      (Source : Unbounded_String;
 422       From   : Positive;
 423       Going  : Direction := Forward) return Natural
 424    with
 425      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
 426      Global => null;
 427    pragma Ada_05 (Index_Non_Blank);
 428
 429    function Count
 430      (Source  : Unbounded_String;
 431       Pattern : String;
 432       Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
 433    with
 434      Pre    => Pattern'Length /= 0,
 435      Global => null;
 436
 437    function Count
 438      (Source  : Unbounded_String;
 439       Pattern : String;
 440       Mapping : Maps.Character_Mapping_Function) return Natural
 441    with
 442      Pre    => Pattern'Length /= 0,
 443      Global => null;
 444
 445    function Count
 446      (Source : Unbounded_String;
 447       Set    : Maps.Character_Set) return Natural
 448    with
 449      Global => null;
 450
 451    procedure Find_Token
 452      (Source : Unbounded_String;
 453       Set    : Maps.Character_Set;
 454       From   : Positive;
 455       Test   : Membership;
 456       First  : out Positive;
 457       Last   : out Natural)
 458    with
 459      Pre    => (if Length (Source) /= 0 then From <= Length (Source)),
 460      Global => null;
 461    pragma Ada_2012 (Find_Token);
 462
 463    procedure Find_Token
 464      (Source : Unbounded_String;
 465       Set    : Maps.Character_Set;
 466       Test   : Membership;
 467       First  : out Positive;
 468       Last   : out Natural)
 469    with
 470      Global => null;
 471
 472    --  Each of the search subprograms (Index, Index_Non_Blank, Count,
 473    --  Find_Token) has the same effect as the corresponding subprogram in
 474    --  Strings.Fixed applied to the string represented by the Unbounded_String
 475    --  parameter.
 476
 477    ------------------------------------
 478    -- String Translation Subprograms --
 479    ------------------------------------
 480
 481    function Translate
 482      (Source  : Unbounded_String;
 483       Mapping : Maps.Character_Mapping) return Unbounded_String
 484    with
 485      Post   => Length (Translate'Result) = Length (Source),
 486      Global => null;
 487
 488    procedure Translate
 489      (Source  : in out Unbounded_String;
 490       Mapping : Maps.Character_Mapping)
 491    with
 492      Post   => Length (Source) = Length (Source)'Old,
 493      Global => null;
 494
 495    function Translate
 496      (Source  : Unbounded_String;
 497       Mapping : Maps.Character_Mapping_Function) return Unbounded_String
 498    with
 499      Post   => Length (Translate'Result) = Length (Source),
 500      Global => null;
 501
 502    procedure Translate
 503      (Source  : in out Unbounded_String;
 504       Mapping : Maps.Character_Mapping_Function)
 505    with
 506      Post   => Length (Source) = Length (Source)'Old,
 507      Global => null;
 508
 509    --  The Translate function has an analogous effect to the corresponding
 510    --  subprogram in Strings.Fixed. The translation is applied to the string
 511    --  represented by the Unbounded_String parameter, and the result is
 512    --  converted (via To_Unbounded_String) to an Unbounded_String.
 513
 514    ---------------------------------------
 515    -- String Transformation Subprograms --
 516    ---------------------------------------
 517
 518    function Replace_Slice
 519      (Source : Unbounded_String;
 520       Low    : Positive;
 521       High   : Natural;
 522       By     : String) return Unbounded_String
 523    with
 524      Pre            =>
 525        Low - 1 <= Length (Source)
 526        and then (if High >= Low
 527                  then Low - 1
 528                    <= Natural'Last - By'Length
 529                     - Natural'Max (Length (Source) - High, 0)
 530                  else Length (Source) <= Natural'Last - By'Length),
 531      Contract_Cases =>
 532        (High >= Low =>
 533           Length (Replace_Slice'Result)
 534         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
 535         others      =>
 536           Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
 537      Global         => null;
 538
 539    procedure Replace_Slice
 540      (Source : in out Unbounded_String;
 541       Low    : Positive;
 542       High   : Natural;
 543       By     : String)
 544    with
 545      Pre            =>
 546        Low - 1 <= Length (Source)
 547        and then (if High >= Low
 548                  then Low - 1
 549                    <= Natural'Last - By'Length
 550                     - Natural'Max (Length (Source) - High, 0)
 551                  else Length (Source) <= Natural'Last - By'Length),
 552      Contract_Cases =>
 553        (High >= Low =>
 554           Length (Source)
 555         = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
 556         others      =>
 557           Length (Source) = Length (Source)'Old + By'Length),
 558      Global         => null;
 559
 560    function Insert
 561      (Source   : Unbounded_String;
 562       Before   : Positive;
 563       New_Item : String) return Unbounded_String
 564    with
 565      Pre    => Before - 1 <= Length (Source)
 566                  and then New_Item'Length <= Natural'Last - Length (Source),
 567      Post   => Length (Insert'Result) = Length (Source) + New_Item'Length,
 568      Global => null;
 569
 570    procedure Insert
 571      (Source   : in out Unbounded_String;
 572       Before   : Positive;
 573       New_Item : String)
 574    with
 575      Pre    => Before - 1 <= Length (Source)
 576                  and then New_Item'Length <= Natural'Last - Length (Source),
 577      Post   => Length (Source) = Length (Source)'Old + New_Item'Length,
 578      Global => null;
 579
 580    function Overwrite
 581      (Source   : Unbounded_String;
 582       Position : Positive;
 583       New_Item : String) return Unbounded_String
 584    with
 585      Pre    => Position - 1 <= Length (Source)
 586                  and then (if New_Item'Length /= 0
 587                            then
 588                            New_Item'Length <= Natural'Last - (Position - 1)),
 589      Post   =>
 590        Length (Overwrite'Result)
 591      = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
 592      Global => null;
 593
 594    procedure Overwrite
 595      (Source   : in out Unbounded_String;
 596       Position : Positive;
 597       New_Item : String)
 598    with
 599      Pre    => Position - 1 <= Length (Source)
 600                  and then (if New_Item'Length /= 0
 601                            then
 602                            New_Item'Length <= Natural'Last - (Position - 1)),
 603      Post   =>
 604        Length (Source)
 605      = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
 606
 607      Global => null;
 608
 609    function Delete
 610      (Source  : Unbounded_String;
 611       From    : Positive;
 612       Through : Natural) return Unbounded_String
 613    with
 614      Pre            => (if Through <= From then From - 1 <= Length (Source)),
 615      Contract_Cases =>
 616        (Through >= From =>
 617           Length (Delete'Result) = Length (Source) - (Through - From + 1),
 618         others          =>
 619           Length (Delete'Result) = Length (Source)),
 620      Global         => null;
 621
 622    procedure Delete
 623      (Source  : in out Unbounded_String;
 624       From    : Positive;
 625       Through : Natural)
 626    with
 627      Pre            => (if Through <= From then From - 1 <= Length (Source)),
 628      Contract_Cases =>
 629        (Through >= From =>
 630           Length (Source) = Length (Source)'Old - (Through - From + 1),
 631         others          =>
 632           Length (Source) = Length (Source)'Old),
 633      Global         => null;
 634
 635    function Trim
 636      (Source : Unbounded_String;
 637       Side   : Trim_End) return Unbounded_String
 638    with
 639      Post   => Length (Trim'Result) <= Length (Source),
 640      Global => null;
 641
 642    procedure Trim
 643      (Source : in out Unbounded_String;
 644       Side   : Trim_End)
 645    with
 646      Post   => Length (Source) <= Length (Source)'Old,
 647      Global => null;
 648
 649    function Trim
 650      (Source : Unbounded_String;
 651       Left   : Maps.Character_Set;
 652       Right  : Maps.Character_Set) return Unbounded_String
 653    with
 654      Post   => Length (Trim'Result) <= Length (Source),
 655      Global => null;
 656
 657    procedure Trim
 658      (Source : in out Unbounded_String;
 659       Left   : Maps.Character_Set;
 660       Right  : Maps.Character_Set)
 661    with
 662      Post   => Length (Source) <= Length (Source)'Old,
 663      Global => null;
 664
 665    function Head
 666      (Source : Unbounded_String;
 667       Count  : Natural;
 668       Pad    : Character := Space) return Unbounded_String
 669    with
 670      Post   => Length (Head'Result) = Count,
 671      Global => null;
 672
 673    procedure Head
 674      (Source : in out Unbounded_String;
 675       Count  : Natural;
 676       Pad    : Character := Space)
 677    with
 678      Post   => Length (Source) = Count,
 679      Global => null;
 680
 681    function Tail
 682      (Source : Unbounded_String;
 683       Count  : Natural;
 684       Pad    : Character := Space) return Unbounded_String
 685    with
 686      Post   => Length (Tail'Result) = Count,
 687      Global => null;
 688
 689    procedure Tail
 690      (Source : in out Unbounded_String;
 691       Count  : Natural;
 692       Pad    : Character := Space)
 693    with
 694      Post   => Length (Source) = Count,
 695      Global => null;
 696
 697    function "*"
 698      (Left  : Natural;
 699       Right : Character) return Unbounded_String
 700    with
 701      Pre    => Left <= Natural'Last,
 702      Post   => Length ("*"'Result) = Left,
 703      Global => null;
 704
 705    function "*"
 706      (Left  : Natural;
 707       Right : String) return Unbounded_String
 708    with
 709      Pre    => (if Left /= 0 then Right'Length <= Natural'Last / Left),
 710      Post   => Length ("*"'Result) = Left * Right'Length,
 711      Global => null;
 712
 713    function "*"
 714      (Left  : Natural;
 715       Right : Unbounded_String) return Unbounded_String
 716    with
 717      Pre    => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
 718      Post   => Length ("*"'Result) = Left * Length (Right),
 719      Global => null;
 720
 721    --  Each of the transformation functions (Replace_Slice, Insert, Overwrite,
 722    --  Delete), selector functions (Trim, Head, Tail), and constructor
 723    --  functions ("*") is likewise analogous to its corresponding subprogram in
 724    --  Strings.Fixed. For each of the subprograms, the corresponding
 725    --  fixed-length string subprogram is applied to the string represented by
 726    --  the Unbounded_String parameter, and To_Unbounded_String is applied the
 727    --  result string.
 728    --
 729    --  For each of the procedures Translate, Replace_Slice, Insert, Overwrite,
 730    --  Delete, Trim, Head, and Tail, the resulting string represented by the
 731    --  Source parameter is given by the corresponding function for fixed-length
 732    --  strings applied to the string represented by Source's original value.
 733
 734 private
 735    pragma Inline (Length);
 736
 737    package AF renames Ada.Finalization;
 738
 739    Null_String : aliased String := "";
 740
 741    function To_Unbounded (S : String) return Unbounded_String
 742      renames To_Unbounded_String;
 743
 744    type Unbounded_String is new AF.Controlled with record
 745       Reference : String_Access := Null_String'Access;
 746       Last      : Natural       := 0;
 747    end record;
 748    --  The Unbounded_String is using a buffered implementation to increase
 749    --  speed of the Append/Delete/Insert procedures. The Reference string
 750    --  pointer above contains the current string value and extra room at the
 751    --  end to be used by the next Append routine. Last is the index of the
 752    --  string ending character. So the current string value is really
 753    --  Reference (1 .. Last).
 754
 755    pragma Stream_Convert (Unbounded_String, To_Unbounded, To_String);
 756    --  Provide stream routines without dragging in Ada.Streams
 757
 758    pragma Finalize_Storage_Only (Unbounded_String);
 759    --  Finalization is required only for freeing storage
 760
 761    procedure Initialize (Object : in out Unbounded_String);
 762    procedure Adjust     (Object : in out Unbounded_String);
 763    procedure Finalize   (Object : in out Unbounded_String);
 764
 765    procedure Realloc_For_Chunk
 766      (Source     : in out Unbounded_String;
 767       Chunk_Size : Natural);
 768    pragma Inline (Realloc_For_Chunk);
 769    --  Adjust the size allocated for the string. Add at least Chunk_Size so it
 770    --  is safe to add a string of this size at the end of the current content.
 771    --  The real size allocated for the string is Chunk_Size + x of the current
 772    --  string size. This buffered handling makes the Append unbounded string
 773    --  routines very fast. This spec is in the private part so that it can be
 774    --  accessed from children (e.g. from Unbounded.Text_IO).
 775
 776    Null_Unbounded_String : constant Unbounded_String :=
 777                              (AF.Controlled with
 778                                 Reference => Null_String'Access,
 779                                 Last      => 0);
 780 end Ada.Strings.Unbounded;