-- bounds of function return results were also fixed, and use of & removed for
-- efficiency reasons.
+-- Ghost code, loop invariants and assertions in this unit are meant for
+-- analysis only, not for run-time checking, as it would be too costly
+-- otherwise. This is enforced by setting the assertion policy to Ignore.
+
+pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
with Ada.Strings.Maps; use Ada.Strings.Maps;
-with Ada.Strings.Search;
-package body Ada.Strings.Fixed is
+package body Ada.Strings.Fixed with SPARK_Mode is
------------------------
-- Search Subprograms --
Right : Character) return String
is
begin
- return Result : String (1 .. Left) do
+ return Result : String (1 .. Left) with Relaxed_Initialization do
for J in Result'Range loop
Result (J) := Right;
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ Result (K)'Initialized and then Result (K) = Right);
end loop;
end return;
end "*";
(Left : Natural;
Right : String) return String
is
- Ptr : Integer := 1;
+ Ptr : Integer := 0;
+
+ -- Parts of the proof involving manipulations with the modulo operator
+ -- are complicated for the prover and can't be done automatically in
+ -- the global subprogram. That's why we isolate them in these two ghost
+ -- lemmas.
+
+ procedure Lemma_Mod (K : Integer) with
+ Ghost,
+ Pre =>
+ Right'Length /= 0
+ and then Ptr mod Right'Length = 0
+ and then Ptr in 0 .. Natural'Last - Right'Length
+ and then K in Ptr .. Ptr + Right'Length - 1,
+ Post => K mod Right'Length = K - Ptr;
+ -- Lemma_Mod is applied to an index considered in Lemma_Split to prove
+ -- that it has the right value modulo Right'Length.
+
+ procedure Lemma_Split (Result : String) with
+ Ghost,
+ Relaxed_Initialization => Result,
+ Pre =>
+ Right'Length /= 0
+ and then Result'First = 1
+ and then Result'Last >= 0
+ and then Ptr mod Right'Length = 0
+ and then Ptr in 0 .. Result'Last - Right'Length
+ and then Result (Result'First .. Ptr + Right'Length)'Initialized
+ and then Result (Ptr + 1 .. Ptr + Right'Length) = Right,
+ Post =>
+ (for all K in Ptr + 1 .. Ptr + Right'Length =>
+ Result (K) = Right (Right'First + (K - 1) mod Right'Length));
+ -- Lemma_Split is used after Result (Ptr + 1 .. Ptr + Right'Length) is
+ -- updated to Right and concludes that the characters match for each
+ -- index when taken modulo Right'Length, as the considered slice starts
+ -- at index 1 modulo Right'Length.
+
+ ---------------
+ -- Lemma_Mod --
+ ---------------
+
+ procedure Lemma_Mod (K : Integer) is null;
+
+ -----------------
+ -- Lemma_Split --
+ -----------------
+
+ procedure Lemma_Split (Result : String) is
+ begin
+ for K in Ptr + 1 .. Ptr + Right'Length loop
+ Lemma_Mod (K - 1);
+ pragma Loop_Invariant
+ (for all J in Ptr + 1 .. K =>
+ Result (J) = Right (Right'First + (J - 1) mod Right'Length));
+ end loop;
+ end Lemma_Split;
+
+ -- Start of processing for "*"
+
begin
- return Result : String (1 .. Left * Right'Length) do
+ if Right'Length = 0 then
+ return "";
+ end if;
+
+ return Result : String (1 .. Left * Right'Length)
+ with Relaxed_Initialization
+ do
for J in 1 .. Left loop
- Result (Ptr .. Ptr + Right'Length - 1) := Right;
+ Result (Ptr + 1 .. Ptr + Right'Length) := Right;
+ Lemma_Split (Result);
Ptr := Ptr + Right'Length;
+ pragma Loop_Invariant (Ptr = J * Right'Length);
+ pragma Loop_Invariant (Result (1 .. Ptr)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. Ptr =>
+ Result (K) = Right (Right'First + (K - 1) mod Right'Length));
end loop;
end return;
end "*";
From : Positive;
Through : Natural) return String
is
- Front : Integer;
begin
if From > Through then
declare
end if;
else
- Front := From - Source'First;
- return Result : String (1 .. Source'Length - (Through - From + 1)) do
- Result (1 .. Front) :=
- Source (Source'First .. From - 1);
- Result (Front + 1 .. Result'Last) :=
- Source (Through + 1 .. Source'Last);
- end return;
+ declare
+ Front : constant Integer := From - Source'First;
+
+ begin
+ return Result : String (1 .. Source'Length - (Through - From + 1))
+ with Relaxed_Initialization
+ do
+ Result (1 .. Front) :=
+ Source (Source'First .. From - 1);
+
+ if Through < Source'Last then
+ Result (Front + 1 .. Result'Last) :=
+ Source (Through + 1 .. Source'Last);
+ end if;
+ end return;
+ end;
end if;
end Delete;
From : Positive;
Through : Natural;
Justify : Alignment := Left;
- Pad : Character := Space)
- is
+ Pad : Character := Space) with SPARK_Mode => Off is
begin
Move (Source => Delete (Source, From, Through),
Target => Source,
subtype Result_Type is String (1 .. Count);
begin
- if Count < Source'Length then
+ if Count <= Source'Length then
return
- Result_Type (Source (Source'First .. Source'First + Count - 1));
+ Result_Type (Source (Source'First .. Source'First + (Count - 1)));
else
- return Result : Result_Type do
+ return Result : Result_Type with Relaxed_Initialization do
Result (1 .. Source'Length) := Source;
for J in Source'Length + 1 .. Count loop
Result (J) := Pad;
+ pragma Loop_Invariant
+ (for all K in Source'Length + 1 .. J =>
+ Result (K)'Initialized and then Result (K) = Pad);
end loop;
end return;
end if;
Front : constant Integer := Before - Source'First;
begin
- if Before not in Source'First .. Source'Last + 1 then
+ if Before - 1 not in Source'First - 1 .. Source'Last then
raise Index_Error;
end if;
- return Result : String (1 .. Source'Length + New_Item'Length) do
+ return Result : String (1 .. Source'Length + New_Item'Length)
+ with Relaxed_Initialization
+ do
Result (1 .. Front) :=
Source (Source'First .. Before - 1);
Result (Front + 1 .. Front + New_Item'Length) :=
New_Item;
- Result (Front + New_Item'Length + 1 .. Result'Last) :=
- Source (Before .. Source'Last);
+ pragma Assert
+ (Result
+ (Before - Source'First + 1
+ .. Before - Source'First + New_Item'Length)
+ = New_Item);
+
+ if Before <= Source'Last then
+ Result (Front + New_Item'Length + 1 .. Result'Last) :=
+ Source (Before .. Source'Last);
+ end if;
+
+ pragma Assert
+ (Result (1 .. Before - Source'First)
+ = Source (Source'First .. Before - 1));
end return;
end Insert;
(Source : in out String;
Before : Positive;
New_Item : String;
- Drop : Truncation := Error)
- is
+ Drop : Truncation := Error) with SPARK_Mode => Off is
begin
Move (Source => Insert (Source, Before, New_Item),
Target => Source,
Target : out String;
Drop : Truncation := Error;
Justify : Alignment := Left;
- Pad : Character := Space)
+ Pad : Character := Space) with SPARK_Mode => Off
is
Sfirst : constant Integer := Source'First;
Slast : constant Integer := Source'Last;
Position : Positive;
New_Item : String) return String is
begin
- if Position not in Source'First .. Source'Last + 1 then
+ if Position - 1 not in Source'First - 1 .. Source'Last then
raise Index_Error;
end if;
Front : constant Integer := Position - Source'First;
begin
- return Result : String (1 .. Result_Length) do
+ return Result : String (1 .. Result_Length)
+ with Relaxed_Initialization
+ do
Result (1 .. Front) := Source (Source'First .. Position - 1);
+ pragma Assert
+ (Result (1 .. Position - Source'First)
+ = Source (Source'First .. Position - 1));
Result (Front + 1 .. Front + New_Item'Length) := New_Item;
- Result (Front + New_Item'Length + 1 .. Result'Length) :=
- Source (Position + New_Item'Length .. Source'Last);
+ pragma Assert
+ (Result
+ (Position - Source'First + 1
+ .. Position - Source'First + New_Item'Length)
+ = New_Item);
+
+ if Position <= Source'Last - New_Item'Length then
+ Result (Front + New_Item'Length + 1 .. Result'Last) :=
+ Source (Position + New_Item'Length .. Source'Last);
+ end if;
+
+ pragma Assert
+ (if Position <= Source'Last - New_Item'Length
+ then
+ Result
+ (Position - Source'First + New_Item'Length + 1
+ .. Result'Last)
+ = Source (Position + New_Item'Length .. Source'Last));
end return;
end;
end Overwrite;
(Source : in out String;
Position : Positive;
New_Item : String;
- Drop : Truncation := Right)
- is
+ Drop : Truncation := Right) with SPARK_Mode => Off is
begin
Move (Source => Overwrite (Source, Position, New_Item),
Target => Source,
(Source : String;
Low : Positive;
High : Natural;
- By : String) return String
- is
+ By : String) return String is
begin
- if Low > Source'Last + 1 or else High < Source'First - 1 then
+ if Low - 1 > Source'Last or else High < Source'First - 1 then
raise Index_Error;
end if;
-- Length of result
begin
- return Result : String (1 .. Result_Length) do
+ return Result : String (1 .. Result_Length)
+ with Relaxed_Initialization do
Result (1 .. Front_Len) := Source (Source'First .. Low - 1);
+ pragma Assert
+ (Result (1 .. Integer'Max (0, Low - Source'First))
+ = Source (Source'First .. Low - 1));
Result (Front_Len + 1 .. Front_Len + By'Length) := By;
- Result (Front_Len + By'Length + 1 .. Result'Length) :=
- Source (High + 1 .. Source'Last);
+
+ if High < Source'Last then
+ Result (Front_Len + By'Length + 1 .. Result'Last) :=
+ Source (High + 1 .. Source'Last);
+ end if;
+
+ pragma Assert
+ (Result (1 .. Integer'Max (0, Low - Source'First))
+ = Source (Source'First .. Low - 1));
+ pragma Assert
+ (Result
+ (Integer'Max (0, Low - Source'First) + 1
+ .. Integer'Max (0, Low - Source'First) + By'Length)
+ = By);
+ pragma Assert
+ (if High < Source'Last
+ then
+ Result
+ (Integer'Max (0, Low - Source'First) + By'Length + 1
+ .. Result'Last)
+ = Source (High + 1 .. Source'Last));
end return;
end;
else
By : String;
Drop : Truncation := Error;
Justify : Alignment := Left;
- Pad : Character := Space)
- is
+ Pad : Character := Space) with SPARK_Mode => Off is
begin
Move (Replace_Slice (Source, Low, High, By), Source, Drop, Justify, Pad);
end Replace_Slice;
subtype Result_Type is String (1 .. Count);
begin
- if Count < Source'Length then
+ if Count = 0 then
+ return "";
+
+ elsif Count < Source'Length then
return Result_Type (Source (Source'Last - Count + 1 .. Source'Last));
-- Pad on left
else
- return Result : Result_Type do
+ return Result : Result_Type with Relaxed_Initialization do
for J in 1 .. Count - Source'Length loop
Result (J) := Pad;
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ Result (K)'Initialized and then Result (K) = Pad);
end loop;
- Result (Count - Source'Length + 1 .. Count) := Source;
+ if Source'Length /= 0 then
+ Result (Count - Source'Length + 1 .. Count) := Source;
+ end if;
end return;
end if;
end Tail;
Mapping : Maps.Character_Mapping) return String
is
begin
- return Result : String (1 .. Source'Length) do
+ return Result : String (1 .. Source'Length)
+ with Relaxed_Initialization
+ do
for J in Source'Range loop
Result (J - (Source'First - 1)) := Value (Mapping, Source (J));
+ pragma Loop_Invariant
+ (for all K in Source'First .. J =>
+ Result (K - (Source'First - 1))'Initialized);
+ pragma Loop_Invariant
+ (for all K in Source'First .. J =>
+ Result (K - (Source'First - 1)) =
+ Value (Mapping, Source (K)));
end loop;
end return;
end Translate;
begin
for J in Source'Range loop
Source (J) := Value (Mapping, Source (J));
+ pragma Loop_Invariant
+ (for all K in Source'First .. J =>
+ Source (K) = Value (Mapping, Source'Loop_Entry (K)));
end loop;
end Translate;
is
pragma Unsuppress (Access_Check);
begin
- return Result : String (1 .. Source'Length) do
+ return Result : String (1 .. Source'Length)
+ with Relaxed_Initialization
+ do
for J in Source'Range loop
Result (J - (Source'First - 1)) := Mapping.all (Source (J));
+ pragma Loop_Invariant
+ (for all K in Source'First .. J =>
+ Result (K - (Source'First - 1))'Initialized);
+ pragma Loop_Invariant
+ (for all K in Source'First .. J =>
+ Result (K - (Source'First - 1)) = Mapping (Source (K)));
end loop;
end return;
end Translate;
begin
for J in Source'Range loop
Source (J) := Mapping.all (Source (J));
+ pragma Loop_Invariant
+ (for all K in Source'First .. J =>
+ Source (K) = Mapping (Source'Loop_Entry (K)));
end loop;
end Translate;
(Source : String;
Side : Trim_End) return String
is
+ Empty_String : constant String (1 .. 0) := "";
+ -- Without declaring the empty string as a separate string starting
+ -- at 1, SPARK provers have trouble proving the postcondition.
begin
case Side is
when Strings.Left =>
-- All blanks case
if Low = 0 then
- return "";
+ return Empty_String;
end if;
declare
-- All blanks case
if High = 0 then
- return "";
+ return Empty_String;
end if;
declare
-- All blanks case
if Low = 0 then
- return "";
+ return Empty_String;
end if;
declare
return "";
end if;
- High :=
- Index (Source, Set => Right, Test => Outside, Going => Backward);
+ High := Index (Source, Set => Right, Test => Outside, Going => Backward);
-- Case where source comprises only characters in Right
end if;
declare
- subtype Result_Type is String (1 .. High - Low + 1);
+ Result_Length : constant Integer := High - Low + 1;
+ subtype Result_Type is String (1 .. Result_Length);
begin
return Result_Type (Source (Low .. High));
-- --
------------------------------------------------------------------------------
--- 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.
-
-pragma Assertion_Policy (Pre => Ignore);
-
-with Ada.Strings.Maps;
-
-- The language-defined package Strings.Fixed provides string-handling
-- subprograms for fixed-length strings; that is, for values of type
-- Standard.String. Several of these subprograms are procedures that modify
-- these effects. Similar control is provided by the string transformation
-- procedures.
+-- 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 and
+-- contract cases 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;
+with Ada.Strings.Search;
+
package Ada.Strings.Fixed with SPARK_Mode is
pragma Preelaborate;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre =>
- Pattern'Length /= 0
- and then (if Source'Length /= 0 then From in Source'Range),
+ 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 no slice in the considered range of Source matches Pattern,
- -- then 0 is returned.
+ -- If Source is the empty string, then 0 is returned
- ((for all J in Source'Range =>
- (if (if Going = Forward
- then J in From .. Source'Last - Pattern'Length + 1
- else J <= From - Pattern'Length + 1)
- then Translate (Source (J .. J - 1 + Pattern'Length), Mapping)
- /= Pattern))
+ (Source'Length = 0
=>
Index'Result = 0,
- -- Otherwise, a valid index is returned
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
- others
+ 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) =>
+ Ada.Strings.Search.Match (Source, Pattern, Mapping, J))
=>
-
-- The result is in the considered range of Source
- (if Going = Forward
- then Index'Result in From .. Source'Last - Pattern'Length + 1
- else Index'Result in Source'First .. From - Pattern'Length + 1)
+ 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
- Translate (Source (Index'Result
- .. Index'Result - 1 + Pattern'Length),
- Mapping)
- = Pattern
+ Ada.Strings.Search.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.
+ -- 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 Translate (Source (J .. J - 1 + Pattern'Length),
- Mapping)
- /= Pattern))),
+ else J - 1 in Index'Result
+ .. From - Pattern'Length)
+ then not (Ada.Strings.Search.Match
+ (Source, Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
Global => null;
pragma Ada_05 (Index);
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),
+ 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 no slice in the considered range of Source matches Pattern,
- -- then 0 is returned.
+ -- If Source is the empty string, then 0 is returned
- ((for all J in Source'Range =>
- (if (if Going = Forward
- then J in From .. Source'Last - Pattern'Length + 1
- else J <= From - Pattern'Length + 1)
- then Translate (Source (J .. J - 1 + Pattern'Length), Mapping)
- /= Pattern))
+ (Source'Length = 0
=>
Index'Result = 0,
- -- Otherwise, a valid index is returned
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
- others
+ 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) =>
+ Ada.Strings.Search.Match (Source, Pattern, Mapping, J))
=>
-
-- The result is in the considered range of Source
- (if Going = Forward
- then Index'Result in From .. Source'Last - Pattern'Length + 1
- else Index'Result in Source'First .. From - Pattern'Length + 1)
+ 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
+ -- The slice beginning at the returned index matches Pattern
- and then
- Translate (Source (Index'Result
- .. Index'Result - 1 + Pattern'Length),
- Mapping)
- = Pattern
+ and then
+ Ada.Strings.Search.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.
+ -- 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 Translate (Source (J .. J - 1 + Pattern'Length),
- Mapping)
- /= Pattern))),
+ else J - 1 in Index'Result
+ .. From - Pattern'Length)
+ then not (Ada.Strings.Search.Match
+ (Source, Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
Global => null;
pragma Ada_05 (Index);
Post => Index'Result in 0 | Source'Range,
Contract_Cases =>
- -- If Source is empty, or if no slice of Source matches Pattern, then
- -- 0 is returned.
+ -- If Source is the empty string, then 0 is returned
(Source'Length = 0
- or else
- (for all J in Source'First .. Source'Last - Pattern'Length + 1 =>
- Translate (Source (J .. J - 1 + Pattern'Length), Mapping)
- /= Pattern)
=>
Index'Result = 0,
- -- Otherwise, a valid index is returned
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
- others
+ Source'Length > 0
+ and then
+ (for some J in
+ Source'First .. Source'Last - (Pattern'Length - 1) =>
+ Ada.Strings.Search.Match (Source, Pattern, Mapping, J))
=>
-
-- The result is in the considered range of Source
- Index'Result in Source'First .. Source'Last - Pattern'Length + 1
+ Index'Result in Source'First .. Source'Last - (Pattern'Length - 1)
-- The slice beginning at the returned index matches Pattern
and then
- Translate (Source (Index'Result
- .. Index'Result - 1 + Pattern'Length),
- Mapping)
- = Pattern
+ Ada.Strings.Search.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.
+ -- 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 =>
then J <= Index'Result - 1
else J - 1 in Index'Result
.. Source'Last - Pattern'Length)
- then Translate (Source (J .. J - 1 + Pattern'Length),
- Mapping)
- /= Pattern))),
+ then not (Ada.Strings.Search.Match
+ (Source, Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
Global => null;
function Index
Going : Direction := Forward;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre => Pattern'Length > 0,
+ Pre => Pattern'Length > 0 and then Mapping /= null,
Post => Index'Result in 0 | Source'Range,
Contract_Cases =>
- -- If Source is empty, or if no slice of Source matches Pattern, then
- -- 0 is returned.
+ -- If Source is the empty string, then 0 is returned
(Source'Length = 0
- or else
- (for all J in Source'First .. Source'Last - Pattern'Length + 1 =>
- Translate (Source (J .. J - 1 + Pattern'Length), Mapping)
- /= Pattern)
=>
Index'Result = 0,
- -- Otherwise, a valid index is returned
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
- others
+ Source'Length > 0
+ and then
+ (for some J in
+ Source'First .. Source'Last - (Pattern'Length - 1) =>
+ Ada.Strings.Search.Match (Source, Pattern, Mapping, J))
=>
-
-- The result is in the considered range of Source
- Index'Result in Source'First .. Source'Last - Pattern'Length + 1
+ Index'Result in Source'First .. Source'Last - (Pattern'Length - 1)
- -- The slice beginning at the returned index matches Pattern
+ -- The slice beginning at the returned index matches Pattern
- and then
- Translate (Source (Index'Result
- .. Index'Result - 1 + Pattern'Length),
- Mapping)
- = Pattern
+ and then
+ Ada.Strings.Search.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.
+ -- 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 =>
then J <= Index'Result - 1
else J - 1 in Index'Result
.. Source'Last - Pattern'Length)
- then Translate (Source (J .. J - 1 + Pattern'Length),
- Mapping)
- /= Pattern))),
+ then not (Ada.Strings.Search.Match
+ (Source, Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
Global => null;
-- If Going = Forward, returns:
(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 = Backwards.
+ -- 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 =>
Test : Membership := Inside;
Going : Direction := Forward) return Natural
with
- Pre => (if Source'Length /= 0 then From in Source'Range),
-
+ Pre => (if Source'Length > 0 then From in Source'Range),
Post => Index'Result in 0 | Source'Range,
Contract_Cases =>
- -- If no character in the considered slice of Source satisfies the
- -- property Test on Set, then 0 is returned.
+ -- 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.
- ((for all I in Source'Range =>
- (if I = From
- or else (I > From) = (Going = Forward)
- then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (I), Set)))
+ (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 range of Source is returned
+ -- Otherwise, a index in the considered range of Source is returned
others
=>
Index'Result in Source'Range
and then (Index'Result = From
- or else (Index'Result > From) = (Going = Forward))
+ or else
+ (Index'Result > From) = (Going = Forward))
-- The character at the returned index satisfies the property
-- Test on Set.
(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 = Backwards.
+ -- 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)))),
+ 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;
pragma Ada_05 (Index);
-- Index searches for the first or last occurrence of any of a set of
Post => Index_Non_Blank'Result in 0 | Source'Range,
Contract_Cases =>
- -- If all characters in the considered slice of Source are Space
- -- characters, then 0 is returned.
+ -- If Source is the empty string, or all characters in the considered
+ -- slice of Source are Space characters, then 0 is returned.
- ((for all J in Source'Range =>
- (if J = From or else (J > From) = (Going = Forward)
- then Source (J) = ' '))
+ (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,
-- The result is the smallest or largest index which is not a
-- Space character, respectively when Going = Forward and
- -- Going = Backwards.
+ -- Going = Backward.
and then
(for all J in Source'Range =>
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 = Backwards.
+ -- Space character, respectively when Going = Forward and Going
+ -- = Backward.
and then
(for all J in Source'Range =>
Pattern : String;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre => Pattern'Length /= 0,
+ Pre => Pattern'Length /= 0 and then Mapping /= null,
Global => null;
-- Returns the maximum number of nonoverlapping slices of Source that match
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
(Source : String;
Mapping : Maps.Character_Mapping_Function) return String
with
+ Pre => Mapping /= null,
Post =>
-- Lower bound of the returned string is 1
(Source : in out String;
Mapping : Maps.Character_Mapping_Function)
with
+ Pre => Mapping /= null,
Post =>
- -- Each character in Source after the call is the translation of
- -- the character at the same position before the call, through Mapping.
+ -- Each character in Source after the call is the translation of the
+ -- character at the same position before the call, through Mapping.
(for all J in Source'Range => Source (J) = Mapping (Source'Old (J))),
Global => null;
with
Post =>
- -- Each character in Source after the call is the translation of
- -- the character at the same position before the call, through Mapping.
+ -- Each character in Source after the call is the translation of the
+ -- character at the same position before the call, through Mapping.
(for all J in Source'Range =>
Source (J) = Ada.Strings.Maps.Value (Mapping, Source'Old (J))),
-- String Transformation Subprograms --
---------------------------------------
- procedure Replace_Slice
- (Source : in out String;
- Low : Positive;
- High : Natural;
- By : String;
- Drop : Truncation := Error;
- Justify : Alignment := Left;
- Pad : Character := Space)
- with
- Pre =>
-
- -- Incomplete contract
-
- Low - 1 <= Source'Last
- and then High >= Source'First - 1,
- Global => null;
- -- If Low > Source'Last+1, or High < Source'First - 1, then Index_Error is
- -- propagated. Otherwise:
- --
- -- * If High >= Low, then the returned string comprises
- -- Source (Source'First .. Low - 1)
- -- & By & Source(High + 1 .. Source'Last), but with lower bound 1.
- --
- -- * If High < Low, then the returned string is
- -- Insert (Source, Before => Low, New_Item => By).
-
function Replace_Slice
(Source : String;
Low : Positive;
-- Length of the returned string
Replace_Slice'Result'Length
- = Natural'Max (0, Low - Source'First)
+ = Integer'Max (0, Low - Source'First)
+ By'Length
- + Natural'Max (Source'Last - High, 0)
+ + Integer'Max (Source'Last - High, 0)
-- Elements starting at Low are replaced by elements of By
and then
- Replace_Slice'Result (1 .. Natural'Max (0, Low - Source'First))
+ Replace_Slice'Result (1 .. Integer'Max (0, Low - Source'First))
= Source (Source'First .. Low - 1)
and then
Replace_Slice'Result
- (Natural'Max (0, Low - Source'First) + 1
- .. Natural'Max (0, Low - Source'First) + By'Length)
+ (Integer'Max (0, Low - Source'First) + 1
+ .. Integer'Max (0, Low - Source'First) + By'Length)
= By
-- When there are remaining characters after the replaced slice,
(if High < Source'Last
then
Replace_Slice'Result
- (Natural'Max (0, Low - Source'First) + By'Length + 1
+ (Integer'Max (0, Low - Source'First) + By'Length + 1
.. Replace_Slice'Result'Last)
= Source (High + 1 .. Source'Last)),
.. Replace_Slice'Result'Last)
= Source (Low .. Source'Last))),
Global => null;
+ -- If Low > Source'Last + 1, or High < Source'First - 1, then Index_Error
+ -- is propagated. Otherwise:
+ --
+ -- * If High >= Low, then the returned string comprises
+ -- Source (Source'First .. Low - 1)
+ -- & By & Source(High + 1 .. Source'Last), but with lower bound 1.
+ --
+ -- * If High < Low, then the returned string is
+ -- Insert (Source, Before => Low, New_Item => By).
+
+ procedure Replace_Slice
+ (Source : in out String;
+ Low : Positive;
+ High : Natural;
+ By : String;
+ Drop : Truncation := Error;
+ Justify : Alignment := Left;
+ Pad : Character := Space)
+ with
+ Pre => Low - 1 <= Source'Last,
+
+ -- Incomplete contract
+
+ Global => null;
-- Equivalent to:
--
-- Move (Replace_Slice (Source, Low, High, By),
-- are appended to the returned string.
and then
- (if Before - 1 < Source'Last
+ (if Before <= Source'Last
then
Insert'Result
(Before - Source'First + New_Item'Length + 1
= Source (Before .. Source'Last)),
Global => null;
-- Propagates Index_Error if Before is not in
- -- Source'First .. Source'Last+1; otherwise, returns
+ -- Source'First .. Source'Last + 1; otherwise, returns
-- Source (Source'First .. Before - 1)
-- & New_Item & Source(Before..Source'Last), but with lower bound 1.
-- Content of the string is Right concatenated with itself Left times
and then
- (for all J in 0 .. Left - 1 =>
- "*"'Result (J * Right'Length + 1 .. (J + 1) * Right'Length)
- = Right),
+ (for all K in "*"'Result'Range =>
+ "*"'Result (K) = Right (Right'First + (K - 1) mod Right'Length)),
Global => null;
-- These functions replicate a character or string a specified number of
-- case of identity mappings for Count and Index, and also Index_Non_Blank
-- is specialized (rather than using the general Index routine).
+-- Ghost code, loop invariants and assertions in this unit are meant for
+-- analysis only, not for run-time checking, as it would be too costly
+-- otherwise. This is enforced by setting the assertion policy to Ignore.
+
+pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
with Ada.Strings.Maps; use Ada.Strings.Maps;
with System; use System;
-package body Ada.Strings.Search is
+package body Ada.Strings.Search with SPARK_Mode is
-----------------------
-- Local Subprograms --
Set : Maps.Character_Set;
Test : Membership) return Boolean
is
- begin
- if Test = Inside then
- return Is_In (Element, Set);
- else
- return not Is_In (Element, Set);
- end if;
- end Belongs;
+ (if Test = Inside then
+ Is_In (Element, Set)
+ else not (Is_In (Element, Set)));
-----------
-- Count --
PL1 : constant Integer := Pattern'Length - 1;
Num : Natural;
Ind : Natural;
- Cur : Natural;
begin
if Pattern = "" then
raise Pattern_Error;
end if;
+ -- Isolating the null string case to ensure Source'First, Source'Last in
+ -- Positive.
+
+ if Source = "" then
+ return 0;
+ end if;
+
Num := 0;
- Ind := Source'First;
+ Ind := Source'First - 1;
-- Unmapped case
- if Mapping'Address = Maps.Identity'Address then
- while Ind <= Source'Last - PL1 loop
+ if Is_Identity (Mapping) then
+ while Ind < Source'Last - PL1 loop
+ Ind := Ind + 1;
if Pattern = Source (Ind .. Ind + PL1) then
Num := Num + 1;
- Ind := Ind + Pattern'Length;
- else
- Ind := Ind + 1;
+ Ind := Ind + PL1;
end if;
+
+ pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
+ pragma Loop_Invariant (Ind >= Source'First);
end loop;
-- Mapped case
else
- while Ind <= Source'Last - PL1 loop
- Cur := Ind;
+ while Ind < Source'Last - PL1 loop
+ Ind := Ind + 1;
for K in Pattern'Range loop
- if Pattern (K) /= Value (Mapping, Source (Cur)) then
- Ind := Ind + 1;
+ if Pattern (K) /= Value (Mapping,
+ Source (Ind + (K - Pattern'First)))
+ then
+ pragma Assert (not (Match (Source, Pattern, Mapping, Ind)));
goto Cont;
- else
- Cur := Cur + 1;
end if;
+
+ pragma Loop_Invariant
+ (for all J in Pattern'First .. K =>
+ Pattern (J) = Value (Mapping,
+ Source (Ind + (J - Pattern'First))));
end loop;
+ pragma Assert (Match (Source, Pattern, Mapping, Ind));
Num := Num + 1;
- Ind := Ind + Pattern'Length;
+ Ind := Ind + PL1;
- <<Cont>>
+ <<Cont>>
null;
+ pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
+ pragma Loop_Invariant (Ind >= Source'First);
end loop;
end if;
PL1 : constant Integer := Pattern'Length - 1;
Num : Natural;
Ind : Natural;
- Cur : Natural;
begin
if Pattern = "" then
raise Pattern_Error;
end if;
+ -- Isolating the null string case to ensure Source'First, Source'Last in
+ -- Positive.
+
+ if Source = "" then
+ return 0;
+ end if;
+
-- Check for null pointer in case checks are off
if Mapping = null then
end if;
Num := 0;
- Ind := Source'First;
- while Ind <= Source'Last - PL1 loop
- Cur := Ind;
+ Ind := Source'First - 1;
+ while Ind < Source'Last - PL1 loop
+ Ind := Ind + 1;
for K in Pattern'Range loop
- if Pattern (K) /= Mapping (Source (Cur)) then
- Ind := Ind + 1;
+ if Pattern (K) /= Mapping (Source (Ind + (K - Pattern'First))) then
+ pragma Assert (not (Match (Source, Pattern, Mapping, Ind)));
goto Cont;
- else
- Cur := Cur + 1;
end if;
+
+ pragma Loop_Invariant
+ (for all J in Pattern'First .. K =>
+ Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
end loop;
+ pragma Assert (Match (Source, Pattern, Mapping, Ind));
Num := Num + 1;
- Ind := Ind + Pattern'Length;
+ Ind := Ind + PL1;
<<Cont>>
null;
+ pragma Loop_Invariant (Num <= Ind - (Source'First - 1));
+ pragma Loop_Invariant (Ind >= Source'First);
end loop;
return Num;
begin
for J in Source'Range loop
+ pragma Loop_Invariant (N <= J - Source'First);
if Is_In (Source (J), Set) then
N := N + 1;
end if;
if Belongs (Source (J), Set, Test) then
First := J;
- for K in J + 1 .. Source'Last loop
- if not Belongs (Source (K), Set, Test) then
- Last := K - 1;
- return;
- end if;
- end loop;
+ if J < Source'Last then
+ for K in J + 1 .. Source'Last loop
+ if not Belongs (Source (K), Set, Test) then
+ Last := K - 1;
+ return;
+ end if;
+
+ pragma Loop_Invariant
+ (for all L in J .. K =>
+ Belongs (Source (L), Set, Test));
+ end loop;
+ end if;
-- Here if J indexes first char of token, and all chars after J
-- are in the token.
Last := Source'Last;
return;
end if;
+
+ pragma Loop_Invariant
+ (for all K in Integer'Max (From, Source'First) .. J =>
+ not (Belongs (Source (K), Set, Test)));
end loop;
-- Here if no token found
if Belongs (Source (J), Set, Test) then
First := J;
- for K in J + 1 .. Source'Last loop
- if not Belongs (Source (K), Set, Test) then
- Last := K - 1;
- return;
- end if;
- end loop;
+ if J < Source'Last then
+ for K in J + 1 .. Source'Last loop
+ if not Belongs (Source (K), Set, Test) then
+ Last := K - 1;
+ return;
+ end if;
+
+ pragma Loop_Invariant
+ (for all L in J .. K =>
+ Belongs (Source (L), Set, Test));
+ end loop;
+ end if;
-- Here if J indexes first char of token, and all chars after J
-- are in the token.
Last := Source'Last;
return;
end if;
+
+ pragma Loop_Invariant
+ (for all K in Source'First .. J =>
+ not (Belongs (Source (K), Set, Test)));
end loop;
-- Here if no token found
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
is
PL1 : constant Integer := Pattern'Length - 1;
- Cur : Natural;
-
- Ind : Integer;
- -- Index for start of match check. This can be negative if the pattern
- -- length is greater than the string length, which is why this variable
- -- is Integer instead of Natural. In this case, the search loops do not
- -- execute at all, so this Ind value is never used.
begin
if Pattern = "" then
raise Pattern_Error;
end if;
+ -- If Pattern is longer than Source, it can't be found
+
+ if Pattern'Length > Source'Length then
+ return 0;
+ end if;
+
-- Forwards case
if Going = Forward then
- Ind := Source'First;
-- Unmapped forward case
- if Mapping'Address = Maps.Identity'Address then
- for J in 1 .. Source'Length - PL1 loop
+ if Is_Identity (Mapping) then
+ for Ind in Source'First .. Source'Last - PL1 loop
if Pattern = Source (Ind .. Ind + PL1) then
+ pragma Assert (Match (Source, Pattern, Mapping, Ind));
return Ind;
- else
- Ind := Ind + 1;
end if;
+
+ pragma Loop_Invariant
+ (for all J in Source'First .. Ind =>
+ not (Match (Source, Pattern, Mapping, J)));
end loop;
-- Mapped forward case
else
- for J in 1 .. Source'Length - PL1 loop
- Cur := Ind;
-
+ for Ind in Source'First .. Source'Last - PL1 loop
for K in Pattern'Range loop
- if Pattern (K) /= Value (Mapping, Source (Cur)) then
+ if Pattern (K) /= Value (Mapping,
+ Source (Ind + (K - Pattern'First)))
+ then
goto Cont1;
- else
- Cur := Cur + 1;
end if;
+
+ pragma Loop_Invariant
+ (for all J in Pattern'First .. K =>
+ Pattern (J) = Value (Mapping,
+ Source (Ind + (J - Pattern'First))));
end loop;
+ pragma Assert (Match (Source, Pattern, Mapping, Ind));
return Ind;
- <<Cont1>>
- Ind := Ind + 1;
+ <<Cont1>>
+ pragma Loop_Invariant
+ (for all J in Source'First .. Ind =>
+ not (Match (Source, Pattern, Mapping, J)));
+ null;
end loop;
end if;
else
-- Unmapped backward case
- Ind := Source'Last - PL1;
-
- if Mapping'Address = Maps.Identity'Address then
- for J in reverse 1 .. Source'Length - PL1 loop
+ if Is_Identity (Mapping) then
+ for Ind in reverse Source'First .. Source'Last - PL1 loop
if Pattern = Source (Ind .. Ind + PL1) then
+ pragma Assert (Match (Source, Pattern, Mapping, Ind));
return Ind;
- else
- Ind := Ind - 1;
end if;
+
+ pragma Loop_Invariant
+ (for all J in Ind .. Source'Last - PL1 =>
+ not (Match (Source, Pattern, Mapping, J)));
end loop;
-- Mapped backward case
else
- for J in reverse 1 .. Source'Length - PL1 loop
- Cur := Ind;
-
+ for Ind in reverse Source'First .. Source'Last - PL1 loop
for K in Pattern'Range loop
- if Pattern (K) /= Value (Mapping, Source (Cur)) then
+ if Pattern (K) /= Value (Mapping,
+ Source (Ind + (K - Pattern'First)))
+ then
goto Cont2;
- else
- Cur := Cur + 1;
end if;
+
+ pragma Loop_Invariant
+ (for all J in Pattern'First .. K =>
+ Pattern (J) = Value (Mapping,
+ Source (Ind + (J - Pattern'First))));
end loop;
+ pragma Assert (Match (Source, Pattern, Mapping, Ind));
return Ind;
- <<Cont2>>
- Ind := Ind - 1;
+ <<Cont2>>
+ pragma Loop_Invariant
+ (for all J in Ind .. Source'Last - PL1 =>
+ not (Match (Source, Pattern, Mapping, J)));
+ null;
end loop;
end if;
end if;
Mapping : Maps.Character_Mapping_Function) return Natural
is
PL1 : constant Integer := Pattern'Length - 1;
- Ind : Natural;
- Cur : Natural;
-
begin
if Pattern = "" then
raise Pattern_Error;
-- Forwards case
if Going = Forward then
- Ind := Source'First;
- for J in 1 .. Source'Length - PL1 loop
- Cur := Ind;
-
+ for Ind in Source'First .. Source'Last - PL1 loop
for K in Pattern'Range loop
- if Pattern (K) /= Mapping.all (Source (Cur)) then
+ if Pattern (K) /= Mapping.all
+ (Source (Ind + (K - Pattern'First)))
+ then
goto Cont1;
- else
- Cur := Cur + 1;
end if;
+
+ pragma Loop_Invariant
+ (for all J in Pattern'First .. K =>
+ Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
end loop;
+ pragma Assert (Match (Source, Pattern, Mapping, Ind));
return Ind;
- <<Cont1>>
- Ind := Ind + 1;
+ <<Cont1>>
+ pragma Loop_Invariant
+ (for all J in Source'First .. Ind =>
+ not (Match (Source, Pattern, Mapping, J)));
+ null;
end loop;
-- Backwards case
else
- Ind := Source'Last - PL1;
- for J in reverse 1 .. Source'Length - PL1 loop
- Cur := Ind;
-
+ for Ind in reverse Source'First .. Source'Last - PL1 loop
for K in Pattern'Range loop
- if Pattern (K) /= Mapping.all (Source (Cur)) then
+ if Pattern (K) /= Mapping.all
+ (Source (Ind + (K - Pattern'First)))
+ then
goto Cont2;
- else
- Cur := Cur + 1;
end if;
+
+ pragma Loop_Invariant
+ (for all J in Pattern'First .. K =>
+ Pattern (J) = Mapping (Source (Ind + (J - Pattern'First))));
end loop;
return Ind;
- <<Cont2>>
- Ind := Ind - 1;
+ <<Cont2>>
+ pragma Loop_Invariant
+ (for all J in Ind .. (Source'Last - PL1) =>
+ not (Match (Source, Pattern, Mapping, J)));
+ null;
end loop;
end if;
if Belongs (Source (J), Set, Test) then
return J;
end if;
+
+ pragma Loop_Invariant
+ (for all C of Source (Source'First .. J) =>
+ not (Belongs (C, Set, Test)));
end loop;
-- Backwards case
if Belongs (Source (J), Set, Test) then
return J;
end if;
+
+ pragma Loop_Invariant
+ (for all C of Source (J .. Source'Last) =>
+ not (Belongs (C, Set, Test)));
end loop;
end if;
Going : Direction := Forward;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
is
+ Result : Natural;
+ PL1 : constant Integer := Pattern'Length - 1;
begin
-- AI05-056: If source is empty result is always zero
raise Index_Error;
end if;
- return
+ Result :=
Index (Source (From .. Source'Last), Pattern, Forward, Mapping);
+ pragma Assert
+ (if (for some J in From .. Source'Last - PL1 =>
+ Match (Source, Pattern, Mapping, J))
+ then Result in From .. Source'Last - PL1
+ else Result = 0);
else
if From > Source'Last then
raise Index_Error;
end if;
- return
+ Result :=
Index (Source (Source'First .. From), Pattern, Backward, Mapping);
+ pragma Assert
+ (if (for some J in Source'First .. From - PL1 =>
+ Match (Source, Pattern, Mapping, J))
+ then Result in Source'First .. From - PL1
+ else Result = 0);
end if;
+
+ return Result;
end Index;
function Index
if Source (J) /= ' ' then
return J;
end if;
+
+ pragma Loop_Invariant
+ (for all C of Source (Source'First .. J) => C = ' ');
end loop;
else -- Going = Backward
if Source (J) /= ' ' then
return J;
end if;
+
+ pragma Loop_Invariant
+ (for all C of Source (J .. Source'Last) => C = ' ');
end loop;
end if;
Going : Direction := Forward) return Natural
is
begin
+
+ -- For equivalence with Index, if Source is empty the result is 0
+
+ if Source'Length = 0 then
+ return 0;
+ end if;
+
if Going = Forward then
if From < Source'First then
raise Index_Error;
end if;
end Index_Non_Blank;
+ function Is_Identity
+ (Mapping : Maps.Character_Mapping) return Boolean
+ with SPARK_Mode => Off
+ is
+ begin
+ return Mapping'Address = Maps.Identity'Address;
+ end Is_Identity;
+
end Ada.Strings.Search;
-- 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. We make this a
--- private package, since user programs should access these subprograms via
--- one of the standard string packages.
+-- 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.
-with Ada.Strings.Maps;
+-- 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.
-private package Ada.Strings.Search is
+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;
+ 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;
+ 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;
+ 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, a 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;
+ 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;
+ 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;
+ 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, a 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;
+ 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;
+ 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;
+ 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;
+ 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;
+ Set : Maps.Character_Set) return Natural
+ with
+ Global => null;
procedure Find_Token
(Source : String;
From : Positive;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ 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);
+ 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;
projects / platform / upstream / gcc.git / commitdiff