1------------------------------------------------------------------------------ 2-- -- 3-- GNAT RUN-TIME COMPONENTS -- 4-- -- 5-- A D A . S T R I N G S . S E A R C H -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 1992-2021, Free Software Foundation, Inc. -- 10-- -- 11-- GNAT is free software; you can redistribute it and/or modify it under -- 12-- terms of the GNU General Public License as published by the Free Soft- -- 13-- ware Foundation; either version 3, or (at your option) any later ver- -- 14-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 15-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 16-- or FITNESS FOR A PARTICULAR PURPOSE. -- 17-- -- 18-- As a special exception under Section 7 of GPL version 3, you are granted -- 19-- additional permissions described in the GCC Runtime Library Exception, -- 20-- version 3.1, as published by the Free Software Foundation. -- 21-- -- 22-- You should have received a copy of the GNU General Public License and -- 23-- a copy of the GCC Runtime Library Exception along with this program; -- 24-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- 25-- <http://www.gnu.org/licenses/>. -- 26-- -- 27-- GNAT was originally developed by the GNAT team at New York University. -- 28-- Extensive contributions were provided by Ada Core Technologies Inc. -- 29-- -- 30------------------------------------------------------------------------------ 31 32-- This package contains the search functions from Ada.Strings.Fixed. They 33-- are separated out because they are shared by Ada.Strings.Bounded and 34-- Ada.Strings.Unbounded, and we don't want to drag in other irrelevant stuff 35-- from Ada.Strings.Fixed when using the other two packages. Although user 36-- programs should access these subprograms via one of the standard string 37-- packages, we do not make this a private package, since ghost function 38-- Match is used in the contracts of the standard string packages. 39 40-- Preconditions in this unit are meant for analysis only, not for run-time 41-- checking, so that the expected exceptions are raised. This is enforced 42-- by setting the corresponding assertion policy to Ignore. Postconditions, 43-- contract cases and ghost code should not be executed at runtime as well, 44-- in order not to slow down the execution of these functions. 45 46pragma Assertion_Policy (Pre => Ignore, 47 Post => Ignore, 48 Contract_Cases => Ignore, 49 Ghost => Ignore); 50 51with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; 52 53package Ada.Strings.Search with SPARK_Mode is 54 pragma Preelaborate; 55 56 -- The ghost function Match tells whether the slice of Source starting at 57 -- From and of length Pattern'Length matches with Pattern with respect to 58 -- Mapping. Pattern should be non-empty and the considered slice should be 59 -- fully included in Source'Range. 60 61 function Match 62 (Source : String; 63 Pattern : String; 64 Mapping : Maps.Character_Mapping_Function; 65 From : Integer) return Boolean 66 is 67 (for all K in Pattern'Range => 68 Pattern (K) = Mapping (Source (From + (K - Pattern'First)))) 69 with 70 Ghost, 71 Pre => Mapping /= null 72 and then Pattern'Length > 0 73 and then Source'Length > 0 74 and then From in Source'First .. Source'Last - (Pattern'Length - 1), 75 Global => null; 76 77 function Match 78 (Source : String; 79 Pattern : String; 80 Mapping : Maps.Character_Mapping; 81 From : Integer) return Boolean 82 is 83 (for all K in Pattern'Range => 84 Pattern (K) = 85 Ada.Strings.Maps.Value 86 (Mapping, Source (From + (K - Pattern'First)))) 87 with 88 Ghost, 89 Pre => Pattern'Length > 0 90 and then Source'Length > 0 91 and then From in Source'First .. Source'Last - (Pattern'Length - 1), 92 Global => null; 93 94 function Is_Identity 95 (Mapping : Maps.Character_Mapping) return Boolean 96 with 97 Post => (if Is_Identity'Result then 98 (for all K in Character => 99 Ada.Strings.Maps.Value (Mapping, K) = K)), 100 Global => null; 101 102 function Index 103 (Source : String; 104 Pattern : String; 105 Going : Direction := Forward; 106 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural 107 with 108 Pre => Pattern'Length > 0, 109 110 Post => Index'Result in 0 | Source'Range, 111 Contract_Cases => 112 113 -- If Source is the empty string, then 0 is returned 114 115 (Source'Length = 0 => Index'Result = 0, 116 117 -- If some slice of Source matches Pattern, then a valid index is 118 -- returned. 119 120 Source'Length > 0 121 and then 122 (for some J in 123 Source'First .. Source'Last - (Pattern'Length - 1) => 124 Match (Source, Pattern, Mapping, J)) 125 => 126 127 -- The result is in the considered range of Source 128 129 Index'Result in Source'First .. Source'Last - (Pattern'Length - 1) 130 131 -- The slice beginning at the returned index matches Pattern 132 133 and then Match (Source, Pattern, Mapping, Index'Result) 134 135 -- The result is the smallest or largest index which satisfies 136 -- the matching, respectively when Going = Forward and Going = 137 -- Backward. 138 139 and then 140 (for all J in Source'Range => 141 (if (if Going = Forward 142 then J <= Index'Result - 1 143 else J - 1 in Index'Result 144 .. Source'Last - Pattern'Length) 145 then not (Match (Source, Pattern, Mapping, J)))), 146 147 -- Otherwise, 0 is returned 148 149 others => Index'Result = 0), 150 Global => null; 151 152 function Index 153 (Source : String; 154 Pattern : String; 155 Going : Direction := Forward; 156 Mapping : Maps.Character_Mapping_Function) return Natural 157 with 158 Pre => Pattern'Length > 0 and then Mapping /= null, 159 Post => Index'Result in 0 | Source'Range, 160 Contract_Cases => 161 162 -- If Source is the null string, then 0 is returned 163 164 (Source'Length = 0 => Index'Result = 0, 165 166 -- If some slice of Source matches Pattern, then a valid index is 167 -- returned. 168 169 Source'Length > 0 and then 170 (for some J in Source'First .. Source'Last - (Pattern'Length - 1) => 171 Match (Source, Pattern, Mapping, J)) 172 => 173 174 -- The result is in the considered range of Source 175 176 Index'Result in Source'First .. Source'Last - (Pattern'Length - 1) 177 178 -- The slice beginning at the returned index matches Pattern 179 180 and then Match (Source, Pattern, Mapping, Index'Result) 181 182 -- The result is the smallest or largest index which satisfies 183 -- the matching, respectively when Going = Forward and Going = 184 -- Backward. 185 186 and then 187 (for all J in Source'Range => 188 (if (if Going = Forward 189 then J <= Index'Result - 1 190 else J - 1 in Index'Result 191 .. Source'Last - Pattern'Length) 192 then not (Match (Source, Pattern, Mapping, J)))), 193 194 -- Otherwise, 0 is returned 195 196 others => Index'Result = 0), 197 Global => null; 198 199 function Index 200 (Source : String; 201 Set : Maps.Character_Set; 202 Test : Membership := Inside; 203 Going : Direction := Forward) return Natural 204 with 205 Post => Index'Result in 0 | Source'Range, 206 Contract_Cases => 207 208 -- If no character of Source satisfies the property Test on Set, then 209 -- 0 is returned. 210 211 ((for all C of Source => 212 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) 213 => 214 Index'Result = 0, 215 216 -- Otherwise, an index in the range of Source is returned 217 218 others => 219 220 -- The result is in the range of Source 221 222 Index'Result in Source'Range 223 224 -- The character at the returned index satisfies the property 225 -- Test on Set. 226 227 and then (Test = Inside) 228 = Ada.Strings.Maps.Is_In (Source (Index'Result), Set) 229 230 -- The result is the smallest or largest index which satisfies 231 -- the property, respectively when Going = Forward and Going = 232 -- Backward. 233 234 and then 235 (for all J in Source'Range => 236 (if J /= Index'Result 237 and then (J < Index'Result) = (Going = Forward) 238 then (Test = Inside) 239 /= Ada.Strings.Maps.Is_In (Source (J), Set)))), 240 Global => null; 241 242 function Index 243 (Source : String; 244 Pattern : String; 245 From : Positive; 246 Going : Direction := Forward; 247 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural 248 with 249 Pre => Pattern'Length > 0 250 and then (if Source'Length > 0 then From in Source'Range), 251 252 Post => Index'Result in 0 | Source'Range, 253 Contract_Cases => 254 255 -- If Source is the empty string, then 0 is returned 256 257 (Source'Length = 0 => Index'Result = 0, 258 259 -- If some slice of Source matches Pattern, then a valid index is 260 -- returned. 261 262 Source'Length > 0 263 and then 264 (for some J in 265 (if Going = Forward then From else Source'First) 266 .. (if Going = Forward then Source'Last else From) 267 - (Pattern'Length - 1) => 268 Match (Source, Pattern, Mapping, J)) 269 => 270 271 -- The result is in the considered range of Source 272 273 Index'Result in 274 (if Going = Forward then From else Source'First) 275 .. (if Going = Forward then Source'Last else From) 276 - (Pattern'Length - 1) 277 278 -- The slice beginning at the returned index matches Pattern 279 280 and then Match (Source, Pattern, Mapping, Index'Result) 281 282 -- The result is the smallest or largest index which satisfies 283 -- the matching, respectively when Going = Forward and Going = 284 -- Backward. 285 286 and then 287 (for all J in Source'Range => 288 (if (if Going = Forward 289 then J in From .. Index'Result - 1 290 else J - 1 in Index'Result 291 .. From - Pattern'Length) 292 then not (Match (Source, Pattern, Mapping, J)))), 293 294 -- Otherwise, 0 is returned 295 296 others => Index'Result = 0), 297 Global => null; 298 299 function Index 300 (Source : String; 301 Pattern : String; 302 From : Positive; 303 Going : Direction := Forward; 304 Mapping : Maps.Character_Mapping_Function) return Natural 305 with 306 Pre => Pattern'Length > 0 307 and then Mapping /= null 308 and then (if Source'Length > 0 then From in Source'Range), 309 310 Post => Index'Result in 0 | Source'Range, 311 Contract_Cases => 312 313 -- If Source is the empty string, then 0 is returned 314 315 (Source'Length = 0 => Index'Result = 0, 316 317 -- If some slice of Source matches Pattern, then a valid index is 318 -- returned. 319 320 Source'Length > 0 321 and then 322 (for some J in 323 (if Going = Forward then From else Source'First) 324 .. (if Going = Forward then Source'Last else From) 325 - (Pattern'Length - 1) => 326 Match (Source, Pattern, Mapping, J)) 327 => 328 329 -- The result is in the considered range of Source 330 331 Index'Result in 332 (if Going = Forward then From else Source'First) 333 .. (if Going = Forward then Source'Last else From) 334 - (Pattern'Length - 1) 335 336 -- The slice beginning at the returned index matches Pattern 337 338 and then Match (Source, Pattern, Mapping, Index'Result) 339 340 -- The result is the smallest or largest index which satisfies 341 -- the matching, respectively when Going = Forward and Going = 342 -- Backwards. 343 344 and then 345 (for all J in Source'Range => 346 (if (if Going = Forward 347 then J in From .. Index'Result - 1 348 else J - 1 in Index'Result 349 .. From - Pattern'Length) 350 then not (Match (Source, Pattern, Mapping, J)))), 351 352 -- Otherwise, 0 is returned 353 354 others => Index'Result = 0), 355 Global => null; 356 357 function Index 358 (Source : String; 359 Set : Maps.Character_Set; 360 From : Positive; 361 Test : Membership := Inside; 362 Going : Direction := Forward) return Natural 363 with 364 Pre => (if Source'Length > 0 then From in Source'Range), 365 Post => Index'Result in 0 | Source'Range, 366 Contract_Cases => 367 368 -- If Source is the empty string, or no character of the considered 369 -- slice of Source satisfies the property Test on Set, then 0 is 370 -- returned. 371 372 (Source'Length = 0 373 or else 374 (for all J in Source'Range => 375 (if J = From or else (J > From) = (Going = Forward) then 376 (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set))) 377 => 378 Index'Result = 0, 379 380 -- Otherwise, an index in the considered range of Source is returned 381 382 others => 383 384 -- The result is in the considered range of Source 385 386 Index'Result in Source'Range 387 and then (Index'Result = From 388 or else 389 (Index'Result > From) = (Going = Forward)) 390 391 -- The character at the returned index satisfies the property 392 -- Test on Set 393 394 and then 395 (Test = Inside) 396 = Ada.Strings.Maps.Is_In (Source (Index'Result), Set) 397 398 -- The result is the smallest or largest index which satisfies 399 -- the property, respectively when Going = Forward and Going = 400 -- Backward. 401 402 and then 403 (for all J in Source'Range => 404 (if J /= Index'Result 405 and then (J < Index'Result) = (Going = Forward) 406 and then (J = From 407 or else (J > From) = (Going = Forward)) 408 then (Test = Inside) 409 /= Ada.Strings.Maps.Is_In (Source (J), Set)))), 410 Global => null; 411 412 function Index_Non_Blank 413 (Source : String; 414 Going : Direction := Forward) return Natural 415 with 416 Post => Index_Non_Blank'Result in 0 | Source'Range, 417 Contract_Cases => 418 419 -- If all characters of Source are Space characters, then 0 is 420 -- returned. 421 422 ((for all C of Source => C = ' ') => Index_Non_Blank'Result = 0, 423 424 -- Otherwise, a valid index is returned 425 426 others => 427 428 -- The result is in the range of Source 429 430 Index_Non_Blank'Result in Source'Range 431 432 -- The character at the returned index is not a Space character 433 434 and then Source (Index_Non_Blank'Result) /= ' ' 435 436 -- The result is the smallest or largest index which is not a 437 -- Space character, respectively when Going = Forward and 438 -- Going = Backward. 439 440 and then 441 (for all J in Source'Range => 442 (if J /= Index_Non_Blank'Result 443 and then (J < Index_Non_Blank'Result) 444 = (Going = Forward) 445 then Source (J) = ' '))), 446 Global => null; 447 448 function Index_Non_Blank 449 (Source : String; 450 From : Positive; 451 Going : Direction := Forward) return Natural 452 with 453 Pre => (if Source'Length /= 0 then From in Source'Range), 454 Post => Index_Non_Blank'Result in 0 | Source'Range, 455 Contract_Cases => 456 457 -- If Source is the null string, or all characters in the considered 458 -- slice of Source are Space characters, then 0 is returned. 459 460 (Source'Length = 0 461 or else 462 (for all J in Source'Range => 463 (if J = From or else (J > From) = (Going = Forward) then 464 Source (J) = ' ')) 465 => 466 Index_Non_Blank'Result = 0, 467 468 -- Otherwise, a valid index is returned 469 470 others => 471 472 -- The result is in the considered range of Source 473 474 Index_Non_Blank'Result in Source'Range 475 and then (Index_Non_Blank'Result = From 476 or else (Index_Non_Blank'Result > From) 477 = (Going = Forward)) 478 479 -- The character at the returned index is not a Space character 480 481 and then Source (Index_Non_Blank'Result) /= ' ' 482 483 -- The result is the smallest or largest index which is not a 484 -- Space character, respectively when Going = Forward and 485 -- Going = Backward. 486 487 and then 488 (for all J in Source'Range => 489 (if J /= Index_Non_Blank'Result 490 and then (J < Index_Non_Blank'Result) 491 = (Going = Forward) 492 and then (J = From or else (J > From) 493 = (Going = Forward)) 494 then Source (J) = ' '))), 495 Global => null; 496 497 function Count 498 (Source : String; 499 Pattern : String; 500 Mapping : Maps.Character_Mapping := Maps.Identity) return Natural 501 with 502 Pre => Pattern'Length > 0, 503 Global => null; 504 505 function Count 506 (Source : String; 507 Pattern : String; 508 Mapping : Maps.Character_Mapping_Function) return Natural 509 with 510 Pre => Pattern'Length > 0 and then Mapping /= null, 511 Global => null; 512 513 function Count 514 (Source : String; 515 Set : Maps.Character_Set) return Natural 516 with 517 Global => null; 518 519 procedure Find_Token 520 (Source : String; 521 Set : Maps.Character_Set; 522 From : Positive; 523 Test : Membership; 524 First : out Positive; 525 Last : out Natural) 526 with 527 Pre => (if Source'Length /= 0 then From in Source'Range), 528 Contract_Cases => 529 530 -- If Source is the empty string, or if no character of the considered 531 -- slice of Source satisfies the property Test on Set, then First is 532 -- set to From and Last is set to 0. 533 534 (Source'Length = 0 535 or else 536 (for all C of Source (From .. Source'Last) => 537 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) 538 => 539 First = From and then Last = 0, 540 541 -- Otherwise, First and Last are set to valid indexes 542 543 others => 544 545 -- First and Last are in the considered range of Source 546 547 First in From .. Source'Last 548 and then Last in First .. Source'Last 549 550 -- No character between From and First satisfies the property Test 551 -- on Set. 552 553 and then 554 (for all C of Source (From .. First - 1) => 555 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) 556 557 -- All characters between First and Last satisfy the property Test 558 -- on Set. 559 560 and then 561 (for all C of Source (First .. Last) => 562 (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set)) 563 564 -- If Last is not Source'Last, then the character at position 565 -- Last + 1 does not satify the property Test on Set. 566 567 and then 568 (if Last < Source'Last 569 then (Test = Inside) 570 /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), 571 Global => null; 572 573 procedure Find_Token 574 (Source : String; 575 Set : Maps.Character_Set; 576 Test : Membership; 577 First : out Positive; 578 Last : out Natural) 579 with 580 Pre => Source'First > 0, 581 Contract_Cases => 582 583 -- If Source is the empty string, or if no character of Source 584 -- satisfies the property Test on Set, then First is set to From 585 -- and Last is set to 0. 586 587 (Source'Length = 0 588 or else 589 (for all C of Source => 590 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) 591 => 592 First = Source'First and then Last = 0, 593 594 -- Otherwise, First and Last are set to valid indexes 595 596 others => 597 598 -- First and Last are in the considered range of Source 599 600 First in Source'Range 601 and then Last in First .. Source'Last 602 603 -- No character before First satisfies the property Test on Set 604 605 and then 606 (for all C of Source (Source'First .. First - 1) => 607 (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) 608 609 -- All characters between First and Last satisfy the property Test 610 -- on Set. 611 612 and then 613 (for all C of Source (First .. Last) => 614 (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set)) 615 616 -- If Last is not Source'Last, then the character at position 617 -- Last + 1 does not satify the property Test on Set. 618 619 and then 620 (if Last < Source'Last 621 then (Test = Inside) 622 /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), 623 Global => null; 624 625end Ada.Strings.Search; 626