Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/libgnat/a-strunb.ads @ 145:1830386684a0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
gcc-9.2.0
author anatofuz
date Thu, 13 Feb 2020 11:34:05 +0900
parents 84e7813d76e9
children
comparison
equal deleted inserted replaced
131:84e7813d76e9 145:1830386684a0
4 -- -- 4 -- --
5 -- A D A . S T R I N G S . U N B O U N D E D -- 5 -- A D A . S T R I N G S . U N B O U N D E D --
6 -- -- 6 -- --
7 -- S p e c -- 7 -- S p e c --
8 -- -- 8 -- --
9 -- Copyright (C) 1992-2018, Free Software Foundation, Inc. -- 9 -- Copyright (C) 1992-2019, Free Software Foundation, Inc. --
10 -- -- 10 -- --
11 -- This specification is derived from the Ada Reference Manual for use with -- 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 -- 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. -- 13 -- apply solely to the contents of the part following the private keyword. --
14 -- -- 14 -- --
31 -- GNAT was originally developed by the GNAT team at New York University. -- 31 -- GNAT was originally developed by the GNAT team at New York University. --
32 -- Extensive contributions were provided by Ada Core Technologies Inc. -- 32 -- Extensive contributions were provided by Ada Core Technologies Inc. --
33 -- -- 33 -- --
34 ------------------------------------------------------------------------------ 34 ------------------------------------------------------------------------------
35 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
36 with Ada.Strings.Maps; 42 with Ada.Strings.Maps;
37 with Ada.Finalization; 43 with Ada.Finalization;
38 44
39 package Ada.Strings.Unbounded is 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
40 pragma Preelaborate; 57 pragma Preelaborate;
41 58
42 type Unbounded_String is private; 59 type Unbounded_String is private;
43 pragma Preelaborable_Initialization (Unbounded_String); 60 pragma Preelaborable_Initialization (Unbounded_String);
44 61
45 Null_Unbounded_String : constant Unbounded_String; 62 Null_Unbounded_String : constant Unbounded_String;
46 63 -- Represents the null String. If an object of type Unbounded_String is not
47 function Length (Source : Unbounded_String) return Natural; 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
48 70
49 type String_Access is access all String; 71 type String_Access is access all String;
72 -- Provides a (nonprivate) access type for explicit processing of
73 -- unbounded-length strings.
50 74
51 procedure Free (X : in out String_Access); 75 procedure Free (X : in out String_Access);
76 -- Performs an unchecked deallocation of an object of type String_Access
52 77
53 -------------------------------------------------------- 78 --------------------------------------------------------
54 -- Conversion, Concatenation, and Selection Functions -- 79 -- Conversion, Concatenation, and Selection Functions --
55 -------------------------------------------------------- 80 --------------------------------------------------------
56 81
57 function To_Unbounded_String 82 function To_Unbounded_String
58 (Source : String) return 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
59 88
60 function To_Unbounded_String 89 function To_Unbounded_String
61 (Length : Natural) return Unbounded_String; 90 (Length : Natural) return Unbounded_String
62 91 with
63 function To_String (Source : Unbounded_String) return String; 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.
64 110
65 procedure Set_Unbounded_String 111 procedure Set_Unbounded_String
66 (Target : out Unbounded_String; 112 (Target : out Unbounded_String;
67 Source : String); 113 Source : String)
114 with
115 Global => null;
68 pragma Ada_05 (Set_Unbounded_String); 116 pragma Ada_05 (Set_Unbounded_String);
117 -- Sets Target to an Unbounded_String that represents Source
69 118
70 procedure Append 119 procedure Append
71 (Source : in out Unbounded_String; 120 (Source : in out Unbounded_String;
72 New_Item : 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;
73 126
74 procedure Append 127 procedure Append
75 (Source : in out Unbounded_String; 128 (Source : in out Unbounded_String;
76 New_Item : 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;
77 134
78 procedure Append 135 procedure Append
79 (Source : in out Unbounded_String; 136 (Source : in out Unbounded_String;
80 New_Item : Character); 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.
81 146
82 function "&" 147 function "&"
83 (Left : Unbounded_String; 148 (Left : Unbounded_String;
84 Right : Unbounded_String) return 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;
85 154
86 function "&" 155 function "&"
87 (Left : Unbounded_String; 156 (Left : Unbounded_String;
88 Right : String) return 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;
89 162
90 function "&" 163 function "&"
91 (Left : String; 164 (Left : String;
92 Right : Unbounded_String) return Unbounded_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;
93 170
94 function "&" 171 function "&"
95 (Left : Unbounded_String; 172 (Left : Unbounded_String;
96 Right : Character) return 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;
97 178
98 function "&" 179 function "&"
99 (Left : Character; 180 (Left : Character;
100 Right : Unbounded_String) return Unbounded_String; 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.
101 192
102 function Element 193 function Element
103 (Source : Unbounded_String; 194 (Source : Unbounded_String;
104 Index : Positive) return Character; 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).
105 201
106 procedure Replace_Element 202 procedure Replace_Element
107 (Source : in out Unbounded_String; 203 (Source : in out Unbounded_String;
108 Index : Positive; 204 Index : Positive;
109 By : Character); 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).
110 213
111 function Slice 214 function Slice
112 (Source : Unbounded_String; 215 (Source : Unbounded_String;
113 Low : Positive; 216 Low : Positive;
114 High : Natural) return String; 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.
115 226
116 function Unbounded_Slice 227 function Unbounded_Slice
117 (Source : Unbounded_String; 228 (Source : Unbounded_String;
118 Low : Positive; 229 Low : Positive;
119 High : Natural) return Unbounded_String; 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;
120 pragma Ada_05 (Unbounded_Slice); 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).
121 240
122 procedure Unbounded_Slice 241 procedure Unbounded_Slice
123 (Source : Unbounded_String; 242 (Source : Unbounded_String;
124 Target : out Unbounded_String; 243 Target : out Unbounded_String;
125 Low : Positive; 244 Low : Positive;
126 High : Natural); 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;
127 pragma Ada_05 (Unbounded_Slice); 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).
128 254
129 function "=" 255 function "="
130 (Left : Unbounded_String; 256 (Left : Unbounded_String;
131 Right : Unbounded_String) return Boolean; 257 Right : Unbounded_String) return Boolean
258 with
259 Global => null;
132 260
133 function "=" 261 function "="
134 (Left : Unbounded_String; 262 (Left : Unbounded_String;
135 Right : String) return Boolean; 263 Right : String) return Boolean
264 with
265 Global => null;
136 266
137 function "=" 267 function "="
138 (Left : String; 268 (Left : String;
139 Right : Unbounded_String) return Boolean; 269 Right : Unbounded_String) return Boolean
270 with
271 Global => null;
140 272
141 function "<" 273 function "<"
142 (Left : Unbounded_String; 274 (Left : Unbounded_String;
143 Right : Unbounded_String) return Boolean; 275 Right : Unbounded_String) return Boolean
276 with
277 Global => null;
144 278
145 function "<" 279 function "<"
146 (Left : Unbounded_String; 280 (Left : Unbounded_String;
147 Right : String) return Boolean; 281 Right : String) return Boolean
282 with
283 Global => null;
148 284
149 function "<" 285 function "<"
150 (Left : String; 286 (Left : String;
151 Right : Unbounded_String) return Boolean; 287 Right : Unbounded_String) return Boolean
288 with
289 Global => null;
152 290
153 function "<=" 291 function "<="
154 (Left : Unbounded_String; 292 (Left : Unbounded_String;
155 Right : Unbounded_String) return Boolean; 293 Right : Unbounded_String) return Boolean
294 with
295 Global => null;
156 296
157 function "<=" 297 function "<="
158 (Left : Unbounded_String; 298 (Left : Unbounded_String;
159 Right : String) return Boolean; 299 Right : String) return Boolean
300 with
301 Global => null;
160 302
161 function "<=" 303 function "<="
162 (Left : String; 304 (Left : String;
163 Right : Unbounded_String) return Boolean; 305 Right : Unbounded_String) return Boolean
306 with
307 Global => null;
164 308
165 function ">" 309 function ">"
166 (Left : Unbounded_String; 310 (Left : Unbounded_String;
167 Right : Unbounded_String) return Boolean; 311 Right : Unbounded_String) return Boolean
312 with
313 Global => null;
168 314
169 function ">" 315 function ">"
170 (Left : Unbounded_String; 316 (Left : Unbounded_String;
171 Right : String) return Boolean; 317 Right : String) return Boolean
318 with
319 Global => null;
172 320
173 function ">" 321 function ">"
174 (Left : String; 322 (Left : String;
175 Right : Unbounded_String) return Boolean; 323 Right : Unbounded_String) return Boolean
324 with
325 Global => null;
176 326
177 function ">=" 327 function ">="
178 (Left : Unbounded_String; 328 (Left : Unbounded_String;
179 Right : Unbounded_String) return Boolean; 329 Right : Unbounded_String) return Boolean
330 with
331 Global => null;
180 332
181 function ">=" 333 function ">="
182 (Left : Unbounded_String; 334 (Left : Unbounded_String;
183 Right : String) return Boolean; 335 Right : String) return Boolean
336 with
337 Global => null;
184 338
185 function ">=" 339 function ">="
186 (Left : String; 340 (Left : String;
187 Right : Unbounded_String) return Boolean; 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.
188 348
189 ------------------------ 349 ------------------------
190 -- Search Subprograms -- 350 -- Search Subprograms --
191 ------------------------ 351 ------------------------
192 352
193 function Index 353 function Index
194 (Source : Unbounded_String; 354 (Source : Unbounded_String;
195 Pattern : String; 355 Pattern : String;
196 Going : Direction := Forward; 356 Going : Direction := Forward;
197 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; 357 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
358 with
359 Pre => Pattern'Length /= 0,
360 Global => null;
198 361
199 function Index 362 function Index
200 (Source : Unbounded_String; 363 (Source : Unbounded_String;
201 Pattern : String; 364 Pattern : String;
202 Going : Direction := Forward; 365 Going : Direction := Forward;
203 Mapping : Maps.Character_Mapping_Function) return Natural; 366 Mapping : Maps.Character_Mapping_Function) return Natural
367 with
368 Pre => Pattern'Length /= 0,
369 Global => null;
204 370
205 function Index 371 function Index
206 (Source : Unbounded_String; 372 (Source : Unbounded_String;
207 Set : Maps.Character_Set; 373 Set : Maps.Character_Set;
208 Test : Membership := Inside; 374 Test : Membership := Inside;
209 Going : Direction := Forward) return Natural; 375 Going : Direction := Forward) return Natural
376 with
377 Global => null;
210 378
211 function Index 379 function Index
212 (Source : Unbounded_String; 380 (Source : Unbounded_String;
213 Pattern : String; 381 Pattern : String;
214 From : Positive; 382 From : Positive;
215 Going : Direction := Forward; 383 Going : Direction := Forward;
216 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; 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;
217 pragma Ada_05 (Index); 389 pragma Ada_05 (Index);
218 390
219 function Index 391 function Index
220 (Source : Unbounded_String; 392 (Source : Unbounded_String;
221 Pattern : String; 393 Pattern : String;
222 From : Positive; 394 From : Positive;
223 Going : Direction := Forward; 395 Going : Direction := Forward;
224 Mapping : Maps.Character_Mapping_Function) return Natural; 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;
225 pragma Ada_05 (Index); 401 pragma Ada_05 (Index);
226 402
227 function Index 403 function Index
228 (Source : Unbounded_String; 404 (Source : Unbounded_String;
229 Set : Maps.Character_Set; 405 Set : Maps.Character_Set;
230 From : Positive; 406 From : Positive;
231 Test : Membership := Inside; 407 Test : Membership := Inside;
232 Going : Direction := Forward) return Natural; 408 Going : Direction := Forward) return Natural
409 with
410 Pre => (if Length (Source) /= 0 then From <= Length (Source)),
411 Global => null;
233 pragma Ada_05 (Index); 412 pragma Ada_05 (Index);
234 413
235 function Index_Non_Blank 414 function Index_Non_Blank
236 (Source : Unbounded_String; 415 (Source : Unbounded_String;
237 Going : Direction := Forward) return Natural; 416 Going : Direction := Forward) return Natural
417 with
418 Global => null;
238 419
239 function Index_Non_Blank 420 function Index_Non_Blank
240 (Source : Unbounded_String; 421 (Source : Unbounded_String;
241 From : Positive; 422 From : Positive;
242 Going : Direction := Forward) return Natural; 423 Going : Direction := Forward) return Natural
424 with
425 Pre => (if Length (Source) /= 0 then From <= Length (Source)),
426 Global => null;
243 pragma Ada_05 (Index_Non_Blank); 427 pragma Ada_05 (Index_Non_Blank);
244 428
245 function Count 429 function Count
246 (Source : Unbounded_String; 430 (Source : Unbounded_String;
247 Pattern : String; 431 Pattern : String;
248 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; 432 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
433 with
434 Pre => Pattern'Length /= 0,
435 Global => null;
249 436
250 function Count 437 function Count
251 (Source : Unbounded_String; 438 (Source : Unbounded_String;
252 Pattern : String; 439 Pattern : String;
253 Mapping : Maps.Character_Mapping_Function) return Natural; 440 Mapping : Maps.Character_Mapping_Function) return Natural
441 with
442 Pre => Pattern'Length /= 0,
443 Global => null;
254 444
255 function Count 445 function Count
256 (Source : Unbounded_String; 446 (Source : Unbounded_String;
257 Set : Maps.Character_Set) return Natural; 447 Set : Maps.Character_Set) return Natural
448 with
449 Global => null;
258 450
259 procedure Find_Token 451 procedure Find_Token
260 (Source : Unbounded_String; 452 (Source : Unbounded_String;
261 Set : Maps.Character_Set; 453 Set : Maps.Character_Set;
262 From : Positive; 454 From : Positive;
263 Test : Membership; 455 Test : Membership;
264 First : out Positive; 456 First : out Positive;
265 Last : out Natural); 457 Last : out Natural)
458 with
459 Pre => (if Length (Source) /= 0 then From <= Length (Source)),
460 Global => null;
266 pragma Ada_2012 (Find_Token); 461 pragma Ada_2012 (Find_Token);
267 462
268 procedure Find_Token 463 procedure Find_Token
269 (Source : Unbounded_String; 464 (Source : Unbounded_String;
270 Set : Maps.Character_Set; 465 Set : Maps.Character_Set;
271 Test : Membership; 466 Test : Membership;
272 First : out Positive; 467 First : out Positive;
273 Last : out Natural); 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.
274 476
275 ------------------------------------ 477 ------------------------------------
276 -- String Translation Subprograms -- 478 -- String Translation Subprograms --
277 ------------------------------------ 479 ------------------------------------
278 480
279 function Translate 481 function Translate
280 (Source : Unbounded_String; 482 (Source : Unbounded_String;
281 Mapping : Maps.Character_Mapping) return Unbounded_String; 483 Mapping : Maps.Character_Mapping) return Unbounded_String
484 with
485 Post => Length (Translate'Result) = Length (Source),
486 Global => null;
282 487
283 procedure Translate 488 procedure Translate
284 (Source : in out Unbounded_String; 489 (Source : in out Unbounded_String;
285 Mapping : Maps.Character_Mapping); 490 Mapping : Maps.Character_Mapping)
491 with
492 Post => Length (Source) = Length (Source)'Old,
493 Global => null;
286 494
287 function Translate 495 function Translate
288 (Source : Unbounded_String; 496 (Source : Unbounded_String;
289 Mapping : Maps.Character_Mapping_Function) return Unbounded_String; 497 Mapping : Maps.Character_Mapping_Function) return Unbounded_String
498 with
499 Post => Length (Translate'Result) = Length (Source),
500 Global => null;
290 501
291 procedure Translate 502 procedure Translate
292 (Source : in out Unbounded_String; 503 (Source : in out Unbounded_String;
293 Mapping : Maps.Character_Mapping_Function); 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.
294 513
295 --------------------------------------- 514 ---------------------------------------
296 -- String Transformation Subprograms -- 515 -- String Transformation Subprograms --
297 --------------------------------------- 516 ---------------------------------------
298 517
299 function Replace_Slice 518 function Replace_Slice
300 (Source : Unbounded_String; 519 (Source : Unbounded_String;
301 Low : Positive; 520 Low : Positive;
302 High : Natural; 521 High : Natural;
303 By : String) return Unbounded_String; 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;
304 538
305 procedure Replace_Slice 539 procedure Replace_Slice
306 (Source : in out Unbounded_String; 540 (Source : in out Unbounded_String;
307 Low : Positive; 541 Low : Positive;
308 High : Natural; 542 High : Natural;
309 By : String); 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;
310 559
311 function Insert 560 function Insert
312 (Source : Unbounded_String; 561 (Source : Unbounded_String;
313 Before : Positive; 562 Before : Positive;
314 New_Item : String) return Unbounded_String; 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;
315 569
316 procedure Insert 570 procedure Insert
317 (Source : in out Unbounded_String; 571 (Source : in out Unbounded_String;
318 Before : Positive; 572 Before : Positive;
319 New_Item : String); 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;
320 579
321 function Overwrite 580 function Overwrite
322 (Source : Unbounded_String; 581 (Source : Unbounded_String;
323 Position : Positive; 582 Position : Positive;
324 New_Item : String) return Unbounded_String; 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;
325 593
326 procedure Overwrite 594 procedure Overwrite
327 (Source : in out Unbounded_String; 595 (Source : in out Unbounded_String;
328 Position : Positive; 596 Position : Positive;
329 New_Item : String); 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;
330 608
331 function Delete 609 function Delete
332 (Source : Unbounded_String; 610 (Source : Unbounded_String;
333 From : Positive; 611 From : Positive;
334 Through : Natural) return Unbounded_String; 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;
335 621
336 procedure Delete 622 procedure Delete
337 (Source : in out Unbounded_String; 623 (Source : in out Unbounded_String;
338 From : Positive; 624 From : Positive;
339 Through : Natural); 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;
340 634
341 function Trim 635 function Trim
342 (Source : Unbounded_String; 636 (Source : Unbounded_String;
343 Side : Trim_End) return Unbounded_String; 637 Side : Trim_End) return Unbounded_String
638 with
639 Post => Length (Trim'Result) <= Length (Source),
640 Global => null;
344 641
345 procedure Trim 642 procedure Trim
346 (Source : in out Unbounded_String; 643 (Source : in out Unbounded_String;
347 Side : Trim_End); 644 Side : Trim_End)
645 with
646 Post => Length (Source) <= Length (Source)'Old,
647 Global => null;
348 648
349 function Trim 649 function Trim
350 (Source : Unbounded_String; 650 (Source : Unbounded_String;
351 Left : Maps.Character_Set; 651 Left : Maps.Character_Set;
352 Right : Maps.Character_Set) return Unbounded_String; 652 Right : Maps.Character_Set) return Unbounded_String
653 with
654 Post => Length (Trim'Result) <= Length (Source),
655 Global => null;
353 656
354 procedure Trim 657 procedure Trim
355 (Source : in out Unbounded_String; 658 (Source : in out Unbounded_String;
356 Left : Maps.Character_Set; 659 Left : Maps.Character_Set;
357 Right : Maps.Character_Set); 660 Right : Maps.Character_Set)
661 with
662 Post => Length (Source) <= Length (Source)'Old,
663 Global => null;
358 664
359 function Head 665 function Head
360 (Source : Unbounded_String; 666 (Source : Unbounded_String;
361 Count : Natural; 667 Count : Natural;
362 Pad : Character := Space) return Unbounded_String; 668 Pad : Character := Space) return Unbounded_String
669 with
670 Post => Length (Head'Result) = Count,
671 Global => null;
363 672
364 procedure Head 673 procedure Head
365 (Source : in out Unbounded_String; 674 (Source : in out Unbounded_String;
366 Count : Natural; 675 Count : Natural;
367 Pad : Character := Space); 676 Pad : Character := Space)
677 with
678 Post => Length (Source) = Count,
679 Global => null;
368 680
369 function Tail 681 function Tail
370 (Source : Unbounded_String; 682 (Source : Unbounded_String;
371 Count : Natural; 683 Count : Natural;
372 Pad : Character := Space) return Unbounded_String; 684 Pad : Character := Space) return Unbounded_String
685 with
686 Post => Length (Tail'Result) = Count,
687 Global => null;
373 688
374 procedure Tail 689 procedure Tail
375 (Source : in out Unbounded_String; 690 (Source : in out Unbounded_String;
376 Count : Natural; 691 Count : Natural;
377 Pad : Character := Space); 692 Pad : Character := Space)
693 with
694 Post => Length (Source) = Count,
695 Global => null;
378 696
379 function "*" 697 function "*"
380 (Left : Natural; 698 (Left : Natural;
381 Right : Character) return Unbounded_String; 699 Right : Character) return Unbounded_String
700 with
701 Pre => Left <= Natural'Last,
702 Post => Length ("*"'Result) = Left,
703 Global => null;
382 704
383 function "*" 705 function "*"
384 (Left : Natural; 706 (Left : Natural;
385 Right : String) return Unbounded_String; 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;
386 712
387 function "*" 713 function "*"
388 (Left : Natural; 714 (Left : Natural;
389 Right : Unbounded_String) return Unbounded_String; 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.
390 733
391 private 734 private
392 pragma Inline (Length); 735 pragma Inline (Length);
393 736
394 package AF renames Ada.Finalization; 737 package AF renames Ada.Finalization;