| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT RUN-TIME COMPONENTS -- |
| -- -- |
| -- A D A . S T R I N G S . S E A R C H -- |
| -- -- |
| -- S p e c -- |
| -- -- |
| -- Copyright (C) 1992-2021, Free Software Foundation, Inc. -- |
| -- -- |
| -- GNAT is free software; you can redistribute it and/or modify it under -- |
| -- terms of the GNU General Public License as published by the Free Soft- -- |
| -- ware Foundation; either version 3, or (at your option) any later ver- -- |
| -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- |
| -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- |
| -- or FITNESS FOR A PARTICULAR PURPOSE. -- |
| -- -- |
| -- As a special exception under Section 7 of GPL version 3, you are granted -- |
| -- additional permissions described in the GCC Runtime Library Exception, -- |
| -- version 3.1, as published by the Free Software Foundation. -- |
| -- -- |
| -- You should have received a copy of the GNU General Public License and -- |
| -- a copy of the GCC Runtime Library Exception along with this program; -- |
| -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- |
| -- <http://www.gnu.org/licenses/>. -- |
| -- -- |
| -- GNAT was originally developed by the GNAT team at New York University. -- |
| -- Extensive contributions were provided by Ada Core Technologies Inc. -- |
| -- -- |
| ------------------------------------------------------------------------------ |
| |
| -- This package contains the search functions from Ada.Strings.Fixed. They |
| -- are separated out because they are shared by Ada.Strings.Bounded and |
| -- Ada.Strings.Unbounded, and we don't want to drag in other irrelevant stuff |
| -- from Ada.Strings.Fixed when using the other two packages. Although user |
| -- programs should access these subprograms via one of the standard string |
| -- packages, we do not make this a private package, since ghost function |
| -- Match is used in the contracts of the standard string packages. |
| |
| -- Preconditions in this unit are meant for analysis only, not for run-time |
| -- checking, so that the expected exceptions are raised. This is enforced |
| -- by setting the corresponding assertion policy to Ignore. Postconditions, |
| -- contract cases and ghost code should not be executed at runtime as well, |
| -- in order not to slow down the execution of these functions. |
| |
| pragma Assertion_Policy (Pre => Ignore, |
| Post => Ignore, |
| Contract_Cases => Ignore, |
| Ghost => Ignore); |
| |
| with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function; |
| |
| package Ada.Strings.Search with SPARK_Mode is |
| pragma Preelaborate; |
| |
| -- The ghost function Match tells whether the slice of Source starting at |
| -- From and of length Pattern'Length matches with Pattern with respect to |
| -- Mapping. Pattern should be non-empty and the considered slice should be |
| -- fully included in Source'Range. |
| |
| function Match |
| (Source : String; |
| Pattern : String; |
| Mapping : Maps.Character_Mapping_Function; |
| From : Integer) return Boolean |
| is |
| (for all K in Pattern'Range => |
| Pattern (K) = Mapping (Source (From + (K - Pattern'First)))) |
| with |
| Ghost, |
| Pre => Mapping /= null |
| and then Pattern'Length > 0 |
| and then Source'Length > 0 |
| and then From in Source'First .. Source'Last - (Pattern'Length - 1), |
| Global => null; |
| |
| function Match |
| (Source : String; |
| Pattern : String; |
| Mapping : Maps.Character_Mapping; |
| From : Integer) return Boolean |
| is |
| (for all K in Pattern'Range => |
| Pattern (K) = |
| Ada.Strings.Maps.Value |
| (Mapping, Source (From + (K - Pattern'First)))) |
| with |
| Ghost, |
| Pre => Pattern'Length > 0 |
| and then Source'Length > 0 |
| and then From in Source'First .. Source'Last - (Pattern'Length - 1), |
| Global => null; |
| |
| function Is_Identity |
| (Mapping : Maps.Character_Mapping) return Boolean |
| with |
| Post => (if Is_Identity'Result then |
| (for all K in Character => |
| Ada.Strings.Maps.Value (Mapping, K) = K)), |
| Global => null; |
| |
| function Index |
| (Source : String; |
| Pattern : String; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
| with |
| Pre => Pattern'Length > 0, |
| |
| Post => Index'Result in 0 | Source'Range, |
| Contract_Cases => |
| |
| -- If Source is the empty string, then 0 is returned |
| |
| (Source'Length = 0 => Index'Result = 0, |
| |
| -- If some slice of Source matches Pattern, then a valid index is |
| -- returned. |
| |
| Source'Length > 0 |
| and then |
| (for some J in |
| Source'First .. Source'Last - (Pattern'Length - 1) => |
| Match (Source, Pattern, Mapping, J)) |
| => |
| |
| -- The result is in the considered range of Source |
| |
| Index'Result in Source'First .. Source'Last - (Pattern'Length - 1) |
| |
| -- The slice beginning at the returned index matches Pattern |
| |
| and then Match (Source, Pattern, Mapping, Index'Result) |
| |
| -- The result is the smallest or largest index which satisfies |
| -- the matching, respectively when Going = Forward and Going = |
| -- Backward. |
| |
| and then |
| (for all J in Source'Range => |
| (if (if Going = Forward |
| then J <= Index'Result - 1 |
| else J - 1 in Index'Result |
| .. Source'Last - Pattern'Length) |
| then not (Match (Source, Pattern, Mapping, J)))), |
| |
| -- Otherwise, 0 is returned |
| |
| others => Index'Result = 0), |
| Global => null; |
| |
| function Index |
| (Source : String; |
| Pattern : String; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping_Function) return Natural |
| with |
| Pre => Pattern'Length > 0 and then Mapping /= null, |
| Post => Index'Result in 0 | Source'Range, |
| Contract_Cases => |
| |
| -- If Source is the null string, then 0 is returned |
| |
| (Source'Length = 0 => Index'Result = 0, |
| |
| -- If some slice of Source matches Pattern, then a valid index is |
| -- returned. |
| |
| Source'Length > 0 and then |
| (for some J in Source'First .. Source'Last - (Pattern'Length - 1) => |
| Match (Source, Pattern, Mapping, J)) |
| => |
| |
| -- The result is in the considered range of Source |
| |
| Index'Result in Source'First .. Source'Last - (Pattern'Length - 1) |
| |
| -- The slice beginning at the returned index matches Pattern |
| |
| and then Match (Source, Pattern, Mapping, Index'Result) |
| |
| -- The result is the smallest or largest index which satisfies |
| -- the matching, respectively when Going = Forward and Going = |
| -- Backward. |
| |
| and then |
| (for all J in Source'Range => |
| (if (if Going = Forward |
| then J <= Index'Result - 1 |
| else J - 1 in Index'Result |
| .. Source'Last - Pattern'Length) |
| then not (Match (Source, Pattern, Mapping, J)))), |
| |
| -- Otherwise, 0 is returned |
| |
| others => Index'Result = 0), |
| Global => null; |
| |
| function Index |
| (Source : String; |
| Set : Maps.Character_Set; |
| Test : Membership := Inside; |
| Going : Direction := Forward) return Natural |
| with |
| Post => Index'Result in 0 | Source'Range, |
| Contract_Cases => |
| |
| -- If no character of Source satisfies the property Test on Set, then |
| -- 0 is returned. |
| |
| ((for all C of Source => |
| (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) |
| => |
| Index'Result = 0, |
| |
| -- Otherwise, an index in the range of Source is returned |
| |
| others => |
| |
| -- The result is in the range of Source |
| |
| Index'Result in Source'Range |
| |
| -- The character at the returned index satisfies the property |
| -- Test on Set. |
| |
| and then (Test = Inside) |
| = Ada.Strings.Maps.Is_In (Source (Index'Result), Set) |
| |
| -- The result is the smallest or largest index which satisfies |
| -- the property, respectively when Going = Forward and Going = |
| -- Backward. |
| |
| and then |
| (for all J in Source'Range => |
| (if J /= Index'Result |
| and then (J < Index'Result) = (Going = Forward) |
| then (Test = Inside) |
| /= Ada.Strings.Maps.Is_In (Source (J), Set)))), |
| Global => null; |
| |
| function Index |
| (Source : String; |
| Pattern : String; |
| From : Positive; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
| with |
| Pre => Pattern'Length > 0 |
| and then (if Source'Length > 0 then From in Source'Range), |
| |
| Post => Index'Result in 0 | Source'Range, |
| Contract_Cases => |
| |
| -- If Source is the empty string, then 0 is returned |
| |
| (Source'Length = 0 => Index'Result = 0, |
| |
| -- If some slice of Source matches Pattern, then a valid index is |
| -- returned. |
| |
| Source'Length > 0 |
| and then |
| (for some J in |
| (if Going = Forward then From else Source'First) |
| .. (if Going = Forward then Source'Last else From) |
| - (Pattern'Length - 1) => |
| Match (Source, Pattern, Mapping, J)) |
| => |
| |
| -- The result is in the considered range of Source |
| |
| Index'Result in |
| (if Going = Forward then From else Source'First) |
| .. (if Going = Forward then Source'Last else From) |
| - (Pattern'Length - 1) |
| |
| -- The slice beginning at the returned index matches Pattern |
| |
| and then Match (Source, Pattern, Mapping, Index'Result) |
| |
| -- The result is the smallest or largest index which satisfies |
| -- the matching, respectively when Going = Forward and Going = |
| -- Backward. |
| |
| and then |
| (for all J in Source'Range => |
| (if (if Going = Forward |
| then J in From .. Index'Result - 1 |
| else J - 1 in Index'Result |
| .. From - Pattern'Length) |
| then not (Match (Source, Pattern, Mapping, J)))), |
| |
| -- Otherwise, 0 is returned |
| |
| others => Index'Result = 0), |
| Global => null; |
| |
| function Index |
| (Source : String; |
| Pattern : String; |
| From : Positive; |
| Going : Direction := Forward; |
| Mapping : Maps.Character_Mapping_Function) return Natural |
| with |
| Pre => Pattern'Length > 0 |
| and then Mapping /= null |
| and then (if Source'Length > 0 then From in Source'Range), |
| |
| Post => Index'Result in 0 | Source'Range, |
| Contract_Cases => |
| |
| -- If Source is the empty string, then 0 is returned |
| |
| (Source'Length = 0 => Index'Result = 0, |
| |
| -- If some slice of Source matches Pattern, then a valid index is |
| -- returned. |
| |
| Source'Length > 0 |
| and then |
| (for some J in |
| (if Going = Forward then From else Source'First) |
| .. (if Going = Forward then Source'Last else From) |
| - (Pattern'Length - 1) => |
| Match (Source, Pattern, Mapping, J)) |
| => |
| |
| -- The result is in the considered range of Source |
| |
| Index'Result in |
| (if Going = Forward then From else Source'First) |
| .. (if Going = Forward then Source'Last else From) |
| - (Pattern'Length - 1) |
| |
| -- The slice beginning at the returned index matches Pattern |
| |
| and then Match (Source, Pattern, Mapping, Index'Result) |
| |
| -- The result is the smallest or largest index which satisfies |
| -- the matching, respectively when Going = Forward and Going = |
| -- Backwards. |
| |
| and then |
| (for all J in Source'Range => |
| (if (if Going = Forward |
| then J in From .. Index'Result - 1 |
| else J - 1 in Index'Result |
| .. From - Pattern'Length) |
| then not (Match (Source, Pattern, Mapping, J)))), |
| |
| -- Otherwise, 0 is returned |
| |
| others => Index'Result = 0), |
| Global => null; |
| |
| function Index |
| (Source : String; |
| Set : Maps.Character_Set; |
| From : Positive; |
| Test : Membership := Inside; |
| Going : Direction := Forward) return Natural |
| with |
| Pre => (if Source'Length > 0 then From in Source'Range), |
| Post => Index'Result in 0 | Source'Range, |
| Contract_Cases => |
| |
| -- If Source is the empty string, or no character of the considered |
| -- slice of Source satisfies the property Test on Set, then 0 is |
| -- returned. |
| |
| (Source'Length = 0 |
| or else |
| (for all J in Source'Range => |
| (if J = From or else (J > From) = (Going = Forward) then |
| (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (J), Set))) |
| => |
| Index'Result = 0, |
| |
| -- Otherwise, an index in the considered range of Source is returned |
| |
| others => |
| |
| -- The result is in the considered range of Source |
| |
| Index'Result in Source'Range |
| and then (Index'Result = From |
| or else |
| (Index'Result > From) = (Going = Forward)) |
| |
| -- The character at the returned index satisfies the property |
| -- Test on Set |
| |
| and then |
| (Test = Inside) |
| = Ada.Strings.Maps.Is_In (Source (Index'Result), Set) |
| |
| -- The result is the smallest or largest index which satisfies |
| -- the property, respectively when Going = Forward and Going = |
| -- Backward. |
| |
| and then |
| (for all J in Source'Range => |
| (if J /= Index'Result |
| and then (J < Index'Result) = (Going = Forward) |
| and then (J = From |
| or else (J > From) = (Going = Forward)) |
| then (Test = Inside) |
| /= Ada.Strings.Maps.Is_In (Source (J), Set)))), |
| Global => null; |
| |
| function Index_Non_Blank |
| (Source : String; |
| Going : Direction := Forward) return Natural |
| with |
| Post => Index_Non_Blank'Result in 0 | Source'Range, |
| Contract_Cases => |
| |
| -- If all characters of Source are Space characters, then 0 is |
| -- returned. |
| |
| ((for all C of Source => C = ' ') => Index_Non_Blank'Result = 0, |
| |
| -- Otherwise, a valid index is returned |
| |
| others => |
| |
| -- The result is in the range of Source |
| |
| Index_Non_Blank'Result in Source'Range |
| |
| -- The character at the returned index is not a Space character |
| |
| and then Source (Index_Non_Blank'Result) /= ' ' |
| |
| -- The result is the smallest or largest index which is not a |
| -- Space character, respectively when Going = Forward and |
| -- Going = Backward. |
| |
| and then |
| (for all J in Source'Range => |
| (if J /= Index_Non_Blank'Result |
| and then (J < Index_Non_Blank'Result) |
| = (Going = Forward) |
| then Source (J) = ' '))), |
| Global => null; |
| |
| function Index_Non_Blank |
| (Source : String; |
| From : Positive; |
| Going : Direction := Forward) return Natural |
| with |
| Pre => (if Source'Length /= 0 then From in Source'Range), |
| Post => Index_Non_Blank'Result in 0 | Source'Range, |
| Contract_Cases => |
| |
| -- If Source is the null string, or all characters in the considered |
| -- slice of Source are Space characters, then 0 is returned. |
| |
| (Source'Length = 0 |
| or else |
| (for all J in Source'Range => |
| (if J = From or else (J > From) = (Going = Forward) then |
| Source (J) = ' ')) |
| => |
| Index_Non_Blank'Result = 0, |
| |
| -- Otherwise, a valid index is returned |
| |
| others => |
| |
| -- The result is in the considered range of Source |
| |
| Index_Non_Blank'Result in Source'Range |
| and then (Index_Non_Blank'Result = From |
| or else (Index_Non_Blank'Result > From) |
| = (Going = Forward)) |
| |
| -- The character at the returned index is not a Space character |
| |
| and then Source (Index_Non_Blank'Result) /= ' ' |
| |
| -- The result is the smallest or largest index which is not a |
| -- Space character, respectively when Going = Forward and |
| -- Going = Backward. |
| |
| and then |
| (for all J in Source'Range => |
| (if J /= Index_Non_Blank'Result |
| and then (J < Index_Non_Blank'Result) |
| = (Going = Forward) |
| and then (J = From or else (J > From) |
| = (Going = Forward)) |
| then Source (J) = ' '))), |
| Global => null; |
| |
| function Count |
| (Source : String; |
| Pattern : String; |
| Mapping : Maps.Character_Mapping := Maps.Identity) return Natural |
| with |
| Pre => Pattern'Length > 0, |
| Global => null; |
| |
| function Count |
| (Source : String; |
| Pattern : String; |
| Mapping : Maps.Character_Mapping_Function) return Natural |
| with |
| Pre => Pattern'Length > 0 and then Mapping /= null, |
| Global => null; |
| |
| function Count |
| (Source : String; |
| Set : Maps.Character_Set) return Natural |
| with |
| Global => null; |
| |
| procedure Find_Token |
| (Source : String; |
| Set : Maps.Character_Set; |
| From : Positive; |
| Test : Membership; |
| First : out Positive; |
| Last : out Natural) |
| with |
| Pre => (if Source'Length /= 0 then From in Source'Range), |
| Contract_Cases => |
| |
| -- If Source is the empty string, or if no character of the considered |
| -- slice of Source satisfies the property Test on Set, then First is |
| -- set to From and Last is set to 0. |
| |
| (Source'Length = 0 |
| or else |
| (for all C of Source (From .. Source'Last) => |
| (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) |
| => |
| First = From and then Last = 0, |
| |
| -- Otherwise, First and Last are set to valid indexes |
| |
| others => |
| |
| -- First and Last are in the considered range of Source |
| |
| First in From .. Source'Last |
| and then Last in First .. Source'Last |
| |
| -- No character between From and First satisfies the property Test |
| -- on Set. |
| |
| and then |
| (for all C of Source (From .. First - 1) => |
| (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) |
| |
| -- All characters between First and Last satisfy the property Test |
| -- on Set. |
| |
| and then |
| (for all C of Source (First .. Last) => |
| (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set)) |
| |
| -- If Last is not Source'Last, then the character at position |
| -- Last + 1 does not satify the property Test on Set. |
| |
| and then |
| (if Last < Source'Last |
| then (Test = Inside) |
| /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), |
| Global => null; |
| |
| procedure Find_Token |
| (Source : String; |
| Set : Maps.Character_Set; |
| Test : Membership; |
| First : out Positive; |
| Last : out Natural) |
| with |
| Pre => Source'First > 0, |
| Contract_Cases => |
| |
| -- If Source is the empty string, or if no character of Source |
| -- satisfies the property Test on Set, then First is set to From |
| -- and Last is set to 0. |
| |
| (Source'Length = 0 |
| or else |
| (for all C of Source => |
| (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) |
| => |
| First = Source'First and then Last = 0, |
| |
| -- Otherwise, First and Last are set to valid indexes |
| |
| others => |
| |
| -- First and Last are in the considered range of Source |
| |
| First in Source'Range |
| and then Last in First .. Source'Last |
| |
| -- No character before First satisfies the property Test on Set |
| |
| and then |
| (for all C of Source (Source'First .. First - 1) => |
| (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) |
| |
| -- All characters between First and Last satisfy the property Test |
| -- on Set. |
| |
| and then |
| (for all C of Source (First .. Last) => |
| (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set)) |
| |
| -- If Last is not Source'Last, then the character at position |
| -- Last + 1 does not satify the property Test on Set. |
| |
| and then |
| (if Last < Source'Last |
| then (Test = Inside) |
| /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), |
| Global => null; |
| |
| end Ada.Strings.Search; |
