------------------------------------------------------------------------------
-- --
-- GNAT RUN-TIME COMPONENTS --
-- --
-- A D A . S T R I N G S . F I X E D --
-- --
-- S p e c --
-- --
-- This specification is derived from the Ada Reference Manual for use with --
-- GNAT. In accordance with the copyright of that document, you can freely --
-- copy and modify this specification, provided that if you redistribute a --
-- modified version, any changes that you have made are clearly indicated. --
-- --
------------------------------------------------------------------------------
-- 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
-- the contents of a String that is passed as an out or an in out parameter;
-- each has additional parameters to control the effect when the logical
-- length of the result differs from the parameter's length.
--
-- For each function that returns a String, the lower bound of the returned
-- value is 1.
--
-- The basic model embodied in the package is that a fixed-length string
-- comprises significant characters and possibly padding (with space
-- characters) on either or both ends. When a shorter string is copied to a
-- longer string, padding is inserted, and when a longer string is copied to a
-- shorter one, padding is stripped. The Move procedure in Strings.Fixed,
-- which takes a String as an out parameter, allows the programmer to control
-- 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;
--------------------------------------------------------------
-- Copy Procedure for Strings of Possibly Different Lengths --
--------------------------------------------------------------
procedure Move
(Source : String;
Target : out String;
Drop : Truncation := Error;
Justify : Alignment := Left;
Pad : Character := Space)
with
-- Incomplete contract
Global => null,
Annotate => (GNATprove, Might_Not_Return);
-- The Move procedure copies characters from Source to Target. If Source
-- has the same length as Target, then the effect is to assign Source to
-- Target. If Source is shorter than Target then:
--
-- * If Justify=Left, then Source is copied into the first Source'Length
-- characters of Target.
--
-- * If Justify=Right, then Source is copied into the last Source'Length
-- characters of Target.
--
-- * If Justify=Center, then Source is copied into the middle Source'Length
-- characters of Target. In this case, if the difference in length
-- between Target and Source is odd, then the extra Pad character is on
-- the right.
--
-- * Pad is copied to each Target character not otherwise assigned.
--
-- If Source is longer than Target, then the effect is based on Drop.
--
-- * If Drop=Left, then the rightmost Target'Length characters of Source
-- are copied into Target.
--
-- * If Drop=Right, then the leftmost Target'Length characters of Source
-- are copied into Target.
--
-- * If Drop=Error, then the effect depends on the value of the Justify
-- parameter and also on whether any characters in Source other than Pad
-- would fail to be copied:
--
-- * If Justify=Left, and if each of the rightmost
-- Source'Length-Target'Length characters in Source is Pad, then the
-- leftmost Target'Length characters of Source are copied to Target.
--
-- * If Justify=Right, and if each of the leftmost
-- Source'Length-Target'Length characters in Source is Pad, then the
-- rightmost Target'Length characters of Source are copied to Target.
--
-- * Otherwise, Length_Error is propagated.
------------------------
-- Search Subprograms --
------------------------
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) =>
Ada.Strings.Search.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
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 =
-- 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 (Ada.Strings.Search.Match
(Source, Pattern, Mapping, J)))),
-- Otherwise, 0 is returned
others
=>
Index'Result = 0),
Global => null,
Annotate => (GNATprove, Always_Return);
pragma Ada_05 (Index);
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) =>
Ada.Strings.Search.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
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 = 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 (Ada.Strings.Search.Match
(Source, Pattern, Mapping, J)))),
-- Otherwise, 0 is returned
others
=>
Index'Result = 0),
Global => null,
Annotate => (GNATprove, Always_Return);
pragma Ada_05 (Index);
-- Each Index function searches, starting from From, for a slice of
-- Source, with length Pattern'Length, that matches Pattern with respect to
-- Mapping; the parameter Going indicates the direction of the lookup. If
-- Source is the null string, Index returns 0; otherwise, if From is not in
-- Source'Range, then Index_Error is propagated. If Going = Forward, then
-- Index returns the smallest index I which is greater than or equal to
-- From such that the slice of Source starting at I matches Pattern. If
-- Going = Backward, then Index returns the largest index I such that the
-- slice of Source starting at I matches Pattern and has an upper bound
-- less than or equal to From. If there is no such slice, then 0 is
-- returned. If Pattern is the null string, then Pattern_Error is
-- propagated.
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) =>
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)
-- The slice beginning at the returned index matches 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 =
-- 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 (Ada.Strings.Search.Match
(Source, Pattern, Mapping, J)))),
-- Otherwise, 0 is returned
others
=>
Index'Result = 0),
Global => null,
Annotate => (GNATprove, Always_Return);
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 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) =>
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)
-- The slice beginning at the returned index matches 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 =
-- 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 (Ada.Strings.Search.Match
(Source, Pattern, Mapping, J)))),
-- Otherwise, 0 is returned
others
=>
Index'Result = 0),
Global => null,
Annotate => (GNATprove, Always_Return);
-- If Going = Forward, returns:
--
-- Index (Source, Pattern, Source'First, Forward, Mapping)
--
-- otherwise, returns:
--
-- Index (Source, Pattern, Source'Last, Backward, Mapping).
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,
Annotate => (GNATprove, Always_Return);
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,
Annotate => (GNATprove, Always_Return);
pragma Ada_05 (Index);
-- Index searches for the first or last occurrence of any of a set of
-- characters (when Test=Inside), or any of the complement of a set of
-- characters (when Test=Outside). If Source is the null string, Index
-- returns 0; otherwise, if From is not in Source'Range, then Index_Error
-- is propagated. Otherwise, it returns the smallest index I >= From (if
-- Going=Forward) or the largest index I <= From (if Going=Backward) such
-- that Source(I) satisfies the Test condition with respect to Set; it
-- returns 0 if there is no such Character in Source.
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 empty 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,
Annotate => (GNATprove, Always_Return);
pragma Ada_05 (Index_Non_Blank);
-- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going)
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,
Annotate => (GNATprove, Always_Return);
-- Returns Index (Source, Maps.To_Set(Space), Outside, Going)
function Count
(Source : String;
Pattern : String;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
with
Pre => Pattern'Length /= 0,
Global => null,
Annotate => (GNATprove, Always_Return);
function Count
(Source : String;
Pattern : String;
Mapping : Maps.Character_Mapping_Function) return Natural
with
Pre => Pattern'Length /= 0 and then Mapping /= null,
Global => null,
Annotate => (GNATprove, Always_Return);
-- Returns the maximum number of nonoverlapping slices of Source that match
-- Pattern with respect to Mapping. If Pattern is the null string then
-- Pattern_Error is propagated.
function Count
(Source : String;
Set : Maps.Character_Set) return Natural
with
Global => null,
Annotate => (GNATprove, Always_Return);
-- Returns the number of occurrences in Source of characters that are in
-- Set.
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,
Annotate => (GNATprove, Always_Return);
pragma Ada_2012 (Find_Token);
-- If Source is not the null string and From is not in Source'Range, then
-- Index_Error is raised. Otherwise, First is set to the index of the first
-- character in Source(From .. Source'Last) that satisfies the Test
-- condition. Last is set to the largest index such that all characters in
-- Source(First .. Last) satisfy the Test condition. If no characters in
-- Source(From .. Source'Last) satisfy the Test condition, First is set to
-- From, and Last is set to 0.
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,
Annotate => (GNATprove, Always_Return);
-- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last)
------------------------------------
-- String Translation Subprograms --
------------------------------------
function Translate
(Source : String;
Mapping : Maps.Character_Mapping_Function) return String
with
Pre => Mapping /= null,
Post =>
-- Lower bound of the returned string is 1
Translate'Result'First = 1
-- The returned string has the same length as Source
and then Translate'Result'Last = Source'Length
-- Each character in the returned string is the translation of the
-- character at the same position in Source through Mapping.
and then
(for all J in Source'Range =>
Translate'Result (J - Source'First + 1)
= Mapping (Source (J))),
Global => null,
Annotate => (GNATprove, Always_Return);
function Translate
(Source : String;
Mapping : Maps.Character_Mapping) return String
with
Post =>
-- Lower bound of the returned string is 1
Translate'Result'First = 1
-- The returned string has the same length as Source
and then Translate'Result'Last = Source'Length
-- Each character in the returned string is the translation of the
-- character at the same position in Source through Mapping.
and then
(for all J in Source'Range =>
Translate'Result (J - Source'First + 1)
= Ada.Strings.Maps.Value (Mapping, Source (J))),
Global => null,
Annotate => (GNATprove, Always_Return);
-- Returns the string S whose length is Source'Length and such that S (I)
-- is the character to which Mapping maps the corresponding element of
-- Source, for I in 1 .. Source'Length.
procedure Translate
(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.
(for all J in Source'Range => Source (J) = Mapping (Source'Old (J))),
Global => null,
Annotate => (GNATprove, Always_Return);
procedure Translate
(Source : in out String;
Mapping : Maps.Character_Mapping)
with
Post =>
-- 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))),
Global => null,
Annotate => (GNATprove, Always_Return);
-- Equivalent to Source := Translate(Source, Mapping)
---------------------------------------
-- String Transformation Subprograms --
---------------------------------------
function Replace_Slice
(Source : String;
Low : Positive;
High : Natural;
By : String) return String
with
Pre =>
Low - 1 <= Source'Last
and then High >= Source'First - 1
and then (if High >= Low
then Natural'Max (0, Low - Source'First)
<= Natural'Last
- By'Length
- Natural'Max (Source'Last - High, 0)
else Source'Length <= Natural'Last - By'Length),
-- Lower bound of the returned string is 1
Post => Replace_Slice'Result'First = 1,
Contract_Cases =>
-- If High >= Low, then the returned string comprises
-- Source (Source'First .. Low - 1) & By
-- & Source(High + 1 .. Source'Last).
(High >= Low =>
-- Length of the returned string
Replace_Slice'Result'Length
= Integer'Max (0, Low - Source'First)
+ By'Length
+ Integer'Max (Source'Last - High, 0)
-- Elements starting at Low are replaced by elements of By
and then
Replace_Slice'Result (1 .. Integer'Max (0, Low - Source'First))
= Source (Source'First .. Low - 1)
and then
Replace_Slice'Result
(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,
-- they are appended to the result.
and then
(if High < Source'Last
then
Replace_Slice'Result
(Integer'Max (0, Low - Source'First) + By'Length + 1
.. Replace_Slice'Result'Last)
= Source (High + 1 .. Source'Last)),
-- If High < Low, then the returned string is
-- Insert (Source, Before => Low, New_Item => By).
others =>
-- Length of the returned string
Replace_Slice'Result'Length = Source'Length + By'Length
-- Elements of By are inserted after the element at Low
and then
Replace_Slice'Result (1 .. Low - Source'First)
= Source (Source'First .. Low - 1)
and then
Replace_Slice'Result
(Low - Source'First + 1 .. Low - Source'First + By'Length)
= By
-- When there are remaining characters after Low in Source, they
-- are appended to the result.
and then
(if Low < Source'Last
then
Replace_Slice'Result
(Low - Source'First + By'Length + 1
.. Replace_Slice'Result'Last)
= Source (Low .. Source'Last))),
Global => null,
Annotate => (GNATprove, Always_Return);
-- 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
and then High >= Source'First - 1
and then (if High >= Low
then Natural'Max (0, Low - Source'First)
<= Natural'Last
- By'Length
- Natural'Max (Source'Last - High, 0)
else Source'Length <= Natural'Last - By'Length),
-- Incomplete contract
Global => null,
Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Replace_Slice (Source, Low, High, By),
-- Source, Drop, Justify, Pad).
function Insert
(Source : String;
Before : Positive;
New_Item : String) return String
with
Pre =>
Before - 1 in Source'First - 1 .. Source'Last
and then Source'Length <= Natural'Last - New_Item'Length,
Post =>
-- Lower bound of the returned string is 1
Insert'Result'First = 1
-- Length of the returned string
and then Insert'Result'Length = Source'Length + New_Item'Length
-- Elements of New_Item are inserted after element at Before
and then
Insert'Result (1 .. Before - Source'First)
= Source (Source'First .. Before - 1)
and then
Insert'Result
(Before - Source'First + 1
.. Before - Source'First + New_Item'Length)
= New_Item
-- When there are remaining characters after Before in Source, they
-- are appended to the returned string.
and then
(if Before <= Source'Last
then
Insert'Result
(Before - Source'First + New_Item'Length + 1
.. Insert'Result'Last)
= Source (Before .. Source'Last)),
Global => null,
Annotate => (GNATprove, Always_Return);
-- Propagates Index_Error if Before is not in
-- Source'First .. Source'Last + 1; otherwise, returns
-- Source (Source'First .. Before - 1)
-- & New_Item & Source(Before..Source'Last), but with lower bound 1.
procedure Insert
(Source : in out String;
Before : Positive;
New_Item : String;
Drop : Truncation := Error)
with
Pre =>
Before - 1 in Source'First - 1 .. Source'Last
and then Source'Length <= Natural'Last - New_Item'Length,
-- Incomplete contract
Global => null,
Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to Move (Insert (Source, Before, New_Item), Source, Drop)
function Overwrite
(Source : String;
Position : Positive;
New_Item : String) return String
with
Pre =>
Position - 1 in Source'First - 1 .. Source'Last
and then
(if Position - Source'First >= Source'Length - New_Item'Length
then Position - Source'First <= Natural'Last - New_Item'Length),
Post =>
-- Lower bound of the returned string is 1
Overwrite'Result'First = 1
-- Length of the returned string
and then
Overwrite'Result'Length
= Integer'Max (Source'Length,
Position - Source'First + New_Item'Length)
-- Elements after Position are replaced by elements of New_Item
and then
Overwrite'Result (1 .. Position - Source'First)
= Source (Source'First .. Position - 1)
and then
Overwrite'Result
(Position - Source'First + 1
.. Position - Source'First + New_Item'Length)
= New_Item
-- If the end of Source is reached before the characters in New_Item
-- are exhausted, the remaining characters from New_Item are appended
-- to the string.
and then
(if Position <= Source'Last - New_Item'Length
then
Overwrite'Result
(Position - Source'First + New_Item'Length + 1
.. Overwrite'Result'Last)
= Source (Position + New_Item'Length .. Source'Last)),
Global => null,
Annotate => (GNATprove, Always_Return);
-- Propagates Index_Error if Position is not in
-- Source'First .. Source'Last + 1; otherwise, returns the string obtained
-- from Source by consecutively replacing characters starting at Position
-- with corresponding characters from New_Item. If the end of Source is
-- reached before the characters in New_Item are exhausted, the remaining
-- characters from New_Item are appended to the string.
procedure Overwrite
(Source : in out String;
Position : Positive;
New_Item : String;
Drop : Truncation := Right)
with
Pre =>
Position - 1 in Source'First - 1 .. Source'Last
and then
(if Position - Source'First >= Source'Length - New_Item'Length
then Position - Source'First <= Natural'Last - New_Item'Length),
-- Incomplete contract
Global => null,
Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to Move(Overwrite(Source, Position, New_Item), Source, Drop)
function Delete
(Source : String;
From : Positive;
Through : Natural) return String
with
Pre => (if From <= Through
then (From in Source'Range
and then Through <= Source'Last)),
-- Lower bound of the returned string is 1
Post =>
Delete'Result'First = 1,
Contract_Cases =>
-- If From <= Through, the characters between From and Through are
-- removed.
(From <= Through =>
-- Length of the returned string
Delete'Result'Length = Source'Length - (Through - From + 1)
-- Elements before From are preserved
and then
Delete'Result (1 .. From - Source'First)
= Source (Source'First .. From - 1)
-- If there are remaining characters after Through, they are
-- appended to the returned string.
and then
(if Through < Source'Last
then Delete'Result
(From - Source'First + 1 .. Delete'Result'Last)
= Source (Through + 1 .. Source'Last)),
-- Otherwise, the returned string is Source with lower bound 1
others =>
Delete'Result'Length = Source'Length
and then Delete'Result = Source),
Global => null,
Annotate => (GNATprove, Always_Return);
-- If From <= Through, the returned string is
-- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with
-- lower bound 1.
procedure Delete
(Source : in out String;
From : Positive;
Through : Natural;
Justify : Alignment := Left;
Pad : Character := Space)
with
Pre => (if From <= Through
then (From in Source'Range
and then Through <= Source'Last)),
-- Incomplete contract
Global => null,
Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Delete (Source, From, Through),
-- Source, Justify => Justify, Pad => Pad).
---------------------------------
-- String Selector Subprograms --
---------------------------------
function Trim
(Source : String;
Side : Trim_End) return String
with
Post =>
-- Lower bound of the returned string is 1
Trim'Result'First = 1
-- If all characters in Source are Space, the returned string is
-- empty.
and then
(if (for all J in Source'Range => Source (J) = ' ')
then Trim'Result = ""
-- Otherwise, the returned string is a slice of Source
else
(declare
Low : constant Positive :=
(if Side = Right then Source'First
else Index_Non_Blank (Source, Forward));
High : constant Positive :=
(if Side = Left then Source'Last
else Index_Non_Blank (Source, Backward));
begin
Trim'Result = Source (Low .. High))),
Global => null,
Annotate => (GNATprove, Always_Return);
-- Returns the string obtained by removing from Source all leading Space
-- characters (if Side = Left), all trailing Space characters (if
-- Side = Right), or all leading and trailing Space characters (if
-- Side = Both).
procedure Trim
(Source : in out String;
Side : Trim_End;
Justify : Alignment := Left;
Pad : Character := Space)
with
-- Incomplete contract
Global => null,
Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Trim (Source, Side), Source, Justify=>Justify, Pad=>Pad).
function Trim
(Source : String;
Left : Maps.Character_Set;
Right : Maps.Character_Set) return String
with
Post =>
-- Lower bound of the returned string is 1
Trim'Result'First = 1
-- If all characters are contained in one of the sets Left and Right,
-- then the returned string is empty.
and then
(if (for all K in Source'Range =>
Ada.Strings.Maps.Is_In (Source (K), Left))
or
(for all K in Source'Range =>
Ada.Strings.Maps.Is_In (Source (K), Right))
then Trim'Result = ""
-- Otherwise, the returned string is a slice of Source
else
(declare
Low : constant Positive :=
Index (Source, Left, Outside, Forward);
High : constant Positive :=
Index (Source, Right, Outside, Backward);
begin
Trim'Result = Source (Low .. High))),
Global => null,
Annotate => (GNATprove, Always_Return);
-- Returns the string obtained by removing from Source all leading
-- characters in Left and all trailing characters in Right.
procedure Trim
(Source : in out String;
Left : Maps.Character_Set;
Right : Maps.Character_Set;
Justify : Alignment := Strings.Left;
Pad : Character := Space)
with
-- Incomplete contract
Global => null,
Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Trim (Source, Left, Right),
-- Source, Justify => Justify, Pad=>Pad).
function Head
(Source : String;
Count : Natural;
Pad : Character := Space) return String
with
Post =>
-- Lower bound of the returned string is 1
Head'Result'First = 1
-- Length of the returned string is Count.
and then Head'Result'Length = Count,
Contract_Cases =>
-- If Count <= Source'Length, then the first Count characters of
-- Source are returned.
(Count <= Source'Length =>
Head'Result = Source (Source'First .. Source'First - 1 + Count),
-- Otherwise, the returned string is Source concatenated with
-- Count - Source'Length Pad characters.
others =>
Head'Result (1 .. Source'Length) = Source
and then
Head'Result (Source'Length + 1 .. Count)
= [1 .. Count - Source'Length => Pad]),
Global => null,
Annotate => (GNATprove, Always_Return);
-- Returns a string of length Count. If Count <= Source'Length, the string
-- comprises the first Count characters of Source. Otherwise, its contents
-- are Source concatenated with Count - Source'Length Pad characters.
procedure Head
(Source : in out String;
Count : Natural;
Justify : Alignment := Left;
Pad : Character := Space)
with
-- Incomplete contract
Global => null,
Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Head (Source, Count, Pad),
-- Source, Drop => Error, Justify => Justify, Pad => Pad).
function Tail
(Source : String;
Count : Natural;
Pad : Character := Space) return String
with
Post =>
-- Lower bound of the returned string is 1
Tail'Result'First = 1
-- Length of the returned string is Count
and then Tail'Result'Length = Count,
Contract_Cases =>
-- If Count is zero, then the returned string is empty
(Count = 0 =>
Tail'Result = "",
-- Otherwise, if Count <= Source'Length, then the last Count
-- characters of Source are returned.
(Count in 1 .. Source'Length) =>
Tail'Result = Source (Source'Last - Count + 1 .. Source'Last),
-- Otherwise, the returned string is Count - Source'Length Pad
-- characters concatenated with Source.
others =>
-- If Source is empty, then the returned string is Count Pad
-- characters.
(if Source'Length = 0
then Tail'Result = [1 .. Count => Pad]
else
Tail'Result (1 .. Count - Source'Length)
= [1 .. Count - Source'Length => Pad]
and then
Tail'Result (Count - Source'Length + 1 .. Tail'Result'Last)
= Source)),
Global => null,
Annotate => (GNATprove, Always_Return);
-- Returns a string of length Count. If Count <= Source'Length, the string
-- comprises the last Count characters of Source. Otherwise, its contents
-- are Count-Source'Length Pad characters concatenated with Source.
procedure Tail
(Source : in out String;
Count : Natural;
Justify : Alignment := Left;
Pad : Character := Space)
with
-- Incomplete contract
Global => null,
Annotate => (GNATprove, Might_Not_Return);
-- Equivalent to:
--
-- Move (Tail (Source, Count, Pad),
-- Source, Drop => Error, Justify => Justify, Pad => Pad).
----------------------------------
-- String Constructor Functions --
----------------------------------
function "*"
(Left : Natural;
Right : Character) return String
with
Post =>
-- Lower bound of the returned string is 1
"*"'Result'First = 1
-- Length of the returned string
and then "*"'Result'Length = Left
-- All characters of the returned string are Right
and then (for all C of "*"'Result => C = Right),
Global => null,
Annotate => (GNATprove, Always_Return);
function "*"
(Left : Natural;
Right : String) return String
with
Pre => (if Right'Length /= 0 then Left <= Natural'Last / Right'Length),
Post =>
-- Lower bound of the returned string is 1
"*"'Result'First = 1
-- Length of the returned string
and then "*"'Result'Length = Left * Right'Length
-- Content of the string is Right concatenated with itself Left times
and then
(for all K in "*"'Result'Range =>
"*"'Result (K) = Right (Right'First + (K - 1) mod Right'Length)),
Global => null,
Annotate => (GNATprove, Always_Return);
-- These functions replicate a character or string a specified number of
-- times. The first function returns a string whose length is Left and each
-- of whose elements is Right. The second function returns a string whose
-- length is Left * Right'Length and whose value is the null string if
-- Left = 0 and otherwise is (Left - 1)*Right & Right with lower bound 1.
end Ada.Strings.Fixed;