@@ -30,22 +30,21 @@
------------------------------------------------------------------------------
with Ada.Strings.Fixed;
-with Ada.Strings.Search;
with Ada.Unchecked_Deallocation;
package body Ada.Strings.Unbounded is
- function Sum (Left : Natural; Right : Integer) return Natural with Inline;
+ function Sum (Left, Right : Natural) return Natural with Inline;
-- Returns summary of Left and Right, raise Constraint_Error on overflow
function Mul (Left, Right : Natural) return Natural with Inline;
-- Returns multiplication of Left and Right, raise Constraint_Error on
-- overflow.
- function Saturated_Sum (Left : Natural; Right : Integer) return Natural;
+ function Saturated_Sum (Left, Right : Natural) return Natural;
-- Returns summary of Left and Right or Natural'Last on overflow
- function Saturated_Mul (Left, Right : Natural) return Natural;
+ function Saturated_Mul (Left, Right : Positive) return Positive;
-- Returns multiplication of Left and Right or Natural'Last on overflow
---------
@@ -67,8 +66,11 @@ package body Ada.Strings.Unbounded is
Result.Reference (1 .. L_Length) :=
Left.Reference (1 .. Left.Last);
- Result.Reference (L_Length + 1 .. Result.Last) :=
- Right.Reference (1 .. Right.Last);
+
+ if L_Length < Natural'Last then
+ Result.Reference (L_Length + 1 .. Result.Last) :=
+ Right.Reference (1 .. Right.Last);
+ end if;
return Result;
end "&";
@@ -86,7 +88,10 @@ package body Ada.Strings.Unbounded is
Result.Reference := new String (1 .. Result.Last);
Result.Reference (1 .. L_Length) := Left.Reference (1 .. Left.Last);
- Result.Reference (L_Length + 1 .. Result.Last) := Right;
+
+ if L_Length < Natural'Last then
+ Result.Reference (L_Length + 1 .. Result.Last) := Right;
+ end if;
return Result;
end "&";
@@ -104,8 +109,11 @@ package body Ada.Strings.Unbounded is
Result.Reference := new String (1 .. Result.Last);
Result.Reference (1 .. Left'Length) := Left;
- Result.Reference (Left'Length + 1 .. Result.Last) :=
- Right.Reference (1 .. Right.Last);
+
+ if Left'Length < Natural'Last then
+ Result.Reference (Left'Length + 1 .. Result.Last) :=
+ Right.Reference (1 .. Right.Last);
+ end if;
return Result;
end "&";
@@ -170,17 +178,21 @@ package body Ada.Strings.Unbounded is
Right : String) return Unbounded_String
is
Len : constant Natural := Right'Length;
- K : Positive;
+ K : Natural;
Result : Unbounded_String;
begin
+ if Len = 0 then
+ return Null_Unbounded_String;
+ end if;
+
Result.Last := Mul (Left, Len);
Result.Reference := new String (1 .. Result.Last);
- K := 1;
+ K := 0;
for J in 1 .. Left loop
- Result.Reference (K .. K + Len - 1) := Right;
+ Result.Reference (K + 1 .. K + Len) := Right;
K := K + Len;
end loop;
@@ -192,17 +204,21 @@ package body Ada.Strings.Unbounded is
Right : Unbounded_String) return Unbounded_String
is
Len : constant Natural := Right.Last;
- K : Positive;
+ K : Natural;
Result : Unbounded_String;
begin
+ if Len = 0 then
+ return Null_Unbounded_String;
+ end if;
+
Result.Last := Mul (Left, Len);
Result.Reference := new String (1 .. Result.Last);
- K := 1;
+ K := 0;
for J in 1 .. Left loop
- Result.Reference (K .. K + Len - 1) :=
+ Result.Reference (K + 1 .. K + Len) :=
Right.Reference (1 .. Right.Last);
K := K + Len;
end loop;
@@ -380,8 +396,12 @@ package body Ada.Strings.Unbounded is
is
begin
Realloc_For_Chunk (Source, New_Item.Last);
- Source.Reference (Source.Last + 1 .. Source.Last + New_Item.Last) :=
- New_Item.Reference (1 .. New_Item.Last);
+
+ if Source.Last < Natural'Last then
+ Source.Reference (Source.Last + 1 .. Source.Last + New_Item.Last) :=
+ New_Item.Reference (1 .. New_Item.Last);
+ end if;
+
Source.Last := Source.Last + New_Item.Last;
end Append;
@@ -391,8 +411,12 @@ package body Ada.Strings.Unbounded is
is
begin
Realloc_For_Chunk (Source, New_Item'Length);
- Source.Reference (Source.Last + 1 .. Source.Last + New_Item'Length) :=
- New_Item;
+
+ if Source.Last < Natural'Last then
+ Source.Reference (Source.Last + 1 .. Source.Last + New_Item'Length) :=
+ New_Item;
+ end if;
+
Source.Last := Source.Last + New_Item'Length;
end Append;
@@ -462,16 +486,20 @@ package body Ada.Strings.Unbounded is
if From > Through then
null;
- elsif From < Source.Reference'First or else Through > Source.Last then
+ elsif From - 1 > Source.Last then
raise Index_Error;
else
declare
- Len : constant Natural := Through - From + 1;
+ Len : constant Natural :=
+ Natural'Min (Source.Last, Through) - From + 1;
begin
- Source.Reference (From .. Source.Last - Len) :=
- Source.Reference (Through + 1 .. Source.Last);
+ if Through < Natural'Last then
+ Source.Reference (From .. Source.Last - Len) :=
+ Source.Reference (Through + 1 .. Source.Last);
+ end if;
+
Source.Last := Source.Last - Len;
end;
end if;
@@ -714,17 +742,19 @@ package body Ada.Strings.Unbounded is
New_Item : String)
is
begin
- if Before not in Source.Reference'First .. Source.Last + 1 then
+ if Before - 1 > Source.Last then
raise Index_Error;
end if;
Realloc_For_Chunk (Source, New_Item'Length);
- Source.Reference
- (Before + New_Item'Length .. Source.Last + New_Item'Length) :=
- Source.Reference (Before .. Source.Last);
+ if Before <= Source.Last then
+ Source.Reference
+ (Before + New_Item'Length .. Source.Last + New_Item'Length) :=
+ Source.Reference (Before .. Source.Last);
+ end if;
- Source.Reference (Before .. Before + New_Item'Length - 1) := New_Item;
+ Source.Reference (Before .. Before - 1 + New_Item'Length) := New_Item;
Source.Last := Source.Last + New_Item'Length;
end Insert;
@@ -733,9 +763,7 @@ package body Ada.Strings.Unbounded is
------------
function Length (Source : Unbounded_String) return Natural is
- begin
- return Source.Last;
- end Length;
+ (Source.Last);
---------
-- Mul --
@@ -769,8 +797,8 @@ package body Ada.Strings.Unbounded is
is
NL : constant Natural := New_Item'Length;
begin
- if Position <= Source.Last - NL + 1 then
- Source.Reference (Position .. Position + NL - 1) := New_Item;
+ if Position - 1 <= Source.Last - NL then
+ Source.Reference (Position .. Position - 1 + NL) := New_Item;
else
declare
Old : String_Access := Source.Reference;
@@ -897,7 +925,7 @@ package body Ada.Strings.Unbounded is
-- Saturated_Mul --
-------------------
- function Saturated_Mul (Left, Right : Natural) return Natural is
+ function Saturated_Mul (Left, Right : Positive) return Positive is
begin
return Mul (Left, Right);
exception
@@ -905,11 +933,11 @@ package body Ada.Strings.Unbounded is
return Natural'Last;
end Saturated_Mul;
- -----------------
+ -------------------
-- Saturated_Sum --
- -----------------
+ -------------------
- function Saturated_Sum (Left : Natural; Right : Integer) return Natural is
+ function Saturated_Sum (Left, Right : Natural) return Natural is
begin
return Sum (Left, Right);
exception
@@ -945,7 +973,7 @@ package body Ada.Strings.Unbounded is
begin
-- Note: test of High > Length is in accordance with AI95-00128
- if Low > Source.Last + 1 or else High > Source.Last then
+ if Low - 1 > Source.Last or else High > Source.Last then
raise Index_Error;
else
return Source.Reference (Low .. High);
@@ -956,7 +984,7 @@ package body Ada.Strings.Unbounded is
-- Sum --
---------
- function Sum (Left : Natural; Right : Integer) return Natural is
+ function Sum (Left, Right : Natural) return Natural is
pragma Unsuppress (Overflow_Check);
begin
return Left + Right;
@@ -993,9 +1021,7 @@ package body Ada.Strings.Unbounded is
---------------
function To_String (Source : Unbounded_String) return String is
- begin
- return Source.Reference (1 .. Source.Last);
- end To_String;
+ (Source.Reference (1 .. Source.Last));
-------------------------
-- To_Unbounded_String --
@@ -35,12 +35,18 @@
-- 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);
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
-with Ada.Strings.Maps;
+with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
with Ada.Finalization;
+with Ada.Strings.Search;
private with Ada.Strings.Text_Buffers;
-- The language-defined package Strings.Unbounded provides a private type
@@ -59,6 +65,13 @@ package Ada.Strings.Unbounded with
is
pragma Preelaborate;
+ -- Contracts may call function Length in the prefix of attribute reference
+ -- to Old as in Length (Source)'Old. Allow this use.
+
+ pragma Unevaluated_Use_Of_Old (Allow);
+
+ subtype String_1 is String (1 .. <>) with Ghost; -- Type used in contracts
+
type Unbounded_String is private with
Default_Initial_Condition => Length (Unbounded_String) = 0;
pragma Preelaborable_Initialization (Unbounded_String);
@@ -84,9 +97,10 @@ is
--------------------------------------------------------
function To_Unbounded_String
- (Source : String) return Unbounded_String
+ (Source : String) return Unbounded_String
with
- Post => To_String (To_Unbounded_String'Result) = Source,
+ Post => To_String (To_Unbounded_String'Result) = Source
+ and then Length (To_Unbounded_String'Result) = Source'Length,
Global => null;
-- Returns an Unbounded_String that represents Source
@@ -126,7 +140,8 @@ is
New_Item : Unbounded_String)
with
Pre => Length (New_Item) <= Natural'Last - Length (Source),
- Post => Length (Source) = Length (Source)'Old + Length (New_Item),
+ Post =>
+ To_String (Source) = To_String (Source)'Old & To_String (New_Item),
Global => null;
procedure Append
@@ -134,7 +149,7 @@ is
New_Item : String)
with
Pre => New_Item'Length <= Natural'Last - Length (Source),
- Post => Length (Source) = Length (Source)'Old + New_Item'Length,
+ Post => To_String (Source) = To_String (Source)'Old & New_Item,
Global => null;
procedure Append
@@ -142,7 +157,7 @@ is
New_Item : Character)
with
Pre => Length (Source) < Natural'Last,
- Post => Length (Source) = Length (Source)'Old + 1,
+ Post => To_String (Source) = To_String (Source)'Old & New_Item,
Global => null;
-- For each of the Append procedures, the resulting string represented by
@@ -154,7 +169,7 @@ is
Right : Unbounded_String) return Unbounded_String
with
Pre => Length (Right) <= Natural'Last - Length (Left),
- Post => Length ("&"'Result) = Length (Left) + Length (Right),
+ Post => To_String ("&"'Result) = To_String (Left) & To_String (Right),
Global => null;
function "&"
@@ -162,7 +177,7 @@ is
Right : String) return Unbounded_String
with
Pre => Right'Length <= Natural'Last - Length (Left),
- Post => Length ("&"'Result) = Length (Left) + Right'Length,
+ Post => To_String ("&"'Result) = To_String (Left) & Right,
Global => null;
function "&"
@@ -170,7 +185,7 @@ is
Right : Unbounded_String) return Unbounded_String
with
Pre => Left'Length <= Natural'Last - Length (Right),
- Post => Length ("&"'Result) = Left'Length + Length (Right),
+ Post => To_String ("&"'Result) = String_1 (Left) & To_String (Right),
Global => null;
function "&"
@@ -178,7 +193,7 @@ is
Right : Character) return Unbounded_String
with
Pre => Length (Left) < Natural'Last,
- Post => Length ("&"'Result) = Length (Left) + 1,
+ Post => To_String ("&"'Result) = To_String (Left) & Right,
Global => null;
function "&"
@@ -186,7 +201,7 @@ is
Right : Unbounded_String) return Unbounded_String
with
Pre => Length (Right) < Natural'Last,
- Post => Length ("&"'Result) = Length (Right) + 1,
+ Post => To_String ("&"'Result) = Left & To_String (Right),
Global => null;
-- Each of the "&" functions returns an Unbounded_String obtained by
@@ -211,7 +226,8 @@ is
By : Character)
with
Pre => Index <= Length (Source),
- Post => Length (Source) = Length (Source)'Old,
+ Post =>
+ To_String (Source) = (To_String (Source)'Old with delta Index => By),
Global => null;
-- Updates Source such that the character at position Index in the string
-- represented by Source is By; propagates Index_Error if
@@ -223,7 +239,9 @@ is
High : Natural) return String
with
Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
- Post => Slice'Result'Length = Natural'Max (0, High - Low + 1),
+ Post => Slice'Result'First = Low
+ and then Slice'Result'Last = High
+ and then Slice'Result = To_String (Source) (Low .. High),
Global => null;
-- Returns the slice at positions Low through High in the string
-- represented by Source; propagates Index_Error if
@@ -237,7 +255,7 @@ is
with
Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
Post =>
- Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
+ To_String (Unbounded_Slice'Result) = To_String (Source) (Low .. High),
Global => null;
pragma Ada_05 (Unbounded_Slice);
-- Returns the slice at positions Low through High in the string
@@ -251,7 +269,7 @@ is
High : Natural)
with
Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
- Post => Length (Target) = Natural'Max (0, High - Low + 1),
+ Post => To_String (Target) = To_String (Source) (Low .. High),
Global => null;
pragma Ada_05 (Unbounded_Slice);
-- Sets Target to the Unbounded_String representing the slice at positions
@@ -283,72 +301,84 @@ is
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
+ Post => "<"'Result = (To_String (Left) < To_String (Right)),
Global => null;
function "<"
(Left : Unbounded_String;
Right : String) return Boolean
with
+ Post => "<"'Result = (To_String (Left) < Right),
Global => null;
function "<"
(Left : String;
Right : Unbounded_String) return Boolean
with
+ Post => "<"'Result = (Left < To_String (Right)),
Global => null;
function "<="
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
+ Post => "<="'Result = (To_String (Left) <= To_String (Right)),
Global => null;
function "<="
(Left : Unbounded_String;
Right : String) return Boolean
with
+ Post => "<="'Result = (To_String (Left) <= Right),
Global => null;
function "<="
(Left : String;
Right : Unbounded_String) return Boolean
with
+ Post => "<="'Result = (Left <= To_String (Right)),
Global => null;
function ">"
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
+ Post => ">"'Result = (To_String (Left) > To_String (Right)),
Global => null;
function ">"
(Left : Unbounded_String;
Right : String) return Boolean
with
+ Post => ">"'Result = (To_String (Left) > Right),
Global => null;
function ">"
(Left : String;
Right : Unbounded_String) return Boolean
with
+ Post => ">"'Result = (Left > To_String (Right)),
Global => null;
function ">="
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
+ Post => ">="'Result = (To_String (Left) >= To_String (Right)),
Global => null;
function ">="
(Left : Unbounded_String;
Right : String) return Boolean
with
+ Post => ">="'Result = (To_String (Left) >= Right),
Global => null;
function ">="
(Left : String;
Right : Unbounded_String) return Boolean
with
+ Post => ">="'Result = (Left >= To_String (Right)),
Global => null;
-- Each of the functions "=", "<", ">", "<=", and ">=" returns the same
@@ -365,8 +395,52 @@ is
Going : Direction := Forward;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
with
- Pre => Pattern'Length /= 0,
- Global => null;
+ Pre => Pattern'Length > 0,
+ Post => Index'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Length (Source) = 0
+ =>
+ Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Length (Source) > 0
+ and then
+ (for some J in 1 .. Length (Source) - (Pattern'Length - 1) =>
+ Search.Match (To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Index'Result in 1 .. Length (Source) - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (To_String (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 1 .. Length (Source) =>
+ (if (if Going = Forward
+ then J <= Index'Result - 1
+ else J - 1 in Index'Result
+ .. Length (Source) - Pattern'Length)
+ then not (Search.Match
+ (To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
+ Global => null;
function Index
(Source : Unbounded_String;
@@ -374,8 +448,52 @@ is
Going : Direction := Forward;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre => Pattern'Length /= 0,
- Global => null;
+ Pre => Pattern'Length /= 0 and then Mapping /= null,
+ Post => Index'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Length (Source) = 0
+ =>
+ Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Length (Source) > 0
+ and then
+ (for some J in 1 .. Length (Source) - (Pattern'Length - 1) =>
+ Search.Match (To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Index'Result in 1 .. Length (Source) - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (To_String (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 1 .. Length (Source) =>
+ (if (if Going = Forward
+ then J <= Index'Result - 1
+ else J - 1 in Index'Result
+ .. Length (Source) - Pattern'Length)
+ then not (Search.Match
+ (To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
+ Global => null;
function Index
(Source : Unbounded_String;
@@ -383,7 +501,43 @@ is
Test : Membership := Inside;
Going : Direction := Forward) return Natural
with
- Global => null;
+ Post => Index'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If no character of Source satisfies the property Test on Set,
+ -- then 0 is returned.
+
+ ((for all C of To_String (Source) =>
+ (Test = Inside) /= 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 1 .. Length (Source)
+
+ -- The character at the returned index satisfies the property
+ -- Test on Set.
+
+ and then
+ (Test = Inside) =
+ Maps.Is_In (Element (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 1 .. Length (Source) =>
+ (if J /= Index'Result
+ and then (J < Index'Result) = (Going = Forward)
+ then (Test = Inside)
+ /= Maps.Is_In (Element (Source, J), Set)))),
+ Global => null;
function Index
(Source : Unbounded_String;
@@ -392,9 +546,60 @@ is
Going : Direction := Forward;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
with
- Pre => (if Length (Source) /= 0 then From <= Length (Source))
- and then Pattern'Length /= 0,
- Global => null;
+ Pre =>
+ (if Length (Source) /= 0 then From <= Length (Source))
+ and then Pattern'Length /= 0,
+ Post => Index'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Length (Source) = 0
+ =>
+ Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Length (Source) > 0
+ and then
+ (for some J in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Length (Source) else From)
+ - (Pattern'Length - 1) =>
+ Search.Match (To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Index'Result in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Length (Source) else From)
+ - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (To_String (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 1 .. Length (Source) =>
+ (if (if Going = Forward
+ then J in From .. Index'Result - 1
+ else J - 1 in Index'Result
+ .. From - Pattern'Length)
+ then not (Search.Match
+ (To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
+ Global => null;
pragma Ada_05 (Index);
function Index
@@ -404,9 +609,61 @@ is
Going : Direction := Forward;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre => (if Length (Source) /= 0 then From <= Length (Source))
- and then Pattern'Length /= 0,
- Global => null;
+ Pre =>
+ (if Length (Source) /= 0 then From <= Length (Source))
+ and then Pattern'Length /= 0
+ and then Mapping /= null,
+ Post => Index'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Length (Source) = 0
+ =>
+ Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Length (Source) > 0
+ and then
+ (for some J in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Length (Source) else From)
+ - (Pattern'Length - 1) =>
+ Search.Match (To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Index'Result in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Length (Source) else From)
+ - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (To_String (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 1 .. Length (Source) =>
+ (if (if Going = Forward
+ then J in From .. Index'Result - 1
+ else J - 1 in Index'Result
+ .. From - Pattern'Length)
+ then not (Search.Match
+ (To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
+ Global => null;
pragma Ada_05 (Index);
function Index
@@ -416,23 +673,147 @@ is
Test : Membership := Inside;
Going : Direction := Forward) return Natural
with
- Pre => (if Length (Source) /= 0 then From <= Length (Source)),
- Global => null;
+ Pre =>
+ (if Length (Source) /= 0 then From <= Length (Source)),
+ Post => Index'Result <= Length (Source),
+ 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.
+
+ (Length (Source) = 0
+ or else
+ (for all J in 1 .. Length (Source) =>
+ (if J = From or else (J > From) = (Going = Forward) then
+ (Test = Inside) /= Maps.Is_In (Element (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 1 .. Length (Source)
+ 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) =
+ Maps.Is_In (Element (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 1 .. Length (Source) =>
+ (if J /= Index'Result
+ and then (J < Index'Result) = (Going = Forward)
+ and then (J = From
+ or else (J > From) = (Going = Forward))
+ then (Test = Inside)
+ /= Maps.Is_In (Element (Source, J), Set)))),
+ Global => null;
pragma Ada_05 (Index);
function Index_Non_Blank
(Source : Unbounded_String;
Going : Direction := Forward) return Natural
with
- Global => null;
+ Post => Index_Non_Blank'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If all characters of Source are Space characters, then 0 is
+ -- returned.
+
+ ((for all C of To_String (Source) => C = ' ')
+ =>
+ Index_Non_Blank'Result = 0,
+
+ -- Otherwise, an index in the range of Source is returned
+
+ others
+ =>
+ -- The result is in the range of Source
+
+ Index_Non_Blank'Result in 1 .. Length (Source)
+
+ -- The character at the returned index is not a Space character
+
+ and then Element (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 1 .. Length (Source) =>
+ (if J /= Index_Non_Blank'Result
+ and then
+ (J < Index_Non_Blank'Result) = (Going = Forward)
+ then Element (Source, J) = ' '))),
+ Global => null;
function Index_Non_Blank
(Source : Unbounded_String;
From : Positive;
Going : Direction := Forward) return Natural
with
- Pre => (if Length (Source) /= 0 then From <= Length (Source)),
- Global => null;
+ Pre =>
+ (if Length (Source) /= 0 then From <= Length (Source)),
+ Post => Index_Non_Blank'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, or all characters of the
+ -- considered slice of Source are Space characters, then 0
+ -- is returned.
+
+ (Length (Source) = 0
+ or else
+ (for all J in 1 .. Length (Source) =>
+ (if J = From or else (J > From) = (Going = Forward) then
+ Element (Source, J) = ' '))
+ =>
+ Index_Non_Blank'Result = 0,
+
+ -- Otherwise, an index in the considered range of Source is
+ -- returned.
+
+ others
+ =>
+ -- The result is in the considered range of Source
+
+ Index_Non_Blank'Result in 1 .. Length (Source)
+ 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 Element (Source, Index_Non_Blank'Result) /= ' '
+
+ -- The result is the smallest or largest index which isn't a
+ -- Space character, respectively when Going = Forward and Going
+ -- = Backward.
+
+ and then
+ (for all J in 1 .. Length (Source) =>
+ (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 Element (Source, J) = ' '))),
+ Global => null;
pragma Ada_05 (Index_Non_Blank);
function Count
@@ -448,7 +829,7 @@ is
Pattern : String;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre => Pattern'Length /= 0,
+ Pre => Pattern'Length /= 0 and then Mapping /= null,
Global => null;
function Count
@@ -465,8 +846,53 @@ is
First : out Positive;
Last : out Natural)
with
- Pre => (if Length (Source) /= 0 then From <= Length (Source)),
- Global => null;
+ Pre =>
+ (if Length (Source) /= 0 then From <= Length (Source)),
+ 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.
+
+ (Length (Source) = 0
+ or else
+ (for all J in From .. Length (Source) =>
+ (Test = Inside) /= Maps.Is_In (Element (Source, J), 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 .. Length (Source)
+ and then Last in First .. Length (Source)
+
+ -- No character between From and First satisfies the property
+ -- Test on Set.
+
+ and then
+ (for all J in From .. First - 1 =>
+ (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+
+ -- All characters between First and Last satisfy the property
+ -- Test on Set.
+
+ and then
+ (for all J in First .. Last =>
+ (Test = Inside) = Maps.Is_In (Element (Source, J), 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 < Length (Source)
+ then
+ (Test = Inside)
+ /= Maps.Is_In (Element (Source, Last + 1), Set))),
+ Global => null;
pragma Ada_2012 (Find_Token);
procedure Find_Token
@@ -476,7 +902,51 @@ is
First : out Positive;
Last : out Natural)
with
- Global => null;
+ 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 1 and Last is set to 0.
+
+ (Length (Source) = 0
+ or else
+ (for all J in 1 .. Length (Source) =>
+ (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+ =>
+ First = 1 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 1 .. Length (Source)
+ and then Last in First .. Length (Source)
+
+ -- No character between 1 and First satisfies the property Test
+ -- on Set.
+
+ and then
+ (for all J in 1 .. First - 1 =>
+ (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+
+ -- All characters between First and Last satisfy the property
+ -- Test on Set.
+
+ and then
+ (for all J in First .. Last =>
+ (Test = Inside) = Maps.Is_In (Element (Source, J), 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 < Length (Source)
+ then
+ (Test = Inside)
+ /= Maps.Is_In (Element (Source, Last + 1), Set))),
+ Global => null;
-- Each of the search subprograms (Index, Index_Non_Blank, Count,
-- Find_Token) has the same effect as the corresponding subprogram in
@@ -491,28 +961,44 @@ is
(Source : Unbounded_String;
Mapping : Maps.Character_Mapping) return Unbounded_String
with
- Post => Length (Translate'Result) = Length (Source),
+ Post => Length (Translate'Result) = Length (Source)
+ and then
+ (for all K in 1 .. Length (Source) =>
+ Element (Translate'Result, K) =
+ Ada.Strings.Maps.Value (Mapping, Element (Source, K))),
Global => null;
procedure Translate
(Source : in out Unbounded_String;
Mapping : Maps.Character_Mapping)
with
- Post => Length (Source) = Length (Source)'Old,
+ Post => Length (Source) = Length (Source)'Old
+ and then
+ (for all K in 1 .. Length (Source) =>
+ Element (Source, K) =
+ Ada.Strings.Maps.Value (Mapping, To_String (Source)'Old (K))),
Global => null;
function Translate
(Source : Unbounded_String;
Mapping : Maps.Character_Mapping_Function) return Unbounded_String
with
- Post => Length (Translate'Result) = Length (Source),
+ Pre => Mapping /= null,
+ Post => Length (Translate'Result) = Length (Source)
+ and then
+ (for all K in 1 .. Length (Source) =>
+ Element (Translate'Result, K) = Mapping (Element (Source, K))),
Global => null;
procedure Translate
(Source : in out Unbounded_String;
Mapping : Maps.Character_Mapping_Function)
with
- Post => Length (Source) = Length (Source)'Old,
+ Pre => Mapping /= null,
+ Post => Length (Source) = Length (Source)'Old
+ and then
+ (for all K in 1 .. Length (Source) =>
+ Element (Source, K) = Mapping (To_String (Source)'Old (K))),
Global => null;
-- The Translate function has an analogous effect to the corresponding
@@ -535,15 +1021,76 @@ is
and then (if High >= Low
then Low - 1
<= Natural'Last - By'Length
- - Natural'Max (Length (Source) - High, 0)
+ - Integer'Max (Length (Source) - High, 0)
else Length (Source) <= Natural'Last - By'Length),
Contract_Cases =>
+
+ -- If High >= Low, when considering the application of To_String to
+ -- convert an Unbounded_String into String, then the returned string
+ -- comprises Source (Source'First .. Low - 1) & By
+ -- & Source(High + 1 .. Source'Last).
+
(High >= Low =>
+
+ -- Length of the returned string
+
Length (Replace_Slice'Result)
- = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+ = Low - 1 + By'Length + Integer'Max (Length (Source) - High, 0)
+
+ -- Elements starting at Low are replaced by elements of By
+
+ and then
+ Slice (Replace_Slice'Result, 1, Low - 1) =
+ Slice (Source, 1, Low - 1)
+ and then
+ Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By
+
+ -- When there are remaining characters after the replaced slice,
+ -- they are appended to the result.
+
+ and then
+ (if High < Length (Source)
+ then
+ Slice (Replace_Slice'Result,
+ Low + By'Length, Length (Replace_Slice'Result)) =
+ Slice (Source, High + 1, Length (Source))),
+
+ -- If High < Low, then the returned string is
+ -- Insert (Source, Before => Low, New_Item => By).
+
others =>
- Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
+
+ -- Length of the returned string
+
+ Length (Replace_Slice'Result) = Length (Source) + By'Length
+
+ -- Elements of By are inserted after the element at Low
+
+ and then
+ Slice (Replace_Slice'Result, 1, Low - 1) =
+ Slice (Source, 1, Low - 1)
+ and then
+ Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By
+
+ -- When there are remaining characters after Low in Source, they
+ -- are appended to the result.
+
+ and then
+ (if Low < Length (Source)
+ then
+ Slice (Replace_Slice'Result,
+ Low + By'Length, Length (Replace_Slice'Result)) =
+ Slice (Source, Low, Length (Source)))),
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 Unbounded_String;
@@ -559,11 +1106,61 @@ is
- Natural'Max (Length (Source) - High, 0)
else Length (Source) <= Natural'Last - By'Length),
Contract_Cases =>
+
+ -- If High >= Low, when considering the application of To_String to
+ -- convert an Unbounded_String into String, then the returned string
+ -- comprises Source (Source'First .. Low - 1) & By
+ -- & Source(High + 1 .. Source'Last).
+
(High >= Low =>
+
+ -- Length of the returned string
+
Length (Source)
- = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+ = Low - 1 + By'Length + Integer'Max (Length (Source)'Old - High, 0)
+
+ -- Elements starting at Low are replaced by elements of By
+
+ and then Slice (Source, 1, Low - 1) =
+ Slice (Source, 1, Low - 1)'Old
+ and then Slice (Source, Low, Low - 1 + By'Length) = By
+
+ -- When there are remaining characters after the replaced slice,
+ -- they are appended to the result.
+
+ and then
+ (if High < Length (Source)'Old
+ then Slice (Source, Low + By'Length, Length (Source)) =
+ Slice (Source,
+ -- Really "High + 1" but expressed with a conditional
+ -- repeating the above test so that the call to Slice
+ -- is valid on entry (under 'Old) even when the test
+ -- evaluates to False.
+ (if High < Length (Source) then High + 1 else 1),
+ Length (Source))'Old),
+
+ -- If High < Low, then the returned string is
+ -- Insert (Source, Before => Low, New_Item => By).
+
others =>
- Length (Source) = Length (Source)'Old + By'Length),
+
+ -- Length of the returned string
+
+ Length (Source) = Length (Source)'Old + By'Length
+
+ -- Elements of By are inserted after the element at Low
+
+ and then Slice (Source, 1, Low - 1) =
+ Slice (Source, 1, Low - 1)'Old
+ and then Slice (Source, Low, Low - 1 + By'Length) = By
+
+ -- When there are remaining characters after Low in Source, they
+ -- are appended to the result.
+
+ and then
+ (if Low < Length (Source)'Old
+ then Slice (Source, Low + By'Length, Length (Source)) =
+ Slice (Source, Low, Length (Source))'Old)),
Global => null;
function Insert
@@ -573,8 +1170,32 @@ is
with
Pre => Before - 1 <= Length (Source)
and then New_Item'Length <= Natural'Last - Length (Source),
- Post => Length (Insert'Result) = Length (Source) + New_Item'Length,
+ Post =>
+ -- Length of the returned string
+
+ Length (Insert'Result) = Length (Source) + New_Item'Length
+
+ -- Elements of New_Item are inserted after element at Before
+
+ and then
+ Slice (Insert'Result, 1, Before - 1) = Slice (Source, 1, Before - 1)
+ and then
+ Slice (Insert'Result, Before, Before - 1 + 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 <= Length (Source) then
+ Slice (Insert'Result, Before + New_Item'Length,
+ Length (Insert'Result)) =
+ Slice (Source, Before, Length (Source))),
Global => null;
+ -- 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 Unbounded_String;
@@ -583,7 +1204,25 @@ is
with
Pre => Before - 1 <= Length (Source)
and then New_Item'Length <= Natural'Last - Length (Source),
- Post => Length (Source) = Length (Source)'Old + New_Item'Length,
+ Post =>
+ -- Length of the returned string
+
+ Length (Source) = Length (Source)'Old + New_Item'Length
+
+ -- Elements of New_Item are inserted after element at Before
+
+ and then
+ Slice (Source, 1, Before - 1) = Slice (Source, 1, Before - 1)'Old
+ and then
+ Slice (Source, Before, Before - 1 + 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 <= Length (Source)'Old then
+ Slice (Source, Before + New_Item'Length, Length (Source)) =
+ Slice (Source, Before, Length (Source))'Old),
Global => null;
function Overwrite
@@ -592,12 +1231,31 @@ is
New_Item : String) return Unbounded_String
with
Pre => Position - 1 <= Length (Source)
- and then (if New_Item'Length /= 0
- then
- New_Item'Length <= Natural'Last - (Position - 1)),
+ and then New_Item'Length <= Natural'Last - (Position - 1),
Post =>
- Length (Overwrite'Result)
- = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
+ -- Length of the returned string
+
+ Length (Overwrite'Result) =
+ Integer'Max (Length (Source), Position - 1 + New_Item'Length)
+
+ -- Elements after Position are replaced by elements of New_Item
+
+ and then
+ Slice (Overwrite'Result, 1, Position - 1) =
+ Slice (Source, 1, Position - 1)
+ and then
+ Slice (Overwrite'Result, Position, Position - 1 + New_Item'Length) =
+ New_Item
+ and then
+ (if Position - 1 + New_Item'Length < Length (Source) then
+
+ -- There are some unchanged characters of Source remaining
+ -- after New_Item.
+
+ Slice (Overwrite'Result,
+ Position + New_Item'Length, Length (Source)) =
+ Slice (Source,
+ Position + New_Item'Length, Length (Source))),
Global => null;
procedure Overwrite
@@ -606,13 +1264,36 @@ is
New_Item : String)
with
Pre => Position - 1 <= Length (Source)
- and then (if New_Item'Length /= 0
- then
- New_Item'Length <= Natural'Last - (Position - 1)),
+ and then New_Item'Length <= Natural'Last - (Position - 1),
Post =>
- Length (Source)
- = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
+ -- Length of the returned string
+
+ Length (Source) =
+ Integer'Max (Length (Source)'Old, Position - 1 + New_Item'Length)
+
+ -- Elements after Position are replaced by elements of New_Item
+
+ and then
+ Slice (Source, 1, Position - 1) = Slice (Source, 1, Position - 1)
+ and then
+ Slice (Source, Position, Position - 1 + New_Item'Length) = New_Item
+ and then
+ (if Position - 1 + New_Item'Length < Length (Source)'Old then
+
+ -- There are some unchanged characters of Source remaining
+ -- after New_Item.
+ Slice (Source,
+ Position + New_Item'Length, Length (Source)'Old) =
+ Slice (Source,
+ -- Really "Position + New_Item'Length" but expressed with
+ -- a conditional repeating the above test so that the
+ -- call to Slice is valid on entry (under 'Old) even
+ -- when the test evaluates to False.
+ (if Position - 1 + New_Item'Length < Length (Source)
+ then Position + New_Item'Length
+ else 1),
+ Length (Source))'Old),
Global => null;
function Delete
@@ -620,12 +1301,19 @@ is
From : Positive;
Through : Natural) return Unbounded_String
with
- Pre => (if Through <= From then From - 1 <= Length (Source)),
+ Pre => (if Through >= From then From - 1 <= Length (Source)),
Contract_Cases =>
(Through >= From =>
- Length (Delete'Result) = Length (Source) - (Through - From + 1),
+ Length (Delete'Result) =
+ From - 1 + Natural'Max (Length (Source) - Through, 0)
+ and then
+ Slice (Delete'Result, 1, From - 1) = Slice (Source, 1, From - 1)
+ and then
+ (if Through < Length (Source) then
+ Slice (Delete'Result, From, Length (Delete'Result)) =
+ Slice (Source, Through + 1, Length (Source))),
others =>
- Length (Delete'Result) = Length (Source)),
+ Delete'Result = Source),
Global => null;
procedure Delete
@@ -633,82 +1321,255 @@ is
From : Positive;
Through : Natural)
with
- Pre => (if Through <= From then From - 1 <= Length (Source)),
+ Pre => (if Through >= From then From - 1 <= Length (Source)),
Contract_Cases =>
(Through >= From =>
- Length (Source) = Length (Source)'Old - (Through - From + 1),
+ Length (Source) =
+ From - 1 + Natural'Max (Length (Source)'Old - Through, 0)
+ and then
+ Slice (Source, 1, From - 1) =
+ To_String (Source)'Old (1 .. From - 1)
+ and then
+ (if Through < Length (Source) then
+ Slice (Source, From, Length (Source)) =
+ To_String (Source)'Old (Through + 1 .. Length (Source)'Old)),
others =>
- Length (Source) = Length (Source)'Old),
+ To_String (Source) = To_String (Source)'Old),
Global => null;
function Trim
(Source : Unbounded_String;
Side : Trim_End) return Unbounded_String
with
- Post => Length (Trim'Result) <= Length (Source),
- Global => null;
+ Contract_Cases =>
+ -- If all characters in Source are Space, the returned string is
+ -- empty.
+
+ ((for all C of To_String (Source) => C = ' ')
+ =>
+ Length (Trim'Result) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ (if Side = Right then 1
+ else Index_Non_Blank (Source, Forward));
+ High : constant Positive :=
+ (if Side = Left then Length (Source)
+ else Index_Non_Blank (Source, Backward));
+ begin
+ To_String (Trim'Result) = Slice (Source, Low, High))),
+ Global => null;
procedure Trim
(Source : in out Unbounded_String;
Side : Trim_End)
with
- Post => Length (Source) <= Length (Source)'Old,
- Global => null;
+ Contract_Cases =>
+ -- If all characters in Source are Space, the returned string is
+ -- empty.
+
+ ((for all C of To_String (Source) => C = ' ')
+ =>
+ Length (Source) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ (if Side = Right then 1
+ else Index_Non_Blank (Source, Forward)'Old);
+ High : constant Positive :=
+ (if Side = Left then Length (Source)'Old
+ else Index_Non_Blank (Source, Backward)'Old);
+ begin
+ To_String (Source) = To_String (Source)'Old (Low .. High))),
+ Global => null;
function Trim
(Source : Unbounded_String;
Left : Maps.Character_Set;
Right : Maps.Character_Set) return Unbounded_String
with
- Post => Length (Trim'Result) <= Length (Source),
- Global => null;
+ Contract_Cases =>
+ -- If all characters in Source are contained in one of the sets Left
+ -- or Right, then the returned string is empty.
+
+ ((for all C of To_String (Source) => Maps.Is_In (C, Left))
+ or else
+ (for all C of To_String (Source) => Maps.Is_In (C, Right))
+ =>
+ Length (Trim'Result) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ Index (Source, Left, Outside, Forward);
+ High : constant Positive :=
+ Index (Source, Right, Outside, Backward);
+ begin
+ To_String (Trim'Result) = Slice (Source, Low, High))),
+ Global => null;
procedure Trim
(Source : in out Unbounded_String;
Left : Maps.Character_Set;
Right : Maps.Character_Set)
with
- Post => Length (Source) <= Length (Source)'Old,
- Global => null;
+ Contract_Cases =>
+ -- If all characters in Source are contained in one of the sets Left
+ -- or Right, then the returned string is empty.
+
+ ((for all C of To_String (Source) => Maps.Is_In (C, Left))
+ or else
+ (for all C of To_String (Source) => Maps.Is_In (C, Right))
+ =>
+ Length (Source) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ Index (Source, Left, Outside, Forward)'Old;
+ High : constant Positive :=
+ Index (Source, Right, Outside, Backward)'Old;
+ begin
+ To_String (Source) = To_String (Source)'Old (Low .. High))),
+ Global => null;
function Head
(Source : Unbounded_String;
Count : Natural;
Pad : Character := Space) return Unbounded_String
with
- Post => Length (Head'Result) = Count,
- Global => null;
+ Post => Length (Head'Result) = Count,
+ Contract_Cases =>
+ (Count <= Length (Source)
+ =>
+ -- Source is cut
+
+ To_String (Head'Result) = Slice (Source, 1, Count),
+
+ others
+ =>
+ -- Source is followed by Pad characters
+
+ Slice (Head'Result, 1, Length (Source)) = To_String (Source)
+ and then
+ Slice (Head'Result, Length (Source) + 1, Count) =
+ [1 .. Count - Length (Source) => Pad]),
+ Global => null;
procedure Head
(Source : in out Unbounded_String;
Count : Natural;
Pad : Character := Space)
with
- Post => Length (Source) = Count,
- Global => null;
+ Post => Length (Source) = Count,
+ Contract_Cases =>
+ (Count <= Length (Source)
+ =>
+ -- Source is cut
+
+ To_String (Source) = Slice (Source, 1, Count),
+
+ others
+ =>
+ -- Source is followed by Pad characters
+
+ Slice (Source, 1, Length (Source)'Old) = To_String (Source)'Old
+ and then
+ Slice (Source, Length (Source)'Old + 1, Count) =
+ [1 .. Count - Length (Source)'Old => Pad]),
+ Global => null;
function Tail
(Source : Unbounded_String;
Count : Natural;
Pad : Character := Space) return Unbounded_String
with
- Post => Length (Tail'Result) = Count,
- Global => null;
+ Post => Length (Tail'Result) = Count,
+ Contract_Cases =>
+ (Count = 0
+ =>
+ True,
+
+ (Count in 1 .. Length (Source))
+ =>
+ -- Source is cut
+
+ To_String (Tail'Result) =
+ Slice (Source, Length (Source) - Count + 1, Length (Source)),
+
+ others
+ =>
+ -- Source is preceded by Pad characters
+
+ (if Length (Source) = 0 then
+ To_String (Tail'Result) = [1 .. Count => Pad]
+ else
+ Slice (Tail'Result, 1, Count - Length (Source)) =
+ [1 .. Count - Length (Source) => Pad]
+ and then
+ Slice (Tail'Result, Count - Length (Source) + 1, Count) =
+ To_String (Source))),
+ Global => null;
procedure Tail
(Source : in out Unbounded_String;
Count : Natural;
Pad : Character := Space)
with
- Post => Length (Source) = Count,
- Global => null;
+ Post => Length (Source) = Count,
+ Contract_Cases =>
+ (Count = 0
+ =>
+ True,
+
+ (Count in 1 .. Length (Source))
+ =>
+ -- Source is cut
+
+ To_String (Source) =
+ Slice (Source,
+ -- Really "Length (Source) - Count + 1" but expressed with a
+ -- conditional repeating the above guard so that the call to
+ -- Slice is valid on entry (under 'Old) even when the test
+ -- evaluates to False.
+ (if Count <= Length (Source) then Length (Source) - Count + 1
+ else 1),
+ Length (Source))'Old,
+
+ others
+ =>
+ -- Source is preceded by Pad characters
+
+ (if Length (Source)'Old = 0 then
+ To_String (Source) = [1 .. Count => Pad]
+ else
+ Slice (Source, 1, Count - Length (Source)'Old) =
+ [1 .. Count - Length (Source)'Old => Pad]
+ and then
+ Slice (Source, Count - Length (Source)'Old + 1, Count) =
+ To_String (Source)'Old)),
+ Global => null;
function "*"
(Left : Natural;
Right : Character) return Unbounded_String
with
Pre => Left <= Natural'Last,
- Post => Length ("*"'Result) = Left,
+ Post => To_String ("*"'Result) = [1 .. Left => Right],
Global => null;
function "*"
@@ -716,7 +1577,13 @@ is
Right : String) return Unbounded_String
with
Pre => (if Left /= 0 then Right'Length <= Natural'Last / Left),
- Post => Length ("*"'Result) = Left * Right'Length,
+ Post =>
+ Length ("*"'Result) = Left * Right'Length
+ and then
+ (if Right'Length > 0 then
+ (for all K in 1 .. Left * Right'Length =>
+ Element ("*"'Result, K) =
+ Right (Right'First + (K - 1) mod Right'Length))),
Global => null;
function "*"
@@ -724,7 +1591,13 @@ is
Right : Unbounded_String) return Unbounded_String
with
Pre => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
- Post => Length ("*"'Result) = Left * Length (Right),
+ Post =>
+ Length ("*"'Result) = Left * Length (Right)
+ and then
+ (if Length (Right) > 0 then
+ (for all K in 1 .. Left * Length (Right) =>
+ Element ("*"'Result, K) =
+ Element (Right, 1 + (K - 1) mod Length (Right)))),
Global => null;
-- Each of the transformation functions (Replace_Slice, Insert, Overwrite,
@@ -29,7 +29,6 @@
-- --
------------------------------------------------------------------------------
-with Ada.Strings.Search;
with Ada.Unchecked_Deallocation;
package body Ada.Strings.Unbounded is
@@ -58,7 +57,7 @@ package body Ada.Strings.Unbounded is
-- Calculation takes into account alignment of the allocated memory
-- segments to use memory effectively by Append/Insert/etc operations.
- function Sum (Left : Natural; Right : Integer) return Natural with Inline;
+ function Sum (Left, Right : Natural) return Natural with Inline;
-- Returns summary of Left and Right, raise Constraint_Error on overflow
function Mul (Left, Right : Natural) return Natural with Inline;
@@ -165,7 +164,11 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL);
DR.Data (1 .. Left'Length) := Left;
- DR.Data (Left'Length + 1 .. DL) := RR.Data (1 .. RR.Last);
+
+ if Left'Length < Natural'Last then
+ DR.Data (Left'Length + 1 .. DL) := RR.Data (1 .. RR.Last);
+ end if;
+
DR.Last := DL;
end if;
@@ -243,7 +246,7 @@ package body Ada.Strings.Unbounded is
is
DL : constant Natural := Mul (Left, Right'Length);
DR : Shared_String_Access;
- K : Positive;
+ K : Natural;
begin
-- Result is an empty string, reuse shared empty string
@@ -255,10 +258,10 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL);
- K := 1;
+ K := 0;
for J in 1 .. Left loop
- DR.Data (K .. K + Right'Length - 1) := Right;
+ DR.Data (K + 1 .. K + Right'Length) := Right;
K := K + Right'Length;
end loop;
@@ -275,7 +278,7 @@ package body Ada.Strings.Unbounded is
RR : constant Shared_String_Access := Right.Reference;
DL : constant Natural := Mul (Left, RR.Last);
DR : Shared_String_Access;
- K : Positive;
+ K : Natural;
begin
-- Result is an empty string, reuse shared empty string
@@ -293,10 +296,10 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL);
- K := 1;
+ K := 0;
for J in 1 .. Left loop
- DR.Data (K .. K + RR.Last - 1) := RR.Data (1 .. RR.Last);
+ DR.Data (K + 1 .. K + RR.Last) := RR.Data (1 .. RR.Last);
K := K + RR.Last;
end loop;
@@ -703,15 +706,15 @@ package body Ada.Strings.Unbounded is
Reference (SR);
DR := SR;
- -- Index is out of range
+ -- From is too large
- elsif Through > SR.Last then
+ elsif From - 1 > SR.Last then
raise Index_Error;
-- Compute size of the result
else
- DL := SR.Last - (Through - From + 1);
+ DL := SR.Last - (Natural'Min (SR.Last, Through) - From + 1);
-- Result is an empty string, reuse shared empty string
@@ -723,7 +726,11 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL);
DR.Data (1 .. From - 1) := SR.Data (1 .. From - 1);
- DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+
+ if Through < Natural'Last then
+ DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+ end if;
+
DR.Last := DL;
end if;
end if;
@@ -746,13 +753,13 @@ package body Ada.Strings.Unbounded is
if From > Through then
null;
- -- Through is outside of the range
+ -- From is too large
- elsif Through > SR.Last then
+ elsif From - 1 > SR.Last then
raise Index_Error;
else
- DL := SR.Last - (Through - From + 1);
+ DL := SR.Last - (Natural'Min (SR.Last, Through) - From + 1);
-- Result is empty, reuse shared empty string
@@ -763,7 +770,10 @@ package body Ada.Strings.Unbounded is
-- Try to reuse existing shared string
elsif Can_Be_Reused (SR, DL) then
- SR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+ if Through < Natural'Last then
+ SR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+ end if;
+
SR.Last := DL;
-- Otherwise, allocate new shared string
@@ -771,7 +781,11 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL);
DR.Data (1 .. From - 1) := SR.Data (1 .. From - 1);
- DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+
+ if Through < Natural'Last then
+ DR.Data (From .. DL) := SR.Data (Through + 1 .. SR.Last);
+ end if;
+
DR.Last := DL;
Source.Reference := DR;
Unreference (SR);
@@ -1093,7 +1107,7 @@ package body Ada.Strings.Unbounded is
begin
-- Check index first
- if Before > SR.Last + 1 then
+ if Before - 1 > SR.Last then
raise Index_Error;
end if;
@@ -1113,9 +1127,13 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL, DL / Growth_Factor);
DR.Data (1 .. Before - 1) := SR.Data (1 .. Before - 1);
- DR.Data (Before .. Before + New_Item'Length - 1) := New_Item;
- DR.Data (Before + New_Item'Length .. DL) :=
- SR.Data (Before .. SR.Last);
+ DR.Data (Before .. Before - 1 + New_Item'Length) := New_Item;
+
+ if Before <= SR.Last then
+ DR.Data (Before + New_Item'Length .. DL) :=
+ SR.Data (Before .. SR.Last);
+ end if;
+
DR.Last := DL;
end if;
@@ -1134,7 +1152,7 @@ package body Ada.Strings.Unbounded is
begin
-- Check bounds
- if Before > SR.Last + 1 then
+ if Before - 1 > SR.Last then
raise Index_Error;
end if;
@@ -1152,9 +1170,12 @@ package body Ada.Strings.Unbounded is
-- Try to reuse existing shared string first
elsif Can_Be_Reused (SR, DL) then
- SR.Data (Before + New_Item'Length .. DL) :=
- SR.Data (Before .. SR.Last);
- SR.Data (Before .. Before + New_Item'Length - 1) := New_Item;
+ if Before <= SR.Last then
+ SR.Data (Before + New_Item'Length .. DL) :=
+ SR.Data (Before .. SR.Last);
+ end if;
+
+ SR.Data (Before .. Before - 1 + New_Item'Length) := New_Item;
SR.Last := DL;
-- Otherwise, allocate new shared string and fill it
@@ -1162,9 +1183,13 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL, DL / Growth_Factor);
DR.Data (1 .. Before - 1) := SR.Data (1 .. Before - 1);
- DR.Data (Before .. Before + New_Item'Length - 1) := New_Item;
- DR.Data (Before + New_Item'Length .. DL) :=
- SR.Data (Before .. SR.Last);
+ DR.Data (Before .. Before - 1 + New_Item'Length) := New_Item;
+
+ if Before <= SR.Last then
+ DR.Data (Before + New_Item'Length .. DL) :=
+ SR.Data (Before .. SR.Last);
+ end if;
+
DR.Last := DL;
Source.Reference := DR;
Unreference (SR);
@@ -1206,7 +1231,7 @@ package body Ada.Strings.Unbounded is
begin
-- Check bounds
- if Position > SR.Last + 1 then
+ if Position - 1 > SR.Last then
raise Index_Error;
end if;
@@ -1228,9 +1253,13 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL);
DR.Data (1 .. Position - 1) := SR.Data (1 .. Position - 1);
- DR.Data (Position .. Position + New_Item'Length - 1) := New_Item;
- DR.Data (Position + New_Item'Length .. DL) :=
- SR.Data (Position + New_Item'Length .. SR.Last);
+ DR.Data (Position .. Position - 1 + New_Item'Length) := New_Item;
+
+ if Position <= SR.Last - New_Item'Length then
+ DR.Data (Position + New_Item'Length .. DL) :=
+ SR.Data (Position + New_Item'Length .. SR.Last);
+ end if;
+
DR.Last := DL;
end if;
@@ -1249,11 +1278,11 @@ package body Ada.Strings.Unbounded is
begin
-- Bounds check
- if Position > SR.Last + 1 then
+ if Position - 1 > SR.Last then
raise Index_Error;
end if;
- DL := Integer'Max (SR.Last, Position + New_Item'Length - 1);
+ DL := Integer'Max (SR.Last, Sum (Position - 1, New_Item'Length));
-- Result is empty string, reuse empty shared string
@@ -1269,7 +1298,7 @@ package body Ada.Strings.Unbounded is
-- Try to reuse existing shared string
elsif Can_Be_Reused (SR, DL) then
- SR.Data (Position .. Position + New_Item'Length - 1) := New_Item;
+ SR.Data (Position .. Position - 1 + New_Item'Length) := New_Item;
SR.Last := DL;
-- Otherwise allocate new shared string and fill it
@@ -1277,9 +1306,13 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL);
DR.Data (1 .. Position - 1) := SR.Data (1 .. Position - 1);
- DR.Data (Position .. Position + New_Item'Length - 1) := New_Item;
- DR.Data (Position + New_Item'Length .. DL) :=
- SR.Data (Position + New_Item'Length .. SR.Last);
+ DR.Data (Position .. Position - 1 + New_Item'Length) := New_Item;
+
+ if Position <= SR.Last - New_Item'Length then
+ DR.Data (Position + New_Item'Length .. DL) :=
+ SR.Data (Position + New_Item'Length .. SR.Last);
+ end if;
+
DR.Last := DL;
Source.Reference := DR;
Unreference (SR);
@@ -1365,15 +1398,14 @@ package body Ada.Strings.Unbounded is
begin
-- Check bounds
- if Low > SR.Last + 1 then
+ if Low - 1 > SR.Last then
raise Index_Error;
end if;
-- Do replace operation when removed slice is not empty
if High >= Low then
- DL := Sum (SR.Last,
- By'Length + Low - Integer'Min (High, SR.Last) - 1);
+ DL := Sum (Low - 1 + Integer'Max (SR.Last - High, 0), By'Length);
-- This is the number of characters remaining in the string after
-- replacing the slice.
@@ -1387,8 +1419,13 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL);
DR.Data (1 .. Low - 1) := SR.Data (1 .. Low - 1);
- DR.Data (Low .. Low + By'Length - 1) := By;
- DR.Data (Low + By'Length .. DL) := SR.Data (High + 1 .. SR.Last);
+ DR.Data (Low .. Low - 1 + By'Length) := By;
+
+ if High < SR.Last then
+ DR.Data (Low + By'Length .. DL) :=
+ SR.Data (High + 1 .. SR.Last);
+ end if;
+
DR.Last := DL;
end if;
@@ -1414,14 +1451,14 @@ package body Ada.Strings.Unbounded is
begin
-- Bounds check
- if Low > SR.Last + 1 then
+ if Low - 1 > SR.Last then
raise Index_Error;
end if;
-- Do replace operation only when replaced slice is not empty
if High >= Low then
- DL := By'Length + SR.Last + Low - Integer'Min (High, SR.Last) - 1;
+ DL := Sum (Low - 1 + Integer'Max (SR.Last - High, 0), By'Length);
-- This is the number of characters remaining in the string after
-- replacing the slice.
@@ -1434,8 +1471,12 @@ package body Ada.Strings.Unbounded is
-- Try to reuse existing shared string
elsif Can_Be_Reused (SR, DL) then
- SR.Data (Low + By'Length .. DL) := SR.Data (High + 1 .. SR.Last);
- SR.Data (Low .. Low + By'Length - 1) := By;
+ if High < SR.Last then
+ SR.Data (Low + By'Length .. DL) :=
+ SR.Data (High + 1 .. SR.Last);
+ end if;
+
+ SR.Data (Low .. Low - 1 + By'Length) := By;
SR.Last := DL;
-- Otherwise allocate new shared string and fill it
@@ -1443,8 +1484,13 @@ package body Ada.Strings.Unbounded is
else
DR := Allocate (DL);
DR.Data (1 .. Low - 1) := SR.Data (1 .. Low - 1);
- DR.Data (Low .. Low + By'Length - 1) := By;
- DR.Data (Low + By'Length .. DL) := SR.Data (High + 1 .. SR.Last);
+ DR.Data (Low .. Low - 1 + By'Length) := By;
+
+ if High < SR.Last then
+ DR.Data (Low + By'Length .. DL) :=
+ SR.Data (High + 1 .. SR.Last);
+ end if;
+
DR.Last := DL;
Source.Reference := DR;
Unreference (SR);
@@ -1509,7 +1555,7 @@ package body Ada.Strings.Unbounded is
begin
-- Note: test of High > Length is in accordance with AI95-00128
- if Low > SR.Last + 1 or else High > SR.Last then
+ if Low - 1 > SR.Last or else High > SR.Last then
raise Index_Error;
else
@@ -1521,7 +1567,7 @@ package body Ada.Strings.Unbounded is
-- Sum --
---------
- function Sum (Left : Natural; Right : Integer) return Natural is
+ function Sum (Left, Right : Natural) return Natural is
pragma Unsuppress (Overflow_Check);
begin
return Left + Right;
@@ -35,9 +35,14 @@
-- 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);
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
-- This package provides an implementation of Ada.Strings.Unbounded that uses
-- reference counts to implement copy on modification (rather than copy on
@@ -77,17 +82,26 @@ pragma Assertion_Policy (Pre => Ignore);
-- make objects of Unbounded_String thread-safe: an instance cannot be
-- accessed by several tasks simultaneously.
-with Ada.Strings.Maps;
+with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
private with Ada.Finalization;
private with System.Atomic_Counters;
+with Ada.Strings.Search;
private with Ada.Strings.Text_Buffers;
package Ada.Strings.Unbounded with
+ SPARK_Mode,
Initial_Condition => Length (Null_Unbounded_String) = 0,
Always_Terminates
is
pragma Preelaborate;
+ -- Contracts may call function Length in the prefix of attribute reference
+ -- to Old as in Length (Source)'Old. Allow this use.
+
+ pragma Unevaluated_Use_Of_Old (Allow);
+
+ subtype String_1 is String (1 .. <>) with Ghost; -- Type used in contracts
+
type Unbounded_String is private with
Default_Initial_Condition => Length (Unbounded_String) = 0;
pragma Preelaborable_Initialization (Unbounded_String);
@@ -99,7 +113,7 @@ is
type String_Access is access all String;
- procedure Free (X : in out String_Access);
+ procedure Free (X : in out String_Access) with SPARK_Mode => Off;
--------------------------------------------------------
-- Conversion, Concatenation, and Selection Functions --
@@ -108,7 +122,8 @@ is
function To_Unbounded_String
(Source : String) return Unbounded_String
with
- Post => To_String (To_Unbounded_String'Result) = Source,
+ Post => To_String (To_Unbounded_String'Result) = Source
+ and then Length (To_Unbounded_String'Result) = Source'Length,
Global => null;
function To_Unbounded_String
@@ -136,7 +151,8 @@ is
New_Item : Unbounded_String)
with
Pre => Length (New_Item) <= Natural'Last - Length (Source),
- Post => Length (Source) = Length (Source)'Old + Length (New_Item),
+ Post =>
+ To_String (Source) = To_String (Source)'Old & To_String (New_Item),
Global => null;
procedure Append
@@ -144,7 +160,7 @@ is
New_Item : String)
with
Pre => New_Item'Length <= Natural'Last - Length (Source),
- Post => Length (Source) = Length (Source)'Old + New_Item'Length,
+ Post => To_String (Source) = To_String (Source)'Old & New_Item,
Global => null;
procedure Append
@@ -152,7 +168,7 @@ is
New_Item : Character)
with
Pre => Length (Source) < Natural'Last,
- Post => Length (Source) = Length (Source)'Old + 1,
+ Post => To_String (Source) = To_String (Source)'Old & New_Item,
Global => null;
function "&"
@@ -160,7 +176,7 @@ is
Right : Unbounded_String) return Unbounded_String
with
Pre => Length (Right) <= Natural'Last - Length (Left),
- Post => Length ("&"'Result) = Length (Left) + Length (Right),
+ Post => To_String ("&"'Result) = To_String (Left) & To_String (Right),
Global => null;
function "&"
@@ -168,7 +184,7 @@ is
Right : String) return Unbounded_String
with
Pre => Right'Length <= Natural'Last - Length (Left),
- Post => Length ("&"'Result) = Length (Left) + Right'Length,
+ Post => To_String ("&"'Result) = To_String (Left) & Right,
Global => null;
function "&"
@@ -176,7 +192,7 @@ is
Right : Unbounded_String) return Unbounded_String
with
Pre => Left'Length <= Natural'Last - Length (Right),
- Post => Length ("&"'Result) = Left'Length + Length (Right),
+ Post => To_String ("&"'Result) = String_1 (Left) & To_String (Right),
Global => null;
function "&"
@@ -184,7 +200,7 @@ is
Right : Character) return Unbounded_String
with
Pre => Length (Left) < Natural'Last,
- Post => Length ("&"'Result) = Length (Left) + 1,
+ Post => To_String ("&"'Result) = To_String (Left) & Right,
Global => null;
function "&"
@@ -192,7 +208,7 @@ is
Right : Unbounded_String) return Unbounded_String
with
Pre => Length (Right) < Natural'Last,
- Post => Length ("&"'Result) = Length (Right) + 1,
+ Post => To_String ("&"'Result) = Left & To_String (Right),
Global => null;
function Element
@@ -209,7 +225,8 @@ is
By : Character)
with
Pre => Index <= Length (Source),
- Post => Length (Source) = Length (Source)'Old,
+ Post =>
+ To_String (Source) = (To_String (Source)'Old with delta Index => By),
Global => null;
function Slice
@@ -218,7 +235,9 @@ is
High : Natural) return String
with
Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
- Post => Slice'Result'Length = Natural'Max (0, High - Low + 1),
+ Post => Slice'Result'First = Low
+ and then Slice'Result'Last = High
+ and then Slice'Result = To_String (Source) (Low .. High),
Global => null;
function Unbounded_Slice
@@ -228,7 +247,7 @@ is
with
Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
Post =>
- Length (Unbounded_Slice'Result) = Natural'Max (0, High - Low + 1),
+ To_String (Unbounded_Slice'Result) = To_String (Source) (Low .. High),
Global => null;
pragma Ada_05 (Unbounded_Slice);
@@ -239,7 +258,7 @@ is
High : Natural)
with
Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
- Post => Length (Target) = Natural'Max (0, High - Low + 1),
+ Post => To_String (Target) = To_String (Source) (Low .. High),
Global => null;
pragma Ada_05 (Unbounded_Slice);
@@ -268,72 +287,84 @@ is
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
+ Post => "<"'Result = (To_String (Left) < To_String (Right)),
Global => null;
function "<"
(Left : Unbounded_String;
Right : String) return Boolean
with
+ Post => "<"'Result = (To_String (Left) < Right),
Global => null;
function "<"
(Left : String;
Right : Unbounded_String) return Boolean
with
+ Post => "<"'Result = (Left < To_String (Right)),
Global => null;
function "<="
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
+ Post => "<="'Result = (To_String (Left) <= To_String (Right)),
Global => null;
function "<="
(Left : Unbounded_String;
Right : String) return Boolean
with
+ Post => "<="'Result = (To_String (Left) <= Right),
Global => null;
function "<="
(Left : String;
Right : Unbounded_String) return Boolean
with
+ Post => "<="'Result = (Left <= To_String (Right)),
Global => null;
function ">"
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
+ Post => ">"'Result = (To_String (Left) > To_String (Right)),
Global => null;
function ">"
(Left : Unbounded_String;
Right : String) return Boolean
with
+ Post => ">"'Result = (To_String (Left) > Right),
Global => null;
function ">"
(Left : String;
Right : Unbounded_String) return Boolean
with
+ Post => ">"'Result = (Left > To_String (Right)),
Global => null;
function ">="
(Left : Unbounded_String;
Right : Unbounded_String) return Boolean
with
+ Post => ">="'Result = (To_String (Left) >= To_String (Right)),
Global => null;
function ">="
(Left : Unbounded_String;
Right : String) return Boolean
with
+ Post => ">="'Result = (To_String (Left) >= Right),
Global => null;
function ">="
(Left : String;
Right : Unbounded_String) return Boolean
with
+ Post => ">="'Result = (Left >= To_String (Right)),
Global => null;
------------------------
@@ -346,8 +377,52 @@ is
Going : Direction := Forward;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
with
- Pre => Pattern'Length /= 0,
- Global => null;
+ Pre => Pattern'Length > 0,
+ Post => Index'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Length (Source) = 0
+ =>
+ Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Length (Source) > 0
+ and then
+ (for some J in 1 .. Length (Source) - (Pattern'Length - 1) =>
+ Search.Match (To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Index'Result in 1 .. Length (Source) - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (To_String (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 1 .. Length (Source) =>
+ (if (if Going = Forward
+ then J <= Index'Result - 1
+ else J - 1 in Index'Result
+ .. Length (Source) - Pattern'Length)
+ then not (Search.Match
+ (To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
+ Global => null;
function Index
(Source : Unbounded_String;
@@ -355,8 +430,52 @@ is
Going : Direction := Forward;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre => Pattern'Length /= 0,
- Global => null;
+ Pre => Pattern'Length /= 0 and then Mapping /= null,
+ Post => Index'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Length (Source) = 0
+ =>
+ Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Length (Source) > 0
+ and then
+ (for some J in 1 .. Length (Source) - (Pattern'Length - 1) =>
+ Search.Match (To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Index'Result in 1 .. Length (Source) - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (To_String (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 1 .. Length (Source) =>
+ (if (if Going = Forward
+ then J <= Index'Result - 1
+ else J - 1 in Index'Result
+ .. Length (Source) - Pattern'Length)
+ then not (Search.Match
+ (To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
+ Global => null;
function Index
(Source : Unbounded_String;
@@ -364,7 +483,43 @@ is
Test : Membership := Inside;
Going : Direction := Forward) return Natural
with
- Global => null;
+ Post => Index'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If no character of Source satisfies the property Test on Set,
+ -- then 0 is returned.
+
+ ((for all C of To_String (Source) =>
+ (Test = Inside) /= 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 1 .. Length (Source)
+
+ -- The character at the returned index satisfies the property
+ -- Test on Set.
+
+ and then
+ (Test = Inside) =
+ Maps.Is_In (Element (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 1 .. Length (Source) =>
+ (if J /= Index'Result
+ and then (J < Index'Result) = (Going = Forward)
+ then (Test = Inside)
+ /= Maps.Is_In (Element (Source, J), Set)))),
+ Global => null;
function Index
(Source : Unbounded_String;
@@ -373,9 +528,60 @@ is
Going : Direction := Forward;
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
with
- Pre => (if Length (Source) /= 0 then From <= Length (Source))
- and then Pattern'Length /= 0,
- Global => null;
+ Pre =>
+ (if Length (Source) /= 0 then From <= Length (Source))
+ and then Pattern'Length /= 0,
+ Post => Index'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Length (Source) = 0
+ =>
+ Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Length (Source) > 0
+ and then
+ (for some J in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Length (Source) else From)
+ - (Pattern'Length - 1) =>
+ Search.Match (To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Index'Result in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Length (Source) else From)
+ - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (To_String (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 1 .. Length (Source) =>
+ (if (if Going = Forward
+ then J in From .. Index'Result - 1
+ else J - 1 in Index'Result
+ .. From - Pattern'Length)
+ then not (Search.Match
+ (To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
+ Global => null;
pragma Ada_05 (Index);
function Index
@@ -385,9 +591,61 @@ is
Going : Direction := Forward;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre => (if Length (Source) /= 0 then From <= Length (Source))
- and then Pattern'Length /= 0,
- Global => null;
+ Pre =>
+ (if Length (Source) /= 0 then From <= Length (Source))
+ and then Pattern'Length /= 0
+ and then Mapping /= null,
+ Post => Index'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Length (Source) = 0
+ =>
+ Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Length (Source) > 0
+ and then
+ (for some J in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Length (Source) else From)
+ - (Pattern'Length - 1) =>
+ Search.Match (To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Index'Result in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Length (Source) else From)
+ - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (To_String (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 1 .. Length (Source) =>
+ (if (if Going = Forward
+ then J in From .. Index'Result - 1
+ else J - 1 in Index'Result
+ .. From - Pattern'Length)
+ then not (Search.Match
+ (To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Index'Result = 0),
+ Global => null;
pragma Ada_05 (Index);
function Index
@@ -397,23 +655,147 @@ is
Test : Membership := Inside;
Going : Direction := Forward) return Natural
with
- Pre => (if Length (Source) /= 0 then From <= Length (Source)),
- Global => null;
+ Pre =>
+ (if Length (Source) /= 0 then From <= Length (Source)),
+ Post => Index'Result <= Length (Source),
+ 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.
+
+ (Length (Source) = 0
+ or else
+ (for all J in 1 .. Length (Source) =>
+ (if J = From or else (J > From) = (Going = Forward) then
+ (Test = Inside) /= Maps.Is_In (Element (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 1 .. Length (Source)
+ 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) =
+ Maps.Is_In (Element (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 1 .. Length (Source) =>
+ (if J /= Index'Result
+ and then (J < Index'Result) = (Going = Forward)
+ and then (J = From
+ or else (J > From) = (Going = Forward))
+ then (Test = Inside)
+ /= Maps.Is_In (Element (Source, J), Set)))),
+ Global => null;
pragma Ada_05 (Index);
function Index_Non_Blank
(Source : Unbounded_String;
Going : Direction := Forward) return Natural
with
- Global => null;
+ Post => Index_Non_Blank'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If all characters of Source are Space characters, then 0 is
+ -- returned.
+
+ ((for all C of To_String (Source) => C = ' ')
+ =>
+ Index_Non_Blank'Result = 0,
+
+ -- Otherwise, an index in the range of Source is returned
+
+ others
+ =>
+ -- The result is in the range of Source
+
+ Index_Non_Blank'Result in 1 .. Length (Source)
+
+ -- The character at the returned index is not a Space character
+
+ and then Element (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 1 .. Length (Source) =>
+ (if J /= Index_Non_Blank'Result
+ and then
+ (J < Index_Non_Blank'Result) = (Going = Forward)
+ then Element (Source, J) = ' '))),
+ Global => null;
function Index_Non_Blank
(Source : Unbounded_String;
From : Positive;
Going : Direction := Forward) return Natural
with
- Pre => (if Length (Source) /= 0 then From <= Length (Source)),
- Global => null;
+ Pre =>
+ (if Length (Source) /= 0 then From <= Length (Source)),
+ Post => Index_Non_Blank'Result <= Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, or all characters of the
+ -- considered slice of Source are Space characters, then 0
+ -- is returned.
+
+ (Length (Source) = 0
+ or else
+ (for all J in 1 .. Length (Source) =>
+ (if J = From or else (J > From) = (Going = Forward) then
+ Element (Source, J) = ' '))
+ =>
+ Index_Non_Blank'Result = 0,
+
+ -- Otherwise, an index in the considered range of Source is
+ -- returned.
+
+ others
+ =>
+ -- The result is in the considered range of Source
+
+ Index_Non_Blank'Result in 1 .. Length (Source)
+ 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 Element (Source, Index_Non_Blank'Result) /= ' '
+
+ -- The result is the smallest or largest index which isn't a
+ -- Space character, respectively when Going = Forward and Going
+ -- = Backward.
+
+ and then
+ (for all J in 1 .. Length (Source) =>
+ (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 Element (Source, J) = ' '))),
+ Global => null;
pragma Ada_05 (Index_Non_Blank);
function Count
@@ -429,7 +811,7 @@ is
Pattern : String;
Mapping : Maps.Character_Mapping_Function) return Natural
with
- Pre => Pattern'Length /= 0,
+ Pre => Pattern'Length /= 0 and then Mapping /= null,
Global => null;
function Count
@@ -446,8 +828,53 @@ is
First : out Positive;
Last : out Natural)
with
- Pre => (if Length (Source) /= 0 then From <= Length (Source)),
- Global => null;
+ Pre =>
+ (if Length (Source) /= 0 then From <= Length (Source)),
+ 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.
+
+ (Length (Source) = 0
+ or else
+ (for all J in From .. Length (Source) =>
+ (Test = Inside) /= Maps.Is_In (Element (Source, J), 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 .. Length (Source)
+ and then Last in First .. Length (Source)
+
+ -- No character between From and First satisfies the property
+ -- Test on Set.
+
+ and then
+ (for all J in From .. First - 1 =>
+ (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+
+ -- All characters between First and Last satisfy the property
+ -- Test on Set.
+
+ and then
+ (for all J in First .. Last =>
+ (Test = Inside) = Maps.Is_In (Element (Source, J), 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 < Length (Source)
+ then
+ (Test = Inside)
+ /= Maps.Is_In (Element (Source, Last + 1), Set))),
+ Global => null;
pragma Ada_2012 (Find_Token);
procedure Find_Token
@@ -457,7 +884,51 @@ is
First : out Positive;
Last : out Natural)
with
- Global => null;
+ 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 1 and Last is set to 0.
+
+ (Length (Source) = 0
+ or else
+ (for all J in 1 .. Length (Source) =>
+ (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+ =>
+ First = 1 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 1 .. Length (Source)
+ and then Last in First .. Length (Source)
+
+ -- No character between 1 and First satisfies the property Test
+ -- on Set.
+
+ and then
+ (for all J in 1 .. First - 1 =>
+ (Test = Inside) /= Maps.Is_In (Element (Source, J), Set))
+
+ -- All characters between First and Last satisfy the property
+ -- Test on Set.
+
+ and then
+ (for all J in First .. Last =>
+ (Test = Inside) = Maps.Is_In (Element (Source, J), 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 < Length (Source)
+ then
+ (Test = Inside)
+ /= Maps.Is_In (Element (Source, Last + 1), Set))),
+ Global => null;
------------------------------------
-- String Translation Subprograms --
@@ -467,28 +938,44 @@ is
(Source : Unbounded_String;
Mapping : Maps.Character_Mapping) return Unbounded_String
with
- Post => Length (Translate'Result) = Length (Source),
+ Post => Length (Translate'Result) = Length (Source)
+ and then
+ (for all K in 1 .. Length (Source) =>
+ Element (Translate'Result, K) =
+ Ada.Strings.Maps.Value (Mapping, Element (Source, K))),
Global => null;
procedure Translate
(Source : in out Unbounded_String;
Mapping : Maps.Character_Mapping)
with
- Post => Length (Source) = Length (Source)'Old,
+ Post => Length (Source) = Length (Source)'Old
+ and then
+ (for all K in 1 .. Length (Source) =>
+ Element (Source, K) =
+ Ada.Strings.Maps.Value (Mapping, To_String (Source)'Old (K))),
Global => null;
function Translate
(Source : Unbounded_String;
Mapping : Maps.Character_Mapping_Function) return Unbounded_String
with
- Post => Length (Translate'Result) = Length (Source),
+ Pre => Mapping /= null,
+ Post => Length (Translate'Result) = Length (Source)
+ and then
+ (for all K in 1 .. Length (Source) =>
+ Element (Translate'Result, K) = Mapping (Element (Source, K))),
Global => null;
procedure Translate
(Source : in out Unbounded_String;
Mapping : Maps.Character_Mapping_Function)
with
- Post => Length (Source) = Length (Source)'Old,
+ Pre => Mapping /= null,
+ Post => Length (Source) = Length (Source)'Old
+ and then
+ (for all K in 1 .. Length (Source) =>
+ Element (Source, K) = Mapping (To_String (Source)'Old (K))),
Global => null;
---------------------------------------
@@ -506,14 +993,66 @@ is
and then (if High >= Low
then Low - 1
<= Natural'Last - By'Length
- - Natural'Max (Length (Source) - High, 0)
+ - Integer'Max (Length (Source) - High, 0)
else Length (Source) <= Natural'Last - By'Length),
Contract_Cases =>
+
+ -- If High >= Low, when considering the application of To_String to
+ -- convert an Unbounded_String into String, then the returned string
+ -- comprises Source (Source'First .. Low - 1) & By
+ -- & Source(High + 1 .. Source'Last).
+
(High >= Low =>
+
+ -- Length of the returned string
+
Length (Replace_Slice'Result)
- = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+ = Low - 1 + By'Length + Integer'Max (Length (Source) - High, 0)
+
+ -- Elements starting at Low are replaced by elements of By
+
+ and then
+ Slice (Replace_Slice'Result, 1, Low - 1) =
+ Slice (Source, 1, Low - 1)
+ and then
+ Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By
+
+ -- When there are remaining characters after the replaced slice,
+ -- they are appended to the result.
+
+ and then
+ (if High < Length (Source)
+ then
+ Slice (Replace_Slice'Result,
+ Low + By'Length, Length (Replace_Slice'Result)) =
+ Slice (Source, High + 1, Length (Source))),
+
+ -- If High < Low, then the returned string is
+ -- Insert (Source, Before => Low, New_Item => By).
+
others =>
- Length (Replace_Slice'Result) = Length (Source)'Old + By'Length),
+
+ -- Length of the returned string
+
+ Length (Replace_Slice'Result) = Length (Source) + By'Length
+
+ -- Elements of By are inserted after the element at Low
+
+ and then
+ Slice (Replace_Slice'Result, 1, Low - 1) =
+ Slice (Source, 1, Low - 1)
+ and then
+ Slice (Replace_Slice'Result, Low, Low - 1 + By'Length) = By
+
+ -- When there are remaining characters after Low in Source, they
+ -- are appended to the result.
+
+ and then
+ (if Low < Length (Source)
+ then
+ Slice (Replace_Slice'Result,
+ Low + By'Length, Length (Replace_Slice'Result)) =
+ Slice (Source, Low, Length (Source)))),
Global => null;
procedure Replace_Slice
@@ -530,11 +1069,61 @@ is
- Natural'Max (Length (Source) - High, 0)
else Length (Source) <= Natural'Last - By'Length),
Contract_Cases =>
+
+ -- If High >= Low, when considering the application of To_String to
+ -- convert an Unbounded_String into String, then the returned string
+ -- comprises Source (Source'First .. Low - 1) & By
+ -- & Source(High + 1 .. Source'Last).
+
(High >= Low =>
+
+ -- Length of the returned string
+
Length (Source)
- = Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High, 0),
+ = Low - 1 + By'Length + Integer'Max (Length (Source)'Old - High, 0)
+
+ -- Elements starting at Low are replaced by elements of By
+
+ and then Slice (Source, 1, Low - 1) =
+ Slice (Source, 1, Low - 1)'Old
+ and then Slice (Source, Low, Low - 1 + By'Length) = By
+
+ -- When there are remaining characters after the replaced slice,
+ -- they are appended to the result.
+
+ and then
+ (if High < Length (Source)'Old
+ then Slice (Source, Low + By'Length, Length (Source)) =
+ Slice (Source,
+ -- Really "High + 1" but expressed with a conditional
+ -- repeating the above test so that the call to Slice
+ -- is valid on entry (under 'Old) even when the test
+ -- evaluates to False.
+ (if High < Length (Source) then High + 1 else 1),
+ Length (Source))'Old),
+
+ -- If High < Low, then the returned string is
+ -- Insert (Source, Before => Low, New_Item => By).
+
others =>
- Length (Source) = Length (Source)'Old + By'Length),
+
+ -- Length of the returned string
+
+ Length (Source) = Length (Source)'Old + By'Length
+
+ -- Elements of By are inserted after the element at Low
+
+ and then Slice (Source, 1, Low - 1) =
+ Slice (Source, 1, Low - 1)'Old
+ and then Slice (Source, Low, Low - 1 + By'Length) = By
+
+ -- When there are remaining characters after Low in Source, they
+ -- are appended to the result.
+
+ and then
+ (if Low < Length (Source)'Old
+ then Slice (Source, Low + By'Length, Length (Source)) =
+ Slice (Source, Low, Length (Source))'Old)),
Global => null;
function Insert
@@ -544,7 +1133,27 @@ is
with
Pre => Before - 1 <= Length (Source)
and then New_Item'Length <= Natural'Last - Length (Source),
- Post => Length (Insert'Result) = Length (Source) + New_Item'Length,
+ Post =>
+ -- Length of the returned string
+
+ Length (Insert'Result) = Length (Source) + New_Item'Length
+
+ -- Elements of New_Item are inserted after element at Before
+
+ and then
+ Slice (Insert'Result, 1, Before - 1) = Slice (Source, 1, Before - 1)
+ and then
+ Slice (Insert'Result, Before, Before - 1 + 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 <= Length (Source) then
+ Slice (Insert'Result, Before + New_Item'Length,
+ Length (Insert'Result)) =
+ Slice (Source, Before, Length (Source))),
Global => null;
procedure Insert
@@ -554,7 +1163,25 @@ is
with
Pre => Before - 1 <= Length (Source)
and then New_Item'Length <= Natural'Last - Length (Source),
- Post => Length (Source) = Length (Source)'Old + New_Item'Length,
+ Post =>
+ -- Length of the returned string
+
+ Length (Source) = Length (Source)'Old + New_Item'Length
+
+ -- Elements of New_Item are inserted after element at Before
+
+ and then
+ Slice (Source, 1, Before - 1) = Slice (Source, 1, Before - 1)'Old
+ and then
+ Slice (Source, Before, Before - 1 + 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 <= Length (Source)'Old then
+ Slice (Source, Before + New_Item'Length, Length (Source)) =
+ Slice (Source, Before, Length (Source))'Old),
Global => null;
function Overwrite
@@ -563,12 +1190,31 @@ is
New_Item : String) return Unbounded_String
with
Pre => Position - 1 <= Length (Source)
- and then (if New_Item'Length /= 0
- then
- New_Item'Length <= Natural'Last - (Position - 1)),
+ and then New_Item'Length <= Natural'Last - (Position - 1),
Post =>
- Length (Overwrite'Result)
- = Natural'Max (Length (Source), Position - 1 + New_Item'Length),
+ -- Length of the returned string
+
+ Length (Overwrite'Result) =
+ Integer'Max (Length (Source), Position - 1 + New_Item'Length)
+
+ -- Elements after Position are replaced by elements of New_Item
+
+ and then
+ Slice (Overwrite'Result, 1, Position - 1) =
+ Slice (Source, 1, Position - 1)
+ and then
+ Slice (Overwrite'Result, Position, Position - 1 + New_Item'Length) =
+ New_Item
+ and then
+ (if Position - 1 + New_Item'Length < Length (Source) then
+
+ -- There are some unchanged characters of Source remaining
+ -- after New_Item.
+
+ Slice (Overwrite'Result,
+ Position + New_Item'Length, Length (Source)) =
+ Slice (Source,
+ Position + New_Item'Length, Length (Source))),
Global => null;
procedure Overwrite
@@ -577,13 +1223,36 @@ is
New_Item : String)
with
Pre => Position - 1 <= Length (Source)
- and then (if New_Item'Length /= 0
- then
- New_Item'Length <= Natural'Last - (Position - 1)),
+ and then New_Item'Length <= Natural'Last - (Position - 1),
Post =>
- Length (Source)
- = Natural'Max (Length (Source)'Old, Position - 1 + New_Item'Length),
+ -- Length of the returned string
+
+ Length (Source) =
+ Integer'Max (Length (Source)'Old, Position - 1 + New_Item'Length)
+
+ -- Elements after Position are replaced by elements of New_Item
+ and then
+ Slice (Source, 1, Position - 1) = Slice (Source, 1, Position - 1)
+ and then
+ Slice (Source, Position, Position - 1 + New_Item'Length) = New_Item
+ and then
+ (if Position - 1 + New_Item'Length < Length (Source)'Old then
+
+ -- There are some unchanged characters of Source remaining
+ -- after New_Item.
+
+ Slice (Source,
+ Position + New_Item'Length, Length (Source)'Old) =
+ Slice (Source,
+ -- Really "Position + New_Item'Length" but expressed with
+ -- a conditional repeating the above test so that the
+ -- call to Slice is valid on entry (under 'Old) even
+ -- when the test evaluates to False.
+ (if Position - 1 + New_Item'Length < Length (Source)
+ then Position + New_Item'Length
+ else 1),
+ Length (Source))'Old),
Global => null;
function Delete
@@ -591,12 +1260,19 @@ is
From : Positive;
Through : Natural) return Unbounded_String
with
- Pre => (if Through <= From then From - 1 <= Length (Source)),
+ Pre => (if Through >= From then From - 1 <= Length (Source)),
Contract_Cases =>
(Through >= From =>
- Length (Delete'Result) = Length (Source) - (Through - From + 1),
+ Length (Delete'Result) =
+ From - 1 + Natural'Max (Length (Source) - Through, 0)
+ and then
+ Slice (Delete'Result, 1, From - 1) = Slice (Source, 1, From - 1)
+ and then
+ (if Through < Length (Source) then
+ Slice (Delete'Result, From, Length (Delete'Result)) =
+ Slice (Source, Through + 1, Length (Source))),
others =>
- Length (Delete'Result) = Length (Source)),
+ Delete'Result = Source),
Global => null;
procedure Delete
@@ -604,82 +1280,255 @@ is
From : Positive;
Through : Natural)
with
- Pre => (if Through <= From then From - 1 <= Length (Source)),
+ Pre => (if Through >= From then From - 1 <= Length (Source)),
Contract_Cases =>
(Through >= From =>
- Length (Source) = Length (Source)'Old - (Through - From + 1),
+ Length (Source) =
+ From - 1 + Natural'Max (Length (Source)'Old - Through, 0)
+ and then
+ Slice (Source, 1, From - 1) =
+ To_String (Source)'Old (1 .. From - 1)
+ and then
+ (if Through < Length (Source) then
+ Slice (Source, From, Length (Source)) =
+ To_String (Source)'Old (Through + 1 .. Length (Source)'Old)),
others =>
- Length (Source) = Length (Source)'Old),
+ To_String (Source) = To_String (Source)'Old),
Global => null;
function Trim
(Source : Unbounded_String;
Side : Trim_End) return Unbounded_String
with
- Post => Length (Trim'Result) <= Length (Source),
- Global => null;
+ Contract_Cases =>
+ -- If all characters in Source are Space, the returned string is
+ -- empty.
+
+ ((for all C of To_String (Source) => C = ' ')
+ =>
+ Length (Trim'Result) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ (if Side = Right then 1
+ else Index_Non_Blank (Source, Forward));
+ High : constant Positive :=
+ (if Side = Left then Length (Source)
+ else Index_Non_Blank (Source, Backward));
+ begin
+ To_String (Trim'Result) = Slice (Source, Low, High))),
+ Global => null;
procedure Trim
(Source : in out Unbounded_String;
Side : Trim_End)
with
- Post => Length (Source) <= Length (Source)'Old,
- Global => null;
+ Contract_Cases =>
+ -- If all characters in Source are Space, the returned string is
+ -- empty.
+
+ ((for all C of To_String (Source) => C = ' ')
+ =>
+ Length (Source) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ (if Side = Right then 1
+ else Index_Non_Blank (Source, Forward)'Old);
+ High : constant Positive :=
+ (if Side = Left then Length (Source)'Old
+ else Index_Non_Blank (Source, Backward)'Old);
+ begin
+ To_String (Source) = To_String (Source)'Old (Low .. High))),
+ Global => null;
function Trim
(Source : Unbounded_String;
Left : Maps.Character_Set;
Right : Maps.Character_Set) return Unbounded_String
with
- Post => Length (Trim'Result) <= Length (Source),
- Global => null;
+ Contract_Cases =>
+ -- If all characters in Source are contained in one of the sets Left
+ -- or Right, then the returned string is empty.
+
+ ((for all C of To_String (Source) => Maps.Is_In (C, Left))
+ or else
+ (for all C of To_String (Source) => Maps.Is_In (C, Right))
+ =>
+ Length (Trim'Result) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ Index (Source, Left, Outside, Forward);
+ High : constant Positive :=
+ Index (Source, Right, Outside, Backward);
+ begin
+ To_String (Trim'Result) = Slice (Source, Low, High))),
+ Global => null;
procedure Trim
(Source : in out Unbounded_String;
Left : Maps.Character_Set;
Right : Maps.Character_Set)
with
- Post => Length (Source) <= Length (Source)'Old,
- Global => null;
+ Contract_Cases =>
+ -- If all characters in Source are contained in one of the sets Left
+ -- or Right, then the returned string is empty.
+
+ ((for all C of To_String (Source) => Maps.Is_In (C, Left))
+ or else
+ (for all C of To_String (Source) => Maps.Is_In (C, Right))
+ =>
+ Length (Source) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ Index (Source, Left, Outside, Forward)'Old;
+ High : constant Positive :=
+ Index (Source, Right, Outside, Backward)'Old;
+ begin
+ To_String (Source) = To_String (Source)'Old (Low .. High))),
+ Global => null;
function Head
(Source : Unbounded_String;
Count : Natural;
Pad : Character := Space) return Unbounded_String
with
- Post => Length (Head'Result) = Count,
- Global => null;
+ Post => Length (Head'Result) = Count,
+ Contract_Cases =>
+ (Count <= Length (Source)
+ =>
+ -- Source is cut
+
+ To_String (Head'Result) = Slice (Source, 1, Count),
+
+ others
+ =>
+ -- Source is followed by Pad characters
+
+ Slice (Head'Result, 1, Length (Source)) = To_String (Source)
+ and then
+ Slice (Head'Result, Length (Source) + 1, Count) =
+ [1 .. Count - Length (Source) => Pad]),
+ Global => null;
procedure Head
(Source : in out Unbounded_String;
Count : Natural;
Pad : Character := Space)
with
- Post => Length (Source) = Count,
- Global => null;
+ Post => Length (Source) = Count,
+ Contract_Cases =>
+ (Count <= Length (Source)
+ =>
+ -- Source is cut
+
+ To_String (Source) = Slice (Source, 1, Count),
+
+ others
+ =>
+ -- Source is followed by Pad characters
+
+ Slice (Source, 1, Length (Source)'Old) = To_String (Source)'Old
+ and then
+ Slice (Source, Length (Source)'Old + 1, Count) =
+ [1 .. Count - Length (Source)'Old => Pad]),
+ Global => null;
function Tail
(Source : Unbounded_String;
Count : Natural;
Pad : Character := Space) return Unbounded_String
with
- Post => Length (Tail'Result) = Count,
- Global => null;
+ Post => Length (Tail'Result) = Count,
+ Contract_Cases =>
+ (Count = 0
+ =>
+ True,
+
+ (Count in 1 .. Length (Source))
+ =>
+ -- Source is cut
+
+ To_String (Tail'Result) =
+ Slice (Source, Length (Source) - Count + 1, Length (Source)),
+
+ others
+ =>
+ -- Source is preceded by Pad characters
+
+ (if Length (Source) = 0 then
+ To_String (Tail'Result) = [1 .. Count => Pad]
+ else
+ Slice (Tail'Result, 1, Count - Length (Source)) =
+ [1 .. Count - Length (Source) => Pad]
+ and then
+ Slice (Tail'Result, Count - Length (Source) + 1, Count) =
+ To_String (Source))),
+ Global => null;
procedure Tail
(Source : in out Unbounded_String;
Count : Natural;
Pad : Character := Space)
with
- Post => Length (Source) = Count,
- Global => null;
+ Post => Length (Source) = Count,
+ Contract_Cases =>
+ (Count = 0
+ =>
+ True,
+
+ (Count in 1 .. Length (Source))
+ =>
+ -- Source is cut
+
+ To_String (Source) =
+ Slice (Source,
+ -- Really "Length (Source) - Count + 1" but expressed with a
+ -- conditional repeating the above guard so that the call to
+ -- Slice is valid on entry (under 'Old) even when the test
+ -- evaluates to False.
+ (if Count <= Length (Source) then Length (Source) - Count + 1
+ else 1),
+ Length (Source))'Old,
+
+ others
+ =>
+ -- Source is preceded by Pad characters
+
+ (if Length (Source)'Old = 0 then
+ To_String (Source) = [1 .. Count => Pad]
+ else
+ Slice (Source, 1, Count - Length (Source)'Old) =
+ [1 .. Count - Length (Source)'Old => Pad]
+ and then
+ Slice (Source, Count - Length (Source)'Old + 1, Count) =
+ To_String (Source)'Old)),
+ Global => null;
function "*"
(Left : Natural;
Right : Character) return Unbounded_String
with
Pre => Left <= Natural'Last,
- Post => Length ("*"'Result) = Left,
+ Post => To_String ("*"'Result) = [1 .. Left => Right],
Global => null;
function "*"
@@ -687,7 +1536,13 @@ is
Right : String) return Unbounded_String
with
Pre => (if Left /= 0 then Right'Length <= Natural'Last / Left),
- Post => Length ("*"'Result) = Left * Right'Length,
+ Post =>
+ Length ("*"'Result) = Left * Right'Length
+ and then
+ (if Right'Length > 0 then
+ (for all K in 1 .. Left * Right'Length =>
+ Element ("*"'Result, K) =
+ Right (Right'First + (K - 1) mod Right'Length))),
Global => null;
function "*"
@@ -695,10 +1550,18 @@ is
Right : Unbounded_String) return Unbounded_String
with
Pre => (if Left /= 0 then Length (Right) <= Natural'Last / Left),
- Post => Length ("*"'Result) = Left * Length (Right),
+ Post =>
+ Length ("*"'Result) = Left * Length (Right)
+ and then
+ (if Length (Right) > 0 then
+ (for all K in 1 .. Left * Length (Right) =>
+ Element ("*"'Result, K) =
+ Element (Right, 1 + (K - 1) mod Length (Right)))),
Global => null;
private
+ pragma SPARK_Mode (Off); -- Controlled types are not in SPARK
+
pragma Inline (Length);
package AF renames Ada.Finalization;