Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/libgnat/a-strunb__shared.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 -- --
30 -- -- 30 -- --
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
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);
35 41
36 -- This package provides an implementation of Ada.Strings.Unbounded that uses 42 -- This package provides an implementation of Ada.Strings.Unbounded that uses
37 -- reference counts to implement copy on modification (rather than copy on 43 -- reference counts to implement copy on modification (rather than copy on
38 -- assignment). This is significantly more efficient on many targets. 44 -- assignment). This is significantly more efficient on many targets.
39 45
71 77
72 with Ada.Strings.Maps; 78 with Ada.Strings.Maps;
73 private with Ada.Finalization; 79 private with Ada.Finalization;
74 private with System.Atomic_Counters; 80 private with System.Atomic_Counters;
75 81
76 package Ada.Strings.Unbounded is 82 package Ada.Strings.Unbounded with
83 Initial_Condition => Length (Null_Unbounded_String) = 0
84 is
77 pragma Preelaborate; 85 pragma Preelaborate;
78 86
79 type Unbounded_String is private; 87 type Unbounded_String is private;
80 pragma Preelaborable_Initialization (Unbounded_String); 88 pragma Preelaborable_Initialization (Unbounded_String);
81 89
82 Null_Unbounded_String : constant Unbounded_String; 90 Null_Unbounded_String : constant Unbounded_String;
83 91
84 function Length (Source : Unbounded_String) return Natural; 92 function Length (Source : Unbounded_String) return Natural with
93 Global => null;
85 94
86 type String_Access is access all String; 95 type String_Access is access all String;
87 96
88 procedure Free (X : in out String_Access); 97 procedure Free (X : in out String_Access);
89 98
90 -------------------------------------------------------- 99 --------------------------------------------------------
91 -- Conversion, Concatenation, and Selection Functions -- 100 -- Conversion, Concatenation, and Selection Functions --
92 -------------------------------------------------------- 101 --------------------------------------------------------
93 102
94 function To_Unbounded_String 103 function To_Unbounded_String
95 (Source : String) return Unbounded_String; 104 (Source : String) return Unbounded_String
105 with
106 Post => Length (To_Unbounded_String'Result) = Source'Length,
107 Global => null;
96 108
97 function To_Unbounded_String 109 function To_Unbounded_String
98 (Length : Natural) return Unbounded_String; 110 (Length : Natural) return Unbounded_String
99 111 with
100 function To_String (Source : Unbounded_String) return String; 112 Post =>
113 Ada.Strings.Unbounded.Length (To_Unbounded_String'Result) = Length,
114 Global => null;
115
116 function To_String (Source : Unbounded_String) return String with
117 Post => To_String'Result'Length = Length (Source),
118 Global => null;
101 119
102 procedure Set_Unbounded_String 120 procedure Set_Unbounded_String
103 (Target : out Unbounded_String; 121 (Target : out Unbounded_String;
104 Source : String); 122 Source : String)
123 with
124 Global => null;
105 pragma Ada_05 (Set_Unbounded_String); 125 pragma Ada_05 (Set_Unbounded_String);
106 126
107 procedure Append 127 procedure Append
108 (Source : in out Unbounded_String; 128 (Source : in out Unbounded_String;
109 New_Item : Unbounded_String); 129 New_Item : Unbounded_String)
130 with
131 Pre => Length (New_Item) <= Natural'Last - Length (Source),
132 Post => Length (Source) = Length (Source)'Old + Length (New_Item),
133 Global => null;
110 134
111 procedure Append 135 procedure Append
112 (Source : in out Unbounded_String; 136 (Source : in out Unbounded_String;
113 New_Item : String); 137 New_Item : String)
138 with
139 Pre => New_Item'Length <= Natural'Last - Length (Source),
140 Post => Length (Source) = Length (Source)'Old + New_Item'Length,
141 Global => null;
114 142
115 procedure Append 143 procedure Append
116 (Source : in out Unbounded_String; 144 (Source : in out Unbounded_String;
117 New_Item : Character); 145 New_Item : Character)
146 with
147 Pre => Length (Source) < Natural'Last,
148 Post => Length (Source) = Length (Source)'Old + 1,
149 Global => null;
118 150
119 function "&" 151 function "&"
120 (Left : Unbounded_String; 152 (Left : Unbounded_String;
121 Right : Unbounded_String) return Unbounded_String; 153 Right : Unbounded_String) return Unbounded_String
154 with
155 Pre => Length (Right) <= Natural'Last - Length (Left),
156 Post => Length ("&"'Result) = Length (Left) + Length (Right),
157 Global => null;
122 158
123 function "&" 159 function "&"
124 (Left : Unbounded_String; 160 (Left : Unbounded_String;
125 Right : String) return Unbounded_String; 161 Right : String) return Unbounded_String
162 with
163 Pre => Right'Length <= Natural'Last - Length (Left),
164 Post => Length ("&"'Result) = Length (Left) + Right'Length,
165 Global => null;
126 166
127 function "&" 167 function "&"
128 (Left : String; 168 (Left : String;
129 Right : Unbounded_String) return Unbounded_String; 169 Right : Unbounded_String) return Unbounded_String
170 with
171 Pre => Left'Length <= Natural'Last - Length (Right),
172 Post => Length ("&"'Result) = Left'Length + Length (Right),
173 Global => null;
130 174
131 function "&" 175 function "&"
132 (Left : Unbounded_String; 176 (Left : Unbounded_String;
133 Right : Character) return Unbounded_String; 177 Right : Character) return Unbounded_String
178 with
179 Pre => Length (Left) < Natural'Last,
180 Post => Length ("&"'Result) = Length (Left) + 1,
181 Global => null;
134 182
135 function "&" 183 function "&"
136 (Left : Character; 184 (Left : Character;
137 Right : Unbounded_String) return Unbounded_String; 185 Right : Unbounded_String) return Unbounded_String
186 with
187 Pre => Length (Right) < Natural'Last,
188 Post => Length ("&"'Result) = Length (Right) + 1,
189 Global => null;
138 190
139 function Element 191 function Element
140 (Source : Unbounded_String; 192 (Source : Unbounded_String;
141 Index : Positive) return Character; 193 Index : Positive) return Character
194 with
195 Pre => Index <= Length (Source),
196 Global => null;
142 197
143 procedure Replace_Element 198 procedure Replace_Element
144 (Source : in out Unbounded_String; 199 (Source : in out Unbounded_String;
145 Index : Positive; 200 Index : Positive;
146 By : Character); 201 By : Character)
202 with
203 Pre => Index <= Length (Source),
204 Post => Length (Source) = Length (Source)'Old,
205 Global => null;
147 206
148 function Slice 207 function Slice
149 (Source : Unbounded_String; 208 (Source : Unbounded_String;
150 Low : Positive; 209 Low : Positive;
151 High : Natural) return String; 210 High : Natural) return String
211 with
212 Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
213 Post => Slice'Result'Length = Natural'Max (0, High - Low + 1),
214 Global => null;
152 215
153 function Unbounded_Slice 216 function Unbounded_Slice
154 (Source : Unbounded_String; 217 (Source : Unbounded_String;
155 Low : Positive; 218 Low : Positive;
156 High : Natural) return Unbounded_String; 219 High : Natural) return Unbounded_String
220 with
221 Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
222 Post =>
223 Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
224 Global => null;
157 pragma Ada_05 (Unbounded_Slice); 225 pragma Ada_05 (Unbounded_Slice);
158 226
159 procedure Unbounded_Slice 227 procedure Unbounded_Slice
160 (Source : Unbounded_String; 228 (Source : Unbounded_String;
161 Target : out Unbounded_String; 229 Target : out Unbounded_String;
162 Low : Positive; 230 Low : Positive;
163 High : Natural); 231 High : Natural)
232 with
233 Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
234 Post => Length (Target) = Natural'Max (0, High - Low + 1),
235 Global => null;
164 pragma Ada_05 (Unbounded_Slice); 236 pragma Ada_05 (Unbounded_Slice);
165 237
166 function "=" 238 function "="
167 (Left : Unbounded_String; 239 (Left : Unbounded_String;
168 Right : Unbounded_String) return Boolean; 240 Right : Unbounded_String) return Boolean
241 with
242 Global => null;
169 243
170 function "=" 244 function "="
171 (Left : Unbounded_String; 245 (Left : Unbounded_String;
172 Right : String) return Boolean; 246 Right : String) return Boolean
247 with
248 Global => null;
173 249
174 function "=" 250 function "="
175 (Left : String; 251 (Left : String;
176 Right : Unbounded_String) return Boolean; 252 Right : Unbounded_String) return Boolean
253 with
254 Global => null;
177 255
178 function "<" 256 function "<"
179 (Left : Unbounded_String; 257 (Left : Unbounded_String;
180 Right : Unbounded_String) return Boolean; 258 Right : Unbounded_String) return Boolean
259 with
260 Global => null;
181 261
182 function "<" 262 function "<"
183 (Left : Unbounded_String; 263 (Left : Unbounded_String;
184 Right : String) return Boolean; 264 Right : String) return Boolean
265 with
266 Global => null;
185 267
186 function "<" 268 function "<"
187 (Left : String; 269 (Left : String;
188 Right : Unbounded_String) return Boolean; 270 Right : Unbounded_String) return Boolean
271 with
272 Global => null;
189 273
190 function "<=" 274 function "<="
191 (Left : Unbounded_String; 275 (Left : Unbounded_String;
192 Right : Unbounded_String) return Boolean; 276 Right : Unbounded_String) return Boolean
277 with
278 Global => null;
193 279
194 function "<=" 280 function "<="
195 (Left : Unbounded_String; 281 (Left : Unbounded_String;
196 Right : String) return Boolean; 282 Right : String) return Boolean
283 with
284 Global => null;
197 285
198 function "<=" 286 function "<="
199 (Left : String; 287 (Left : String;
200 Right : Unbounded_String) return Boolean; 288 Right : Unbounded_String) return Boolean
289 with
290 Global => null;
201 291
202 function ">" 292 function ">"
203 (Left : Unbounded_String; 293 (Left : Unbounded_String;
204 Right : Unbounded_String) return Boolean; 294 Right : Unbounded_String) return Boolean
295 with
296 Global => null;
205 297
206 function ">" 298 function ">"
207 (Left : Unbounded_String; 299 (Left : Unbounded_String;
208 Right : String) return Boolean; 300 Right : String) return Boolean
301 with
302 Global => null;
209 303
210 function ">" 304 function ">"
211 (Left : String; 305 (Left : String;
212 Right : Unbounded_String) return Boolean; 306 Right : Unbounded_String) return Boolean
307 with
308 Global => null;
213 309
214 function ">=" 310 function ">="
215 (Left : Unbounded_String; 311 (Left : Unbounded_String;
216 Right : Unbounded_String) return Boolean; 312 Right : Unbounded_String) return Boolean
313 with
314 Global => null;
217 315
218 function ">=" 316 function ">="
219 (Left : Unbounded_String; 317 (Left : Unbounded_String;
220 Right : String) return Boolean; 318 Right : String) return Boolean
319 with
320 Global => null;
221 321
222 function ">=" 322 function ">="
223 (Left : String; 323 (Left : String;
224 Right : Unbounded_String) return Boolean; 324 Right : Unbounded_String) return Boolean
325 with
326 Global => null;
225 327
226 ------------------------ 328 ------------------------
227 -- Search Subprograms -- 329 -- Search Subprograms --
228 ------------------------ 330 ------------------------
229 331
230 function Index 332 function Index
231 (Source : Unbounded_String; 333 (Source : Unbounded_String;
232 Pattern : String; 334 Pattern : String;
233 Going : Direction := Forward; 335 Going : Direction := Forward;
234 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; 336 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
337 with
338 Pre => Pattern'Length /= 0,
339 Global => null;
235 340
236 function Index 341 function Index
237 (Source : Unbounded_String; 342 (Source : Unbounded_String;
238 Pattern : String; 343 Pattern : String;
239 Going : Direction := Forward; 344 Going : Direction := Forward;
240 Mapping : Maps.Character_Mapping_Function) return Natural; 345 Mapping : Maps.Character_Mapping_Function) return Natural
346 with
347 Pre => Pattern'Length /= 0,
348 Global => null;
241 349
242 function Index 350 function Index
243 (Source : Unbounded_String; 351 (Source : Unbounded_String;
244 Set : Maps.Character_Set; 352 Set : Maps.Character_Set;
245 Test : Membership := Inside; 353 Test : Membership := Inside;
246 Going : Direction := Forward) return Natural; 354 Going : Direction := Forward) return Natural
355 with
356 Global => null;
247 357
248 function Index 358 function Index
249 (Source : Unbounded_String; 359 (Source : Unbounded_String;
250 Pattern : String; 360 Pattern : String;
251 From : Positive; 361 From : Positive;
252 Going : Direction := Forward; 362 Going : Direction := Forward;
253 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; 363 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
364 with
365 Pre => (if Length (Source) /= 0
366 then From <= Length (Source))
367 and then Pattern'Length /= 0,
368 Global => null;
254 pragma Ada_05 (Index); 369 pragma Ada_05 (Index);
255 370
256 function Index 371 function Index
257 (Source : Unbounded_String; 372 (Source : Unbounded_String;
258 Pattern : String; 373 Pattern : String;
259 From : Positive; 374 From : Positive;
260 Going : Direction := Forward; 375 Going : Direction := Forward;
261 Mapping : Maps.Character_Mapping_Function) return Natural; 376 Mapping : Maps.Character_Mapping_Function) return Natural
377 with
378 Pre => (if Length (Source) /= 0
379 then From <= Length (Source))
380 and then Pattern'Length /= 0,
381 Global => null;
382
262 pragma Ada_05 (Index); 383 pragma Ada_05 (Index);
263 384
264 function Index 385 function Index
265 (Source : Unbounded_String; 386 (Source : Unbounded_String;
266 Set : Maps.Character_Set; 387 Set : Maps.Character_Set;
267 From : Positive; 388 From : Positive;
268 Test : Membership := Inside; 389 Test : Membership := Inside;
269 Going : Direction := Forward) return Natural; 390 Going : Direction := Forward) return Natural
391 with
392 Pre => (if Length (Source) /= 0 then From <= Length (Source)),
393 Global => null;
270 pragma Ada_05 (Index); 394 pragma Ada_05 (Index);
271 395
272 function Index_Non_Blank 396 function Index_Non_Blank
273 (Source : Unbounded_String; 397 (Source : Unbounded_String;
274 Going : Direction := Forward) return Natural; 398 Going : Direction := Forward) return Natural
399 with
400 Global => null;
275 401
276 function Index_Non_Blank 402 function Index_Non_Blank
277 (Source : Unbounded_String; 403 (Source : Unbounded_String;
278 From : Positive; 404 From : Positive;
279 Going : Direction := Forward) return Natural; 405 Going : Direction := Forward) return Natural
406 with
407 Pre => (if Length (Source) /= 0 then From <= Length (Source)),
408 Global => null;
280 pragma Ada_05 (Index_Non_Blank); 409 pragma Ada_05 (Index_Non_Blank);
281 410
282 function Count 411 function Count
283 (Source : Unbounded_String; 412 (Source : Unbounded_String;
284 Pattern : String; 413 Pattern : String;
285 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural; 414 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
415 with
416 Pre => Pattern'Length /= 0,
417 Global => null;
286 418
287 function Count 419 function Count
288 (Source : Unbounded_String; 420 (Source : Unbounded_String;
289 Pattern : String; 421 Pattern : String;
290 Mapping : Maps.Character_Mapping_Function) return Natural; 422 Mapping : Maps.Character_Mapping_Function) return Natural
423 with
424 Pre => Pattern'Length /= 0,
425 Global => null;
291 426
292 function Count 427 function Count
293 (Source : Unbounded_String; 428 (Source : Unbounded_String;
294 Set : Maps.Character_Set) return Natural; 429 Set : Maps.Character_Set) return Natural
430 with
431 Global => null;
295 432
296 procedure Find_Token 433 procedure Find_Token
297 (Source : Unbounded_String; 434 (Source : Unbounded_String;
298 Set : Maps.Character_Set; 435 Set : Maps.Character_Set;
299 From : Positive; 436 From : Positive;
300 Test : Membership; 437 Test : Membership;
301 First : out Positive; 438 First : out Positive;
302 Last : out Natural); 439 Last : out Natural)
440 with
441 Pre => (if Length (Source) /= 0 then From <= Length (Source)),
442 Global => null;
303 pragma Ada_2012 (Find_Token); 443 pragma Ada_2012 (Find_Token);
304 444
305 procedure Find_Token 445 procedure Find_Token
306 (Source : Unbounded_String; 446 (Source : Unbounded_String;
307 Set : Maps.Character_Set; 447 Set : Maps.Character_Set;
308 Test : Membership; 448 Test : Membership;
309 First : out Positive; 449 First : out Positive;
310 Last : out Natural); 450 Last : out Natural)
451 with
452 Global => null;
311 453
312 ------------------------------------ 454 ------------------------------------
313 -- String Translation Subprograms -- 455 -- String Translation Subprograms --
314 ------------------------------------ 456 ------------------------------------
315 457
316 function Translate 458 function Translate
317 (Source : Unbounded_String; 459 (Source : Unbounded_String;
318 Mapping : Maps.Character_Mapping) return Unbounded_String; 460 Mapping : Maps.Character_Mapping) return Unbounded_String
461 with
462 Post => Length (Translate'Result) = Length (Source),
463 Global => null;
319 464
320 procedure Translate 465 procedure Translate
321 (Source : in out Unbounded_String; 466 (Source : in out Unbounded_String;
322 Mapping : Maps.Character_Mapping); 467 Mapping : Maps.Character_Mapping)
468 with
469 Post => Length (Source) = Length (Source)'Old,
470 Global => null;
323 471
324 function Translate 472 function Translate
325 (Source : Unbounded_String; 473 (Source : Unbounded_String;
326 Mapping : Maps.Character_Mapping_Function) return Unbounded_String; 474 Mapping : Maps.Character_Mapping_Function) return Unbounded_String
475 with
476 Post => Length (Translate'Result) = Length (Source),
477 Global => null;
327 478
328 procedure Translate 479 procedure Translate
329 (Source : in out Unbounded_String; 480 (Source : in out Unbounded_String;
330 Mapping : Maps.Character_Mapping_Function); 481 Mapping : Maps.Character_Mapping_Function)
482 with
483 Post => Length (Source) = Length (Source)'Old,
484 Global => null;
331 485
332 --------------------------------------- 486 ---------------------------------------
333 -- String Transformation Subprograms -- 487 -- String Transformation Subprograms --
334 --------------------------------------- 488 ---------------------------------------
335 489
336 function Replace_Slice 490 function Replace_Slice
337 (Source : Unbounded_String; 491 (Source : Unbounded_String;
338 Low : Positive; 492 Low : Positive;
339 High : Natural; 493 High : Natural;
340 By : String) return Unbounded_String; 494 By : String) return Unbounded_String
495 with
496 Pre =>
497 Low - 1 <= Length (Source)
498 and then (if High >= Low
499 then Low - 1
500 <= Natural'Last - By'Length
501 - Natural'Max (Length (Source) - High, 0)
502 else Length (Source) <= Natural'Last - By'Length),
503 Contract_Cases =>
504 (High >= Low =>
505 Length (Replace_Slice'Result)
506 = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
507 others =>
508 Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
509 Global => null;
341 510
342 procedure Replace_Slice 511 procedure Replace_Slice
343 (Source : in out Unbounded_String; 512 (Source : in out Unbounded_String;
344 Low : Positive; 513 Low : Positive;
345 High : Natural; 514 High : Natural;
346 By : String); 515 By : String)
516 with
517 Pre =>
518 Low - 1 <= Length (Source)
519 and then (if High >= Low
520 then Low - 1
521 <= Natural'Last - By'Length
522 - Natural'Max (Length (Source) - High, 0)
523 else Length (Source) <= Natural'Last - By'Length),
524 Contract_Cases =>
525 (High >= Low =>
526 Length (Source)
527 = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
528 others =>
529 Length (Source) = Length (Source)'Old + By'Length),
530 Global => null;
347 531
348 function Insert 532 function Insert
349 (Source : Unbounded_String; 533 (Source : Unbounded_String;
350 Before : Positive; 534 Before : Positive;
351 New_Item : String) return Unbounded_String; 535 New_Item : String) return Unbounded_String
536 with
537 Pre => Before - 1 <= Length (Source)
538 and then New_Item'Length <= Natural'Last - Length (Source),
539 Post => Length (Insert'Result) = Length (Source) + New_Item'Length,
540 Global => null;
352 541
353 procedure Insert 542 procedure Insert
354 (Source : in out Unbounded_String; 543 (Source : in out Unbounded_String;
355 Before : Positive; 544 Before : Positive;
356 New_Item : String); 545 New_Item : String)
546 with
547 Pre => Before - 1 <= Length (Source)
548 and then New_Item'Length <= Natural'Last - Length (Source),
549 Post => Length (Source) = Length (Source)'Old + New_Item'Length,
550 Global => null;
357 551
358 function Overwrite 552 function Overwrite
359 (Source : Unbounded_String; 553 (Source : Unbounded_String;
360 Position : Positive; 554 Position : Positive;
361 New_Item : String) return Unbounded_String; 555 New_Item : String) return Unbounded_String
556 with
557 Pre => Position - 1 <= Length (Source)
558 and then (if New_Item'Length /= 0
559 then
560 New_Item'Length <= Natural'Last - (Position - 1)),
561 Post =>
562 Length (Overwrite'Result)
563 = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
564 Global => null;
362 565
363 procedure Overwrite 566 procedure Overwrite
364 (Source : in out Unbounded_String; 567 (Source : in out Unbounded_String;
365 Position : Positive; 568 Position : Positive;
366 New_Item : String); 569 New_Item : String)
570 with
571 Pre => Position - 1 <= Length (Source)
572 and then (if New_Item'Length /= 0
573 then
574 New_Item'Length <= Natural'Last - (Position - 1)),
575 Post =>
576 Length (Source)
577 = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
578
579 Global => null;
367 580
368 function Delete 581 function Delete
369 (Source : Unbounded_String; 582 (Source : Unbounded_String;
370 From : Positive; 583 From : Positive;
371 Through : Natural) return Unbounded_String; 584 Through : Natural) return Unbounded_String
585 with
586 Pre => (if Through <= From then From - 1 <= Length (Source)),
587 Contract_Cases =>
588 (Through >= From =>
589 Length (Delete'Result) = Length (Source) - (Through - From + 1),
590 others =>
591 Length (Delete'Result) = Length (Source)),
592 Global => null;
372 593
373 procedure Delete 594 procedure Delete
374 (Source : in out Unbounded_String; 595 (Source : in out Unbounded_String;
375 From : Positive; 596 From : Positive;
376 Through : Natural); 597 Through : Natural)
598 with
599 Pre => (if Through <= From then From - 1 <= Length (Source)),
600 Contract_Cases =>
601 (Through >= From =>
602 Length (Source) = Length (Source)'Old - (Through - From + 1),
603 others =>
604 Length (Source) = Length (Source)'Old),
605 Global => null;
377 606
378 function Trim 607 function Trim
379 (Source : Unbounded_String; 608 (Source : Unbounded_String;
380 Side : Trim_End) return Unbounded_String; 609 Side : Trim_End) return Unbounded_String
610 with
611 Post => Length (Trim'Result) <= Length (Source),
612 Global => null;
381 613
382 procedure Trim 614 procedure Trim
383 (Source : in out Unbounded_String; 615 (Source : in out Unbounded_String;
384 Side : Trim_End); 616 Side : Trim_End)
617 with
618 Post => Length (Source) <= Length (Source)'Old,
619 Global => null;
385 620
386 function Trim 621 function Trim
387 (Source : Unbounded_String; 622 (Source : Unbounded_String;
388 Left : Maps.Character_Set; 623 Left : Maps.Character_Set;
389 Right : Maps.Character_Set) return Unbounded_String; 624 Right : Maps.Character_Set) return Unbounded_String
625 with
626 Post => Length (Trim'Result) <= Length (Source),
627 Global => null;
390 628
391 procedure Trim 629 procedure Trim
392 (Source : in out Unbounded_String; 630 (Source : in out Unbounded_String;
393 Left : Maps.Character_Set; 631 Left : Maps.Character_Set;
394 Right : Maps.Character_Set); 632 Right : Maps.Character_Set)
633 with
634 Post => Length (Source) <= Length (Source)'Old,
635 Global => null;
395 636
396 function Head 637 function Head
397 (Source : Unbounded_String; 638 (Source : Unbounded_String;
398 Count : Natural; 639 Count : Natural;
399 Pad : Character := Space) return Unbounded_String; 640 Pad : Character := Space) return Unbounded_String
641 with
642 Post => Length (Head'Result) = Count,
643 Global => null;
400 644
401 procedure Head 645 procedure Head
402 (Source : in out Unbounded_String; 646 (Source : in out Unbounded_String;
403 Count : Natural; 647 Count : Natural;
404 Pad : Character := Space); 648 Pad : Character := Space)
649 with
650 Post => Length (Source) = Count,
651 Global => null;
405 652
406 function Tail 653 function Tail
407 (Source : Unbounded_String; 654 (Source : Unbounded_String;
408 Count : Natural; 655 Count : Natural;
409 Pad : Character := Space) return Unbounded_String; 656 Pad : Character := Space) return Unbounded_String
657 with
658 Post => Length (Tail'Result) = Count,
659 Global => null;
410 660
411 procedure Tail 661 procedure Tail
412 (Source : in out Unbounded_String; 662 (Source : in out Unbounded_String;
413 Count : Natural; 663 Count : Natural;
414 Pad : Character := Space); 664 Pad : Character := Space)
665 with
666 Post => Length (Source) = Count,
667 Global => null;
415 668
416 function "*" 669 function "*"
417 (Left : Natural; 670 (Left : Natural;
418 Right : Character) return Unbounded_String; 671 Right : Character) return Unbounded_String
672 with
673 Pre => Left <= Natural'Last,
674 Post => Length ("*"'Result) = Left,
675 Global => null;
419 676
420 function "*" 677 function "*"
421 (Left : Natural; 678 (Left : Natural;
422 Right : String) return Unbounded_String; 679 Right : String) return Unbounded_String
680 with
681 Pre => (if Left /= 0 then Right'Length <= Natural'Last / Left),
682 Post => Length ("*"'Result) = Left * Right'Length,
683 Global => null;
423 684
424 function "*" 685 function "*"
425 (Left : Natural; 686 (Left : Natural;
426 Right : Unbounded_String) return Unbounded_String; 687 Right : Unbounded_String) return Unbounded_String
688 with
689 Pre => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
690 Post => Length ("*"'Result) = Left * Length (Right),
691 Global => null;
427 692
428 private 693 private
429 pragma Inline (Length); 694 pragma Inline (Length);
430 695
431 package AF renames Ada.Finalization; 696 package AF renames Ada.Finalization;