public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r12-3813] [Ada] Contracts written for the Ada.Strings.Bounded library
@ 2021-09-22 15:11 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2021-09-22 15:11 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:1647bc2a78b2182007f011ff0a43f872086ee512
commit r12-3813-g1647bc2a78b2182007f011ff0a43f872086ee512
Author: Pierre-Alexandre Bazin <bazin@adacore.com>
Date: Fri Jul 2 15:43:44 2021 +0200
[Ada] Contracts written for the Ada.Strings.Bounded library
gcc/ada/
* libgnat/a-strbou.adb: Turn SPARK_Mode on.
* libgnat/a-strbou.ads: Write contracts.
* libgnat/a-strfix.ads (Index): Fix grammar error in a comment.
* libgnat/a-strsea.ads (Index): Likewise.
* libgnat/a-strsup.adb: Rewrite the body to take into account
the new definition of Super_String using Relaxed_Initialization
and a predicate.
(Super_Replicate, Super_Translate, Times): Added loop
invariants, and ghost lemmas for Super_Replicate and Times.
(Super_Trim): Rewrite the body using search functions to
determine the cutting points.
(Super_Element, Super_Length, Super_Slice, Super_To_String):
Remove (now written as expression functions in a-strsup.ads).
* libgnat/a-strsup.ads: Added contracts.
(Super_Element, Super_Length, Super_Slice, Super_To_String):
Rewrite as expression functions.
Diff:
---
gcc/ada/libgnat/a-strbou.adb | 2 +-
gcc/ada/libgnat/a-strbou.ads | 2074 ++++++++++++++++++++++++++++++++----
gcc/ada/libgnat/a-strfix.ads | 6 +-
gcc/ada/libgnat/a-strsea.ads | 6 +-
gcc/ada/libgnat/a-strsup.adb | 1163 +++++++++++++--------
gcc/ada/libgnat/a-strsup.ads | 2383 ++++++++++++++++++++++++++++++++++++++++--
6 files changed, 4911 insertions(+), 723 deletions(-)
diff --git a/gcc/ada/libgnat/a-strbou.adb b/gcc/ada/libgnat/a-strbou.adb
index 61b3d73852d..01a2002673b 100644
--- a/gcc/ada/libgnat/a-strbou.adb
+++ b/gcc/ada/libgnat/a-strbou.adb
@@ -29,7 +29,7 @@
-- --
------------------------------------------------------------------------------
-package body Ada.Strings.Bounded is
+package body Ada.Strings.Bounded with SPARK_Mode is
package body Generic_Bounded_Length is
diff --git a/gcc/ada/libgnat/a-strbou.ads b/gcc/ada/libgnat/a-strbou.ads
index f0cf7b26052..b88e04935b1 100644
--- a/gcc/ada/libgnat/a-strbou.ads
+++ b/gcc/ada/libgnat/a-strbou.ads
@@ -33,25 +33,33 @@
-- --
------------------------------------------------------------------------------
--- Preconditions in this unit are meant for analysis only, not for run-time
--- checking, so that the expected exceptions are raised. This is enforced by
--- setting the corresponding assertion policy to Ignore.
-
-pragma Assertion_Policy (Pre => Ignore);
-
-with Ada.Strings.Maps;
+with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
with Ada.Strings.Superbounded;
+with Ada.Strings.Search;
-package Ada.Strings.Bounded is
+package Ada.Strings.Bounded with SPARK_Mode is
pragma Preelaborate;
generic
Max : Positive;
-- Maximum length of a Bounded_String
- package Generic_Bounded_Length with
- Initial_Condition => Length (Null_Bounded_String) = 0
+ package Generic_Bounded_Length with SPARK_Mode,
+ Initializes => (Null_Bounded_String => Max,
+ Max_Length => Max),
+ Initial_Condition => Length (Null_Bounded_String) = 0,
+ Abstract_State => null
is
+ -- Preconditions in this unit are meant for analysis only, not for
+ -- run-time checking, so that the expected exceptions are raised. This
+ -- is enforced by setting the corresponding assertion policy to Ignore.
+ -- Postconditions and contract cases should not be executed at runtime
+ -- as well, in order not to slow down the execution of these functions.
+
+ pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
Max_Length : constant Positive := Max;
@@ -73,14 +81,24 @@ package Ada.Strings.Bounded is
(Source : String;
Drop : Truncation := Error) return Bounded_String
with
- Pre => (if Source'Length > Max_Length then Drop /= Error),
- Post =>
- Length (To_Bounded_String'Result)
- = Natural'Min (Max_Length, Source'Length),
- Global => null;
+ Pre => (if Source'Length > Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Source'Length <= Max_Length
+ =>
+ To_String (To_Bounded_String'Result) = Source,
+
+ Source'Length > Max_Length and then Drop = Left
+ =>
+ To_String (To_Bounded_String'Result) =
+ Source (Source'Last - Max_Length + 1 .. Source'Last),
+
+ others -- Drop = Right
+ =>
+ To_String (To_Bounded_String'Result) =
+ Source (Source'First .. Source'First - 1 + Max_Length)),
+ Global => Max_Length;
function To_String (Source : Bounded_String) return String with
- Post => To_String'Result'Length = Length (Source),
Global => null;
procedure Set_Bounded_String
@@ -88,9 +106,22 @@ package Ada.Strings.Bounded is
Source : String;
Drop : Truncation := Error)
with
- Pre => (if Source'Length > Max_Length then Drop /= Error),
- Post => Length (Target) = Natural'Min (Max_Length, Source'Length),
- Global => null;
+ Pre => (if Source'Length > Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Source'Length <= Max_Length
+ =>
+ To_String (Target) = Source,
+
+ Source'Length > Max_Length and then Drop = Left
+ =>
+ To_String (Target) =
+ Source (Source'Last - Max_Length + 1 .. Source'Last),
+
+ others -- Drop = Right
+ =>
+ To_String (Target) =
+ Source (Source'First .. Source'First - 1 + Max_Length)),
+ Global => (Proof_In => Max_Length);
pragma Ada_05 (Set_Bounded_String);
function Append
@@ -98,138 +129,404 @@ package Ada.Strings.Bounded is
Right : Bounded_String;
Drop : Truncation := Error) return Bounded_String
with
- Pre =>
+ Pre =>
(if Length (Left) > Max_Length - Length (Right)
then Drop /= Error),
- Post =>
- Length (Append'Result)
- = Natural'Min (Max_Length, Length (Left) + Length (Right)),
- Global => null;
+ Contract_Cases =>
+ (Length (Left) <= Max_Length - Length (Right)
+ =>
+ Length (Append'Result) = Length (Left) + Length (Right)
+ and then
+ Slice (Append'Result, 1, Length (Left)) = To_String (Left)
+ and then
+ (if Length (Right) > 0 then
+ Slice (Append'Result,
+ Length (Left) + 1, Length (Append'Result)) =
+ To_String (Right)),
+
+ Length (Left) > Max_Length - Length (Right)
+ and then Drop = Strings.Left
+ =>
+ Length (Append'Result) = Max_Length
+ and then
+ (if Length (Right) < Max_Length then
+ Slice (Append'Result, 1, Max_Length - Length (Right)) =
+ Slice (Left,
+ Length (Left) - Max_Length + Length (Right) + 1,
+ Length (Left)))
+ and then
+ Slice (Append'Result,
+ Max_Length - Length (Right) + 1, Max_Length) =
+ To_String (Right),
+
+ others -- Drop = Right
+ =>
+ Length (Append'Result) = Max_Length
+ and then
+ Slice (Append'Result, 1, Length (Left)) = To_String (Left)
+ and then
+ (if Length (Left) < Max_Length then
+ Slice (Append'Result, Length (Left) + 1, Max_Length) =
+ Slice (Right, 1, Max_Length - Length (Left)))),
+ Global => (Proof_In => Max_Length);
function Append
(Left : Bounded_String;
Right : String;
Drop : Truncation := Error) return Bounded_String
with
- Pre =>
+ Pre =>
(if Right'Length > Max_Length - Length (Left)
then Drop /= Error),
- Post =>
- Length (Append'Result)
- = Natural'Min (Max_Length, Length (Left) + Right'Length),
- Global => null;
+ Contract_Cases =>
+ (Length (Left) <= Max_Length - Right'Length
+ =>
+ Length (Append'Result) = Length (Left) + Right'Length
+ and then
+ Slice (Append'Result, 1, Length (Left)) = To_String (Left)
+ and then
+ (if Right'Length > 0 then
+ Slice (Append'Result,
+ Length (Left) + 1, Length (Append'Result)) =
+ Right),
+
+ Length (Left) > Max_Length - Right'Length
+ and then Drop = Strings.Left
+ =>
+ Length (Append'Result) = Max_Length
+ and then
+ (if Right'Length < Max_Length then
+
+ -- The result is the end of Left followed by Right
+
+ Slice (Append'Result, 1, Max_Length - Right'Length) =
+ Slice (Left,
+ Length (Left) - Max_Length + Right'Length + 1,
+ Length (Left))
+ and then
+ Slice (Append'Result,
+ Max_Length - Right'Length + 1, Max_Length) =
+ Right
+ else
+ -- The result is the last Max_Length characters of Right
+
+ To_String (Append'Result) =
+ Right (Right'Last - Max_Length + 1 .. Right'Last)),
+
+ others -- Drop = Right
+ =>
+ Length (Append'Result) = Max_Length
+ and then
+ Slice (Append'Result, 1, Length (Left)) = To_String (Left)
+ and then
+ (if Length (Left) < Max_Length then
+ Slice (Append'Result, Length (Left) + 1, Max_Length) =
+ Right (Right'First
+ .. Max_Length - Length (Left) - 1 + Right'First))),
+ Global => (Proof_In => Max_Length);
function Append
(Left : String;
Right : Bounded_String;
Drop : Truncation := Error) return Bounded_String
with
- Pre =>
+ Pre =>
(if Left'Length > Max_Length - Length (Right)
then Drop /= Error),
- Post =>
- Length (Append'Result)
- = Natural'Min (Max_Length, Left'Length + Length (Right)),
- Global => null;
+ Contract_Cases =>
+ (Left'Length <= Max_Length - Length (Right)
+ =>
+ Length (Append'Result) = Left'Length + Length (Right)
+ and then Slice (Append'Result, 1, Left'Length) = Left
+ and then
+ (if Length (Right) > 0 then
+ Slice (Append'Result,
+ Left'Length + 1, Length (Append'Result)) =
+ To_String (Right)),
+
+ Left'Length > Max_Length - Length (Right)
+ and then Drop = Strings.Left
+ =>
+ Length (Append'Result) = Max_Length
+ and then
+ (if Length (Right) < Max_Length then
+ Slice (Append'Result, 1, Max_Length - Length (Right)) =
+ Left (Left'Last - Max_Length + Length (Right) + 1
+ .. Left'Last))
+ and then
+ Slice (Append'Result,
+ Max_Length - Length (Right) + 1, Max_Length) =
+ To_String (Right),
+
+ others -- Drop = Right
+ =>
+ Length (Append'Result) = Max_Length
+ and then
+ (if Left'Length < Max_Length then
+
+ -- The result is Left followed by the beginning of Right
+
+ Slice (Append'Result, 1, Left'Length) = Left
+ and then
+ Slice (Append'Result, Left'Length + 1, Max_Length) =
+ Slice (Right, 1, Max_Length - Left'Length)
+ else
+ -- The result is the first Max_Length characters of Left
+
+ To_String (Append'Result) =
+ Left (Left'First .. Max_Length - 1 + Left'First))),
+ Global => (Proof_In => Max_Length);
function Append
(Left : Bounded_String;
Right : Character;
Drop : Truncation := Error) return Bounded_String
with
- Pre => (if Length (Left) = Max_Length then Drop /= Error),
- Post =>
- Length (Append'Result)
- = Natural'Min (Max_Length, Length (Left) + 1),
- Global => null;
+ Pre => (if Length (Left) = Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Length (Left) < Max_Length
+ =>
+ Length (Append'Result) = Length (Left) + 1
+ and then
+ Slice (Append'Result, 1, Length (Left)) = To_String (Left)
+ and then Element (Append'Result, Length (Left) + 1) = Right,
+
+ Length (Left) = Max_Length and then Drop = Strings.Right
+ =>
+ Length (Append'Result) = Max_Length
+ and then To_String (Append'Result) = To_String (Left),
+
+ others -- Drop = Left
+ =>
+ Length (Append'Result) = Max_Length
+ and then
+ Slice (Append'Result, 1, Max_Length - 1) =
+ Slice (Left, 2, Max_Length)
+ and then Element (Append'Result, Max_Length) = Right),
+ Global => (Proof_In => Max_Length);
function Append
(Left : Character;
Right : Bounded_String;
Drop : Truncation := Error) return Bounded_String
with
- Pre => (if Length (Right) = Max_Length then Drop /= Error),
- Post =>
- Length (Append'Result)
- = Natural'Min (Max_Length, 1 + Length (Right)),
- Global => null;
+ Pre => (if Length (Right) = Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Length (Right) < Max_Length
+ =>
+ Length (Append'Result) = Length (Right) + 1
+ and then
+ Slice (Append'Result, 2, Length (Right) + 1) =
+ To_String (Right)
+ and then Element (Append'Result, 1) = Left,
+
+ Length (Right) = Max_Length and then Drop = Strings.Left
+ =>
+ Length (Append'Result) = Max_Length
+ and then To_String (Append'Result) = To_String (Right),
+
+ others -- Drop = Right
+ =>
+ Length (Append'Result) = Max_Length
+ and then
+ Slice (Append'Result, 2, Max_Length) =
+ Slice (Right, 1, Max_Length - 1)
+ and then Element (Append'Result, 1) = Left),
+ Global => (Proof_In => Max_Length);
procedure Append
(Source : in out Bounded_String;
New_Item : Bounded_String;
Drop : Truncation := Error)
with
- Pre =>
+ Pre =>
(if Length (Source) > Max_Length - Length (New_Item)
then Drop /= Error),
- Post =>
- Length (Source)
- = Natural'Min (Max_Length, Length (Source)'Old + Length (New_Item)),
- Global => null;
+ Contract_Cases =>
+ (Length (Source) <= Max_Length - Length (New_Item)
+ =>
+ Length (Source) = Length (Source'Old) + Length (New_Item)
+ and then
+ Slice (Source, 1, Length (Source'Old)) =
+ To_String (Source'Old)
+ and then
+ (if Length (New_Item) > 0 then
+ Slice (Source, Length (Source'Old) + 1, Length (Source)) =
+ To_String (New_Item)),
+
+ Length (Source) > Max_Length - Length (New_Item)
+ and then Drop = Left
+ =>
+ Length (Source) = Max_Length
+ and then
+ (if Length (New_Item) < Max_Length then
+ Slice (Source, 1, Max_Length - Length (New_Item)) =
+ Slice (Source'Old,
+ Length (Source'Old) - Max_Length + Length (New_Item)
+ + 1,
+ Length (Source'Old)))
+ and then
+ Slice (Source, Max_Length - Length (New_Item) + 1, Max_Length)
+ = To_String (New_Item),
+
+ others -- Drop = Right
+ =>
+ Length (Source) = Max_Length
+ and then
+ Slice (Source, 1, Length (Source'Old)) =
+ To_String (Source'Old)
+ and then
+ (if Length (Source'Old) < Max_Length then
+ Slice (Source, Length (Source'Old) + 1, Max_Length) =
+ Slice (New_Item, 1, Max_Length - Length (Source'Old)))),
+ Global => (Proof_In => Max_Length);
procedure Append
(Source : in out Bounded_String;
New_Item : String;
Drop : Truncation := Error)
with
- Pre =>
+ Pre =>
(if New_Item'Length > Max_Length - Length (Source)
then Drop /= Error),
- Post =>
- Length (Source)
- = Natural'Min (Max_Length, Length (Source)'Old + New_Item'Length),
- Global => null;
+ Contract_Cases =>
+ (Length (Source) <= Max_Length - New_Item'Length
+ =>
+ Length (Source) = Length (Source'Old) + New_Item'Length
+ and then
+ Slice (Source, 1, Length (Source'Old)) =
+ To_String (Source'Old)
+ and then
+ (if New_Item'Length > 0 then
+ Slice (Source, Length (Source'Old) + 1, Length (Source)) =
+ New_Item),
+
+ Length (Source) > Max_Length - New_Item'Length
+ and then Drop = Left
+ =>
+ Length (Source) = Max_Length
+ and then
+ (if New_Item'Length < Max_Length then
+
+ -- The result is the end of Source followed by New_Item
+
+ Slice (Source, 1, Max_Length - New_Item'Length) =
+ Slice (Source'Old,
+ Length (Source'Old) - Max_Length + New_Item'Length + 1,
+ Length (Source'Old))
+ and then
+ Slice (Source,
+ Max_Length - New_Item'Length + 1, Max_Length) =
+ New_Item
+ else
+ -- The result is the last Max_Length characters of
+ -- New_Item.
+
+ To_String (Source) = New_Item
+ (New_Item'Last - Max_Length + 1 .. New_Item'Last)),
+
+ others -- Drop = Right
+ =>
+ Length (Source) = Max_Length
+ and then
+ Slice (Source, 1, Length (Source'Old)) =
+ To_String (Source'Old)
+ and then
+ (if Length (Source'Old) < Max_Length then
+ Slice (Source, Length (Source'Old) + 1, Max_Length) =
+ New_Item (New_Item'First
+ .. Max_Length - Length (Source'Old) - 1
+ + New_Item'First))),
+ Global => (Proof_In => Max_Length);
procedure Append
(Source : in out Bounded_String;
New_Item : Character;
Drop : Truncation := Error)
with
- Pre => (if Length (Source) = Max_Length then Drop /= Error),
- Post =>
- Length (Source)
- = Natural'Min (Max_Length, Length (Source)'Old + 1),
- Global => null;
+ Pre => (if Length (Source) = Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Length (Source) < Max_Length
+ =>
+ Length (Source) = Length (Source'Old) + 1
+ and then
+ Slice (Source, 1, Length (Source'Old)) =
+ To_String (Source'Old)
+ and then Element (Source, Length (Source'Old) + 1) = New_Item,
+
+ Length (Source) = Max_Length and then Drop = Right
+ =>
+ Length (Source) = Max_Length
+ and then To_String (Source) = To_String (Source'Old),
+
+ others -- Drop = Left
+ =>
+ Length (Source) = Max_Length
+ and then
+ Slice (Source, 1, Max_Length - 1) =
+ Slice (Source'Old, 2, Max_Length)
+ and then Element (Source, Max_Length) = New_Item),
+ Global => (Proof_In => Max_Length);
function "&"
(Left : Bounded_String;
Right : Bounded_String) return Bounded_String
with
Pre => Length (Left) <= Max_Length - Length (Right),
- Post => Length ("&"'Result) = Length (Left) + Length (Right),
- Global => null;
+ Post => Length ("&"'Result) = Length (Left) + Length (Right)
+ and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
+ and then
+ (if Length (Right) > 0 then
+ Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) =
+ To_String (Right)),
+ Global => (Proof_In => Max_Length);
function "&"
(Left : Bounded_String;
Right : String) return Bounded_String
with
Pre => Right'Length <= Max_Length - Length (Left),
- Post => Length ("&"'Result) = Length (Left) + Right'Length,
- Global => null;
+ Post => Length ("&"'Result) = Length (Left) + Right'Length
+ and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
+ and then
+ (if Right'Length > 0 then
+ Slice ("&"'Result, Length (Left) + 1, Length ("&"'Result)) =
+ Right),
+ Global => (Proof_In => Max_Length);
function "&"
(Left : String;
Right : Bounded_String) return Bounded_String
with
Pre => Left'Length <= Max_Length - Length (Right),
- Post => Length ("&"'Result) = Left'Length + Length (Right),
- Global => null;
+ Post => Length ("&"'Result) = Left'Length + Length (Right)
+ and then Slice ("&"'Result, 1, Left'Length) = Left
+ and then
+ (if Length (Right) > 0 then
+ Slice ("&"'Result, Left'Length + 1, Length ("&"'Result)) =
+ To_String (Right)),
+ Global => (Proof_In => Max_Length);
function "&"
(Left : Bounded_String;
Right : Character) return Bounded_String
with
Pre => Length (Left) < Max_Length,
- Post => Length ("&"'Result) = Length (Left) + 1,
- Global => null;
+ Post => Length ("&"'Result) = Length (Left) + 1
+ and then Slice ("&"'Result, 1, Length (Left)) = To_String (Left)
+ and then Element ("&"'Result, Length (Left) + 1) = Right,
+ Global => (Proof_In => Max_Length);
function "&"
(Left : Character;
Right : Bounded_String) return Bounded_String
with
Pre => Length (Right) < Max_Length,
- Post => Length ("&"'Result) = 1 + Length (Right),
- Global => null;
+ Post => Length ("&"'Result) = 1 + Length (Right)
+ and then Element ("&"'Result, 1) = Left
+ and then
+ Slice ("&"'Result, 2, Length ("&"'Result)) = To_String (Right),
+ Global => (Proof_In => Max_Length);
function Element
(Source : Bounded_String;
@@ -244,7 +541,10 @@ package Ada.Strings.Bounded is
By : Character)
with
Pre => Index <= Length (Source),
- Post => Length (Source) = Length (Source)'Old,
+ Post => Length (Source) = Length (Source'Old)
+ and then (for all K in 1 .. Length (Source) =>
+ Element (Source, K) =
+ (if K = Index then By else Element (Source'Old, K))),
Global => null;
function Slice
@@ -253,7 +553,6 @@ package Ada.Strings.Bounded 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),
Global => null;
function Bounded_Slice
@@ -262,8 +561,7 @@ package Ada.Strings.Bounded is
High : Natural) return Bounded_String
with
Pre => Low - 1 <= Length (Source) and then High <= Length (Source),
- Post =>
- Length (Bounded_Slice'Result) = Natural'Max (0, High - Low + 1),
+ Post => To_String (Bounded_Slice'Result) = Slice (Source, Low, High),
Global => null;
pragma Ada_05 (Bounded_Slice);
@@ -274,7 +572,7 @@ package Ada.Strings.Bounded 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) = Slice (Source, Low, High),
Global => null;
pragma Ada_05 (Bounded_Slice);
@@ -282,90 +580,105 @@ package Ada.Strings.Bounded is
(Left : Bounded_String;
Right : Bounded_String) return Boolean
with
+ Post => "="'Result = (To_String (Left) = To_String (Right)),
Global => null;
function "="
(Left : Bounded_String;
Right : String) return Boolean
with
+ Post => "="'Result = (To_String (Left) = Right),
Global => null;
function "="
(Left : String;
Right : Bounded_String) return Boolean
with
+ Post => "="'Result = (Left = To_String (Right)),
Global => null;
function "<"
(Left : Bounded_String;
Right : Bounded_String) return Boolean
with
+ Post => "<"'Result = (To_String (Left) < To_String (Right)),
Global => null;
function "<"
(Left : Bounded_String;
Right : String) return Boolean
with
+ Post => "<"'Result = (To_String (Left) < Right),
Global => null;
function "<"
(Left : String;
Right : Bounded_String) return Boolean
with
+ Post => "<"'Result = (Left < To_String (Right)),
Global => null;
function "<="
(Left : Bounded_String;
Right : Bounded_String) return Boolean
with
+ Post => "<="'Result = (To_String (Left) <= To_String (Right)),
Global => null;
function "<="
(Left : Bounded_String;
Right : String) return Boolean
with
+ Post => "<="'Result = (To_String (Left) <= Right),
Global => null;
function "<="
(Left : String;
Right : Bounded_String) return Boolean
with
+ Post => "<="'Result = (Left <= To_String (Right)),
Global => null;
function ">"
(Left : Bounded_String;
Right : Bounded_String) return Boolean
with
+ Post => ">"'Result = (To_String (Left) > To_String (Right)),
Global => null;
function ">"
(Left : Bounded_String;
Right : String) return Boolean
with
+ Post => ">"'Result = (To_String (Left) > Right),
Global => null;
function ">"
(Left : String;
Right : Bounded_String) return Boolean
with
+ Post => ">"'Result = (Left > To_String (Right)),
Global => null;
function ">="
(Left : Bounded_String;
Right : Bounded_String) return Boolean
with
+ Post => ">="'Result = (To_String (Left) >= To_String (Right)),
Global => null;
function ">="
(Left : Bounded_String;
Right : String) return Boolean
with
+ Post => ">="'Result = (To_String (Left) >= Right),
Global => null;
function ">="
(Left : String;
Right : Bounded_String) return Boolean
with
+ Post => ">="'Result = (Left >= To_String (Right)),
Global => null;
----------------------
@@ -378,8 +691,52 @@ package Ada.Strings.Bounded 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 : Bounded_String;
@@ -387,8 +744,52 @@ package Ada.Strings.Bounded 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 : Bounded_String;
@@ -396,7 +797,43 @@ package Ada.Strings.Bounded 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 : Bounded_String;
@@ -405,11 +842,60 @@ package Ada.Strings.Bounded 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
@@ -419,11 +905,61 @@ package Ada.Strings.Bounded 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
@@ -433,23 +969,147 @@ package Ada.Strings.Bounded 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 : Bounded_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 : Bounded_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
@@ -465,7 +1125,7 @@ package Ada.Strings.Bounded 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
@@ -482,8 +1142,53 @@ package Ada.Strings.Bounded 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
@@ -493,7 +1198,51 @@ package Ada.Strings.Bounded 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 --
@@ -503,28 +1252,44 @@ package Ada.Strings.Bounded is
(Source : Bounded_String;
Mapping : Maps.Character_Mapping) return Bounded_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 Bounded_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, Element (Source'Old, K))),
Global => null;
function Translate
(Source : Bounded_String;
Mapping : Maps.Character_Mapping_Function) return Bounded_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 Bounded_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 (Element (Source'Old, K))),
Global => null;
---------------------------------------
@@ -541,23 +1306,128 @@ package Ada.Strings.Bounded is
Pre =>
Low - 1 <= Length (Source)
and then
- (if Drop = Error
- then (if High >= Low
- then Low - 1
- <= Max_Length - By'Length
- - Natural'Max (Length (Source) - High, 0)
- else Length (Source) <= Max_Length - By'Length)),
+ (if Drop = Error
+ then (if High >= Low
+ then Low - 1
+ <= Max_Length - By'Length
+ - Integer'Max (Length (Source) - High, 0)
+ else Length (Source) <= Max_Length - By'Length)),
Contract_Cases =>
- (High >= Low =>
- Length (Replace_Slice'Result)
- = Natural'Min
- (Max_Length,
- Low - 1 + By'Length + Natural'Max (Length (Source) - High,
- 0)),
- others =>
- Length (Replace_Slice'Result)
- = Natural'Min (Max_Length, Length (Source) + By'Length)),
- Global => null;
+ (Low - 1 <= Max_Length - By'Length
+ - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
+ =>
+ -- Total length is lower than Max_Length: nothing is dropped
+
+ -- Note that if High < Low, the insertion is done before Low,
+ -- so in all cases the starting position of the slice of Source
+ -- remaining after the replaced Slice is Integer'Max (High + 1,
+ -- Low).
+
+ Length (Replace_Slice'Result) = Low - 1 + By'Length
+ + Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
+ 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
+ and then
+ (if Integer'Max (High, Low - 1) < Length (Source) then
+ Slice (Replace_Slice'Result,
+ Low + By'Length, Length (Replace_Slice'Result)) =
+ Slice (Source,
+ Integer'Max (High + 1, Low), Length (Source))),
+
+ Low - 1 > Max_Length - By'Length
+ - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
+ and then Drop = Left
+ =>
+ -- Final_Slice is the length of the slice of Source remaining
+ -- after the replaced part.
+ (declare
+ Final_Slice : constant Natural :=
+ Integer'Max
+ (Length (Source) - Integer'Max (High, Low - 1), 0);
+ begin
+ -- The result is of maximal length and ends by the last
+ -- Final_Slice characters of Source.
+
+ Length (Replace_Slice'Result) = Max_Length
+ and then
+ (if Final_Slice > 0 then
+ Slice (Replace_Slice'Result,
+ Max_Length - Final_Slice + 1, Max_Length) =
+ Slice (Source,
+ Integer'Max (High + 1, Low), Length (Source)))
+
+ -- Depending on when we reach Max_Length, either the first
+ -- part of Source is fully dropped and By is partly dropped,
+ -- or By is fully added and the first part of Source is
+ -- partly dropped.
+
+ and then
+ (if Max_Length - Final_Slice - By'Length <= 0 then
+
+ -- The first (possibly zero) characters of By are
+ -- dropped.
+
+ (if Final_Slice < Max_Length then
+ Slice (Replace_Slice'Result,
+ 1, Max_Length - Final_Slice) =
+ By (By'Last - Max_Length + Final_Slice + 1
+ .. By'Last))
+
+ else -- By is added to the result
+
+ Slice (Replace_Slice'Result,
+ Max_Length - Final_Slice - By'Length + 1,
+ Max_Length - Final_Slice) =
+ By
+
+ -- The first characters of Source (1 .. Low - 1) are
+ -- dropped.
+
+ and then Slice (Replace_Slice'Result, 1,
+ Max_Length - Final_Slice - By'Length) =
+ Slice (Source,
+ Low - Max_Length + Final_Slice + By'Length,
+ Low - 1))),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first Low -
+ -- 1 characters of Source.
+
+ Length (Replace_Slice'Result) = Max_Length
+ and then
+ Slice (Replace_Slice'Result, 1, Low - 1) =
+ Slice (Source, 1, Low - 1)
+
+ -- Depending on when we reach Max_Length, either the last part
+ -- of Source is fully dropped and By is partly dropped, or By
+ -- is fully added and the last part of Source is partly
+ -- dropped.
+
+ and then
+ (if Low - 1 >= Max_Length - By'Length then
+
+ -- The last characters of By are dropped
+
+ Slice (Replace_Slice'Result, Low, Max_Length) =
+ By (By'First .. Max_Length - Low + By'First)
+
+ else -- By is fully added
+
+ Slice (Replace_Slice'Result, Low, Low + By'Length - 1) = By
+
+ -- Then Source starting from Integer'Max (High + 1, Low)
+ -- is added but the last characters are dropped.
+
+ and then Slice (Replace_Slice'Result,
+ Low + By'Length, Max_Length) =
+ Slice (Source, Integer'Max (High + 1, Low),
+ Integer'Max (High + 1, Low) +
+ (Max_Length - Low - By'Length)))),
+ Global => (Proof_In => Max_Length);
procedure Replace_Slice
(Source : in out Bounded_String;
@@ -569,23 +1439,120 @@ package Ada.Strings.Bounded is
Pre =>
Low - 1 <= Length (Source)
and then
- (if Drop = Error
- then (if High >= Low
- then Low - 1
- <= Max_Length - By'Length
- - Natural'Max (Length (Source) - High, 0)
- else Length (Source) <= Max_Length - By'Length)),
+ (if Drop = Error
+ then (if High >= Low
+ then Low - 1
+ <= Max_Length - By'Length
+ - Natural'Max (Length (Source) - High, 0)
+ else Length (Source) <= Max_Length - By'Length)),
Contract_Cases =>
- (High >= Low =>
- Length (Source)
- = Natural'Min
- (Max_Length,
- Low - 1 + By'Length + Natural'Max (Length (Source)'Old - High,
- 0)),
- others =>
- Length (Source)
- = Natural'Min (Max_Length, Length (Source)'Old + By'Length)),
- Global => null;
+ (Low - 1 <= Max_Length - By'Length
+ - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
+ =>
+ -- Total length is lower than Max_Length: nothing is dropped
+
+ -- Note that if High < Low, the insertion is done before Low,
+ -- so in all cases the starting position of the slice of Source
+ -- remaining after the replaced Slice is Integer'Max (High + 1,
+ -- Low).
+
+ Length (Source) = Low - 1 + By'Length + Integer'Max
+ (Length (Source'Old) - Integer'Max (High, Low - 1), 0)
+ and then
+ Slice (Source, 1, Low - 1) = Slice (Source'Old, 1, Low - 1)
+ and then Slice (Source, Low, Low - 1 + By'Length) = By
+ and then
+ (if Integer'Max (High, Low - 1) < Length (Source'Old) then
+ Slice (Source, Low + By'Length, Length (Source)) =
+ Slice (Source'Old,
+ Integer'Max (High + 1, Low), Length (Source'Old))),
+
+ Low - 1 > Max_Length - By'Length
+ - Integer'Max (Length (Source) - Integer'Max (High, Low - 1), 0)
+ and then Drop = Left
+ =>
+ -- Final_Slice is the length of the slice of Source remaining
+ -- after the replaced part.
+ (declare
+ Final_Slice : constant Integer :=
+ Integer'Max (0,
+ Length (Source'Old) - Integer'Max (High, Low - 1));
+ begin
+ -- The result is of maximal length and ends by the last
+ -- Final_Slice characters of Source.
+
+ Length (Source) = Max_Length
+ and then
+ (if Final_Slice > 0 then
+ Slice (Source,
+ Max_Length - Final_Slice + 1, Max_Length) =
+ Slice (Source'Old,
+ Integer'Max (High + 1, Low), Length (Source'Old)))
+
+ -- Depending on when we reach Max_Length, either the first
+ -- part of Source is fully dropped and By is partly dropped,
+ -- or By is fully added and the first part of Source is
+ -- partly dropped.
+
+ and then
+ (if Max_Length - Final_Slice - By'Length <= 0 then
+
+ -- The first characters of By are dropped
+
+ (if Final_Slice < Max_Length then
+ Slice (Source, 1, Max_Length - Final_Slice) =
+ By (By'Last - Max_Length + Final_Slice + 1
+ .. By'Last))
+
+ else -- By is added to the result
+
+ Slice (Source,
+ Max_Length - Final_Slice - By'Length + 1,
+ Max_Length - Final_Slice) = By
+
+ -- The first characters of Source (1 .. Low - 1) are
+ -- dropped.
+
+ and then Slice (Source, 1,
+ Max_Length - Final_Slice - By'Length) =
+ Slice (Source'Old,
+ Low - Max_Length + Final_Slice + By'Length,
+ Low - 1))),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first Low -
+ -- 1 characters of Source.
+
+ Length (Source) = Max_Length
+ and then
+ Slice (Source, 1, Low - 1) = Slice (Source'Old, 1, Low - 1)
+
+ -- Depending on when we reach Max_Length, either the last part
+ -- of Source is fully dropped and By is partly dropped, or By
+ -- is fully added and the last part of Source is partly
+ -- dropped.
+
+ and then
+ (if Low - 1 >= Max_Length - By'Length then
+
+ -- The last characters of By are dropped
+
+ Slice (Source, Low, Max_Length) =
+ By (By'First .. Max_Length - Low + By'First)
+
+ else -- By is fully added
+
+ Slice (Source, Low, Low + By'Length - 1) = By
+
+ -- Then Source starting from Natural'Max (High + 1, Low)
+ -- is added but the last characters are dropped.
+
+ and then Slice (Source, Low + By'Length, Max_Length) =
+ Slice (Source'Old, Integer'Max (High + 1, Low),
+ Integer'Max (High + 1, Low) +
+ (Max_Length - Low - By'Length)))),
+ Global => (Proof_In => Max_Length);
function Insert
(Source : Bounded_String;
@@ -593,14 +1560,114 @@ package Ada.Strings.Bounded is
New_Item : String;
Drop : Truncation := Error) return Bounded_String
with
- Pre =>
+ Pre =>
Before - 1 <= Length (Source)
and then (if New_Item'Length > Max_Length - Length (Source)
then Drop /= Error),
- Post =>
- Length (Insert'Result)
- = Natural'Min (Max_Length, Length (Source) + New_Item'Length),
- Global => null;
+ Contract_Cases =>
+ (Length (Source) <= Max_Length - New_Item'Length
+ =>
+ -- Total length is lower than Max_Length: nothing is dropped
+
+ Length (Insert'Result) = Length (Source) + New_Item'Length
+ 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
+ and then
+ (if Before <= Length (Source) then
+ Slice (Insert'Result,
+ Before + New_Item'Length, Length (Insert'Result)) =
+ Slice (Source, Before, Length (Source))),
+
+ Length (Source) > Max_Length - New_Item'Length and then Drop = Left
+ =>
+ -- The result is of maximal length and ends by the last
+ -- characters of Source.
+
+ Length (Insert'Result) = Max_Length
+ and then
+ (if Before <= Length (Source) then
+ Slice (Insert'Result,
+ Max_Length - Length (Source) + Before, Max_Length) =
+ Slice (Source, Before, Length (Source)))
+
+ -- Depending on when we reach Max_Length, either the first part
+ -- of Source is fully dropped and New_Item is partly dropped,
+ -- or New_Item is fully added and the first part of Source is
+ -- partly dropped.
+
+ and then
+ (if Max_Length - Length (Source) - 1 + Before
+ < New_Item'Length
+ then
+ -- The first characters of New_Item are dropped
+
+ (if Length (Source) - Before + 1 < Max_Length then
+ Slice (Insert'Result,
+ 1, Max_Length - Length (Source) - 1 + Before) =
+ New_Item
+ (New_Item'Last - Max_Length + Length (Source)
+ - Before + 2
+ .. New_Item'Last))
+
+ else -- New_Item is added to the result
+
+ Slice (Insert'Result,
+ Max_Length - Length (Source) - New_Item'Length + Before,
+ Max_Length - Length (Source) - 1 + Before) = New_Item
+
+ -- The first characters of Source (1 .. Before - 1) are
+ -- dropped.
+
+ and then Slice (Insert'Result,
+ 1, Max_Length - Length (Source) - New_Item'Length
+ - 1 + Before) =
+ Slice (Source,
+ Length (Source) - Max_Length + New_Item'Length
+ + 1,
+ Before - 1)),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first
+ -- characters of Source.
+
+ Length (Insert'Result) = Max_Length
+ and then
+ Slice (Insert'Result, 1, Before - 1) =
+ Slice (Source, 1, Before - 1)
+
+ -- Depending on when we reach Max_Length, either the last part
+ -- of Source is fully dropped and New_Item is partly dropped,
+ -- or New_Item is fully added and the last part of Source is
+ -- partly dropped.
+
+ and then
+ (if Before - 1 >= Max_Length - New_Item'Length then
+
+ -- The last characters of New_Item are dropped
+
+ Slice (Insert'Result, Before, Max_Length) =
+ New_Item (New_Item'First
+ .. Max_Length - Before + New_Item'First)
+
+ else -- New_Item is fully added
+
+ Slice (Insert'Result,
+ Before, Before + New_Item'Length - 1) =
+ New_Item
+
+ -- Then Source starting from Before is added but the
+ -- last characters are dropped.
+
+ and then Slice (Insert'Result,
+ Before + New_Item'Length, Max_Length) =
+ Slice (Source,
+ Before, Max_Length - New_Item'Length))),
+ Global => (Proof_In => Max_Length);
procedure Insert
(Source : in out Bounded_String;
@@ -608,14 +1675,113 @@ package Ada.Strings.Bounded is
New_Item : String;
Drop : Truncation := Error)
with
- Pre =>
+ Pre =>
Before - 1 <= Length (Source)
and then (if New_Item'Length > Max_Length - Length (Source)
then Drop /= Error),
- Post =>
- Length (Source)
- = Natural'Min (Max_Length, Length (Source)'Old + New_Item'Length),
- Global => null;
+ Contract_Cases =>
+ (Length (Source) <= Max_Length - New_Item'Length
+ =>
+ -- Total length is lower than Max_Length: nothing is dropped
+
+ Length (Source) = Length (Source'Old) + New_Item'Length
+ and then
+ Slice (Source, 1, Before - 1) =
+ Slice (Source'Old, 1, Before - 1)
+ and then
+ Slice (Source, Before, Before - 1 + New_Item'Length) =
+ New_Item
+ and then
+ (if Before <= Length (Source'Old) then
+ Slice (Source, Before + New_Item'Length, Length (Source)) =
+ Slice (Source'Old, Before, Length (Source'Old))),
+
+ Length (Source) > Max_Length - New_Item'Length and then Drop = Left
+ =>
+ -- The result is of maximal length and ends by the last
+ -- characters of Source.
+
+ Length (Source) = Max_Length
+ and then
+ (if Before <= Length (Source'Old) then
+ Slice (Source,
+ Max_Length - Length (Source'Old) + Before, Max_Length) =
+ Slice (Source'Old, Before, Length (Source'Old)))
+
+ -- Depending on when we reach Max_Length, either the first part
+ -- of Source is fully dropped and New_Item is partly dropped,
+ -- or New_Item is fully added and the first part of Source is
+ -- partly dropped.
+
+ and then
+ (if Max_Length - Length (Source'Old) - 1 + Before
+ < New_Item'Length
+ then
+ -- The first characters of New_Item are dropped
+
+ (if Length (Source'Old) - Before + 1 < Max_Length then
+ Slice (Source,
+ 1, Max_Length - Length (Source'Old) - 1 + Before) =
+ New_Item
+ (New_Item'Last - Max_Length + Length (Source'Old)
+ - Before + 2
+ .. New_Item'Last))
+
+ else -- New_Item is added to the result
+
+ Slice (Source,
+ Max_Length - Length (Source'Old) - New_Item'Length
+ + Before,
+ Max_Length - Length (Source'Old) - 1 + Before) = New_Item
+
+ -- The first characters of Source (1 .. Before - 1) are
+ -- dropped.
+
+ and then Slice (Source, 1,
+ Max_Length - Length (Source'Old) - New_Item'Length
+ - 1 + Before) =
+ Slice (Source'Old,
+ Length (Source'Old)
+ - Max_Length + New_Item'Length + 1,
+ Before - 1)),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first
+ -- characters of Source.
+
+ Length (Source) = Max_Length
+ and then
+ Slice (Source, 1, Before - 1) =
+ Slice (Source'Old, 1, Before - 1)
+
+ -- Depending on when we reach Max_Length, either the last part
+ -- of Source is fully dropped and New_Item is partly dropped,
+ -- or New_Item is fully added and the last part of Source is
+ -- partly dropped.
+
+ and then
+ (if Before - 1 >= Max_Length - New_Item'Length then
+
+ -- The last characters of New_Item are dropped
+
+ Slice (Source, Before, Max_Length) =
+ New_Item (New_Item'First
+ .. Max_Length - Before + New_Item'First)
+
+ else -- New_Item is fully added
+
+ Slice (Source, Before, Before + New_Item'Length - 1) =
+ New_Item
+
+ -- Then Source starting from Before is added but the
+ -- last characters are dropped.
+
+ and then
+ Slice (Source, Before + New_Item'Length, Max_Length) =
+ Slice (Source'Old,
+ Before, Max_Length - New_Item'Length))),
+ Global => (Proof_In => Max_Length);
function Overwrite
(Source : Bounded_String;
@@ -623,16 +1789,86 @@ package Ada.Strings.Bounded is
New_Item : String;
Drop : Truncation := Error) return Bounded_String
with
- Pre =>
+ Pre =>
Position - 1 <= Length (Source)
and then (if New_Item'Length > Max_Length - (Position - 1)
then Drop /= Error),
- Post =>
- Length (Overwrite'Result)
- = Natural'Max
- (Length (Source),
- Natural'Min (Max_Length, Position - 1 + New_Item'Length)),
- Global => null;
+ Contract_Cases =>
+ (Position - 1 <= Max_Length - New_Item'Length
+ =>
+ -- The length is unchanged, unless New_Item overwrites further
+ -- than the end of Source. In this contract case, we suppose
+ -- New_Item doesn't overwrite further than Max_Length.
+
+ Length (Overwrite'Result) =
+ Integer'Max (Length (Source), Position - 1 + New_Item'Length)
+ 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))),
+
+ Position - 1 > Max_Length - New_Item'Length and then Drop = Left
+ =>
+ Length (Overwrite'Result) = Max_Length
+
+ -- If a part of the result has to be dropped, it means New_Item
+ -- is overwriting further than the end of Source. Thus the
+ -- result is necessarily ending by New_Item. However, we don't
+ -- know whether New_Item covers all Max_Length characters or
+ -- some characters of Source are remaining at the left.
+
+ and then
+ (if New_Item'Length > Max_Length then
+
+ -- New_Item covers all Max_Length characters
+
+ To_String (Overwrite'Result) =
+ New_Item
+ (New_Item'Last - Max_Length + 1 .. New_Item'Last)
+ else
+ -- New_Item fully appears at the end
+
+ Slice (Overwrite'Result,
+ Max_Length - New_Item'Length + 1, Max_Length) =
+ New_Item
+
+ -- The left of Source is cut
+
+ and then
+ Slice (Overwrite'Result,
+ 1, Max_Length - New_Item'Length) =
+ Slice (Source,
+ Position - Max_Length + New_Item'Length,
+ Position - 1)),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first
+ -- characters of Source.
+
+ Length (Overwrite'Result) = Max_Length
+ and then
+ Slice (Overwrite'Result, 1, Position - 1) =
+ Slice (Source, 1, Position - 1)
+
+ -- Then New_Item is written until Max_Length
+
+ and then Slice (Overwrite'Result, Position, Max_Length) =
+ New_Item
+ (New_Item'First .. Max_Length - Position + New_Item'First)),
+ Global => (Proof_In => Max_Length);
procedure Overwrite
(Source : in out Bounded_String;
@@ -640,16 +1876,85 @@ package Ada.Strings.Bounded is
New_Item : String;
Drop : Truncation := Error)
with
- Pre =>
+ Pre =>
Position - 1 <= Length (Source)
and then (if New_Item'Length > Max_Length - (Position - 1)
then Drop /= Error),
- Post =>
- Length (Source)
- = Natural'Max
- (Length (Source)'Old,
- Natural'Min (Max_Length, Position - 1 + New_Item'Length)),
- Global => null;
+ Contract_Cases =>
+ (Position - 1 <= Max_Length - New_Item'Length
+ =>
+ -- The length of Source is unchanged, unless New_Item overwrites
+ -- further than the end of Source. In this contract case, we
+ -- suppose New_Item doesn't overwrite further than Max_Length.
+
+ Length (Source) = Integer'Max
+ (Length (Source'Old), Position - 1 + New_Item'Length)
+ and then
+ Slice (Source, 1, Position - 1) =
+ Slice (Source'Old, 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'Old,
+ Position + New_Item'Length, Length (Source'Old))),
+
+ Position - 1 > Max_Length - New_Item'Length and then Drop = Left
+ =>
+ Length (Source) = Max_Length
+
+ -- If a part of the result has to be dropped, it means New_Item
+ -- is overwriting further than the end of Source. Thus the
+ -- result is necessarily ending by New_Item. However, we don't
+ -- know whether New_Item covers all Max_Length characters or
+ -- some characters of Source are remaining at the left.
+
+ and then
+ (if New_Item'Length > Max_Length then
+
+ -- New_Item covers all Max_Length characters
+
+ To_String (Source) =
+ New_Item
+ (New_Item'Last - Max_Length + 1 .. New_Item'Last)
+ else
+ -- New_Item fully appears at the end
+
+ Slice (Source,
+ Max_Length - New_Item'Length + 1, Max_Length) =
+ New_Item
+
+ -- The left of Source is cut
+
+ and then
+ Slice (Source, 1, Max_Length - New_Item'Length) =
+ Slice (Source'Old,
+ Position - Max_Length + New_Item'Length,
+ Position - 1)),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first
+ -- characters of Source.
+
+ Length (Source) = Max_Length
+ and then
+ Slice (Source, 1, Position - 1) =
+ Slice (Source'Old, 1, Position - 1)
+
+ -- New_Item is written until Max_Length
+
+ and then Slice (Source, Position, Max_Length) =
+ New_Item
+ (New_Item'First .. Max_Length - Position + New_Item'First)),
+ Global => (Proof_In => Max_Length);
function Delete
(Source : Bounded_String;
@@ -657,13 +1962,20 @@ package Ada.Strings.Bounded is
Through : Natural) return Bounded_String
with
Pre =>
- (if Through <= From then From - 1 <= Length (Source)),
+ (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
@@ -672,12 +1984,19 @@ package Ada.Strings.Bounded is
Through : Natural)
with
Pre =>
- (if Through <= From then From - 1 <= Length (Source)),
+ (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) = Slice (Source'Old, 1, From - 1)
+ and then
+ (if Through < Length (Source) then
+ Slice (Source, From, Length (Source)) =
+ Slice (Source'Old, Through + 1, Length (Source'Old))),
others =>
- Length (Source) = Length (Source)'Old),
+ Source = Source'Old),
Global => null;
---------------------------------
@@ -688,31 +2007,111 @@ package Ada.Strings.Bounded is
(Source : Bounded_String;
Side : Trim_End) return Bounded_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 Bounded_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'Old, Forward));
+ High : constant Positive :=
+ (if Side = Left then Length (Source'Old)
+ else Index_Non_Blank (Source'Old, Backward));
+ begin
+ To_String (Source) = Slice (Source'Old, Low, High))),
+ Global => null;
function Trim
(Source : Bounded_String;
Left : Maps.Character_Set;
Right : Maps.Character_Set) return Bounded_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 Bounded_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'Old, Left, Outside, Forward);
+ High : constant Positive :=
+ Index (Source'Old, Right, Outside, Backward);
+ begin
+ To_String (Source) = Slice (Source'Old, Low, High))),
+ Global => null;
function Head
(Source : Bounded_String;
@@ -720,9 +2119,55 @@ package Ada.Strings.Bounded is
Pad : Character := Space;
Drop : Truncation := Error) return Bounded_String
with
- Pre => (if Count > Max_Length then Drop /= Error),
- Post => Length (Head'Result) = Natural'Min (Max_Length, Count),
- Global => null;
+ Pre => (if Count > Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Count <= Length (Source)
+ =>
+ -- Source is cut
+
+ To_String (Head'Result) = Slice (Source, 1, Count),
+
+ Count > Length (Source) and then Count <= Max_Length
+ =>
+ -- Source is followed by Pad characters
+
+ Length (Head'Result) = Count
+ and then
+ Slice (Head'Result, 1, Length (Source)) = To_String (Source)
+ and then
+ Slice (Head'Result, Length (Source) + 1, Count) =
+ (1 .. Count - Length (Source) => Pad),
+
+ Count > Max_Length and then Drop = Right
+ =>
+ -- Source is followed by Pad characters
+
+ Length (Head'Result) = Max_Length
+ and then
+ Slice (Head'Result, 1, Length (Source)) = To_String (Source)
+ and then
+ Slice (Head'Result, Length (Source) + 1, Max_Length) =
+ (1 .. Max_Length - Length (Source) => Pad),
+
+ Count - Length (Source) > Max_Length and then Drop = Left
+ =>
+ -- Source is fully dropped at the left
+
+ To_String (Head'Result) = (1 .. Max_Length => Pad),
+
+ others
+ =>
+ -- Source is partly dropped at the left
+
+ Length (Head'Result) = Max_Length
+ and then
+ Slice (Head'Result, 1, Max_Length - Count + Length (Source)) =
+ Slice (Source, Count - Max_Length + 1, Length (Source))
+ and then
+ Slice (Head'Result,
+ Max_Length - Count + Length (Source) + 1, Max_Length) =
+ (1 .. Count - Length (Source) => Pad)),
+ Global => (Proof_In => Max_Length);
procedure Head
(Source : in out Bounded_String;
@@ -730,9 +2175,58 @@ package Ada.Strings.Bounded is
Pad : Character := Space;
Drop : Truncation := Error)
with
- Pre => (if Count > Max_Length then Drop /= Error),
- Post => Length (Source) = Natural'Min (Max_Length, Count),
- Global => null;
+ Pre => (if Count > Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Count <= Length (Source)
+ =>
+ -- Source is cut
+
+ To_String (Source) = Slice (Source'Old, 1, Count),
+
+ Count > Length (Source) and then Count <= Max_Length
+ =>
+ -- Source is followed by Pad characters
+
+ Length (Source) = Count
+ and then
+ 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),
+
+ Count > Max_Length and then Drop = Right
+ =>
+ -- Source is followed by Pad characters
+
+ Length (Source) = Max_Length
+ and then
+ Slice (Source, 1, Length (Source'Old)) =
+ To_String (Source'Old)
+ and then
+ Slice (Source, Length (Source'Old) + 1, Max_Length) =
+ (1 .. Max_Length - Length (Source'Old) => Pad),
+
+ Count - Length (Source) > Max_Length and then Drop = Left
+ =>
+ -- Source is fully dropped on the left
+
+ To_String (Source) = (1 .. Max_Length => Pad),
+
+ others
+ =>
+ -- Source is partly dropped on the left
+
+ Length (Source) = Max_Length
+ and then
+ Slice (Source, 1, Max_Length - Count + Length (Source'Old)) =
+ Slice (Source'Old,
+ Count - Max_Length + 1, Length (Source'Old))
+ and then
+ Slice (Source,
+ Max_Length - Count + Length (Source'Old) + 1, Max_Length) =
+ (1 .. Count - Length (Source'Old) => Pad)),
+ Global => (Proof_In => Max_Length);
function Tail
(Source : Bounded_String;
@@ -740,9 +2234,61 @@ package Ada.Strings.Bounded is
Pad : Character := Space;
Drop : Truncation := Error) return Bounded_String
with
- Pre => (if Count > Max_Length then Drop /= Error),
- Post => Length (Tail'Result) = Natural'Min (Max_Length, Count),
- Global => null;
+ Pre => (if Count > Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Count < Length (Source)
+ =>
+ -- Source is cut
+
+ (if Count > 0 then
+ To_String (Tail'Result) =
+ Slice (Source, Length (Source) - Count + 1, Length (Source))
+ else Length (Tail'Result) = 0),
+
+ Count >= Length (Source) and then Count < Max_Length
+ =>
+ -- Source is preceded by Pad characters
+
+ Length (Tail'Result) = Count
+ and then
+ 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),
+
+ Count >= Max_Length and then Drop = Left
+ =>
+ -- Source is preceded by Pad characters
+
+ Length (Tail'Result) = Max_Length
+ and then
+ Slice (Tail'Result, 1, Max_Length - Length (Source)) =
+ (1 .. Max_Length - Length (Source) => Pad)
+ and then
+ (if Length (Source) > 0 then
+ Slice (Tail'Result,
+ Max_Length - Length (Source) + 1, Max_Length) =
+ To_String (Source)),
+
+ Count - Length (Source) >= Max_Length and then Drop /= Left
+ =>
+ -- Source is fully dropped on the right
+
+ To_String (Tail'Result) = (1 .. Max_Length => Pad),
+
+ others
+ =>
+ -- Source is partly dropped on the right
+
+ Length (Tail'Result) = Max_Length
+ and then
+ Slice (Tail'Result, 1, Count - Length (Source)) =
+ (1 .. Count - Length (Source) => Pad)
+ and then
+ Slice (Tail'Result, Count - Length (Source) + 1, Max_Length) =
+ Slice (Source, 1, Max_Length - Count + Length (Source))),
+ Global => (Proof_In => Max_Length);
procedure Tail
(Source : in out Bounded_String;
@@ -750,9 +2296,63 @@ package Ada.Strings.Bounded is
Pad : Character := Space;
Drop : Truncation := Error)
with
- Pre => (if Count > Max_Length then Drop /= Error),
- Post => Length (Source) = Natural'Min (Max_Length, Count),
- Global => null;
+ Pre => (if Count > Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Count < Length (Source)
+ =>
+ -- Source is cut
+
+ (if Count > 0 then
+ To_String (Source) =
+ Slice (Source'Old,
+ Length (Source'Old) - Count + 1, Length (Source'Old))
+ else Length (Source) = 0),
+
+ Count >= Length (Source) and then Count < Max_Length
+ =>
+ -- Source is preceded by Pad characters
+
+ Length (Source) = Count
+ and then
+ 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),
+
+ Count >= Max_Length and then Drop = Left
+ =>
+ -- Source is preceded by Pad characters
+
+ Length (Source) = Max_Length
+ and then
+ Slice (Source, 1, Max_Length - Length (Source'Old)) =
+ (1 .. Max_Length - Length (Source'Old) => Pad)
+ and then
+ (if Length (Source'Old) > 0 then
+ Slice (Source,
+ Max_Length - Length (Source'Old) + 1, Max_Length) =
+ To_String (Source'Old)),
+
+ Count - Length (Source) >= Max_Length and then Drop /= Left
+ =>
+ -- Source is fully dropped at the right
+
+ To_String (Source) = (1 .. Max_Length => Pad),
+
+ others
+ =>
+ -- Source is partly dropped at the right
+
+ Length (Source) = Max_Length
+ and then
+ Slice (Source, 1, Count - Length (Source'Old)) =
+ (1 .. Count - Length (Source'Old) => Pad)
+ and then
+ Slice (Source, Count - Length (Source'Old) + 1, Max_Length) =
+ Slice (Source'Old,
+ 1, Max_Length - Count + Length (Source'Old))),
+ Global => (Proof_In => Max_Length);
------------------------------------
-- String Constructor Subprograms --
@@ -763,24 +2363,36 @@ package Ada.Strings.Bounded is
Right : Character) return Bounded_String
with
Pre => Left <= Max_Length,
- Post => Length ("*"'Result) = Left,
- Global => null;
+ Post => To_String ("*"'Result) = (1 .. Left => Right),
+ Global => Max_Length;
function "*"
(Left : Natural;
Right : String) return Bounded_String
with
Pre => (if Left /= 0 then Right'Length <= Max_Length / Left),
- Post => Length ("*"'Result) = Left * Right'Length,
- Global => null;
+ 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 => Max_Length;
function "*"
(Left : Natural;
Right : Bounded_String) return Bounded_String
with
Pre => (if Left /= 0 then Length (Right) <= Max_Length / Left),
- Post => Length ("*"'Result) = Left * Length (Right),
- Global => null;
+ 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 => (Proof_In => Max_Length);
function Replicate
(Count : Natural;
@@ -789,37 +2401,80 @@ package Ada.Strings.Bounded is
with
Pre => (if Count > Max_Length then Drop /= Error),
Post =>
- Length (Replicate'Result)
- = Natural'Min (Max_Length, Count),
- Global => null;
+ To_String (Replicate'Result) =
+ (1 .. Natural'Min (Max_Length, Count) => Item),
+ Global => Max_Length;
function Replicate
(Count : Natural;
Item : String;
Drop : Truncation := Error) return Bounded_String
with
- Pre =>
- (if Item'Length /= 0
- and then Count > Max_Length / Item'Length
+ Pre =>
+ (if Count /= 0 and then Item'Length > Max_Length / Count
then Drop /= Error),
- Post =>
- Length (Replicate'Result)
- = Natural'Min (Max_Length, Count * Item'Length),
- Global => null;
+ Contract_Cases =>
+ (Count = 0 or else Item'Length <= Max_Length / Count
+ =>
+ Length (Replicate'Result) = Count * Item'Length
+ and then
+ (if Item'Length > 0 then
+ (for all K in 1 .. Count * Item'Length =>
+ Element (Replicate'Result, K) =
+ Item (Item'First + (K - 1) mod Item'Length))),
+ Count /= 0
+ and then Item'Length > Max_Length / Count
+ and then Drop = Right
+ =>
+ Length (Replicate'Result) = Max_Length
+ and then
+ (for all K in 1 .. Max_Length =>
+ Element (Replicate'Result, K) =
+ Item (Item'First + (K - 1) mod Item'Length)),
+ others -- Drop = Left
+ =>
+ Length (Replicate'Result) = Max_Length
+ and then
+ (for all K in 1 .. Max_Length =>
+ Element (Replicate'Result, K) =
+ Item (Item'Last - (Max_Length - K) mod Item'Length))),
+ Global => Max_Length;
function Replicate
(Count : Natural;
Item : Bounded_String;
Drop : Truncation := Error) return Bounded_String
with
- Pre =>
- (if Length (Item) /= 0
- and then Count > Max_Length / Length (Item)
+ Pre =>
+ (if Count /= 0 and then Length (Item) > Max_Length / Count
then Drop /= Error),
- Post =>
- Length (Replicate'Result)
- = Natural'Min (Max_Length, Count * Length (Item)),
- Global => null;
+ Contract_Cases =>
+ ((if Count /= 0 then Length (Item) <= Max_Length / Count)
+ =>
+ Length (Replicate'Result) = Count * Length (Item)
+ and then
+ (if Length (Item) > 0 then
+ (for all K in 1 .. Count * Length (Item) =>
+ Element (Replicate'Result, K) =
+ Element (Item, 1 + (K - 1) mod Length (Item)))),
+ Count /= 0
+ and then Length (Item) > Max_Length / Count
+ and then Drop = Right
+ =>
+ Length (Replicate'Result) = Max_Length
+ and then
+ (for all K in 1 .. Max_Length =>
+ Element (Replicate'Result, K) =
+ Element (Item, 1 + (K - 1) mod Length (Item))),
+ others -- Drop = Left
+ =>
+ Length (Replicate'Result) = Max_Length
+ and then
+ (for all K in 1 .. Max_Length =>
+ Element (Replicate'Result, K) =
+ Element (Item,
+ Length (Item) - (Max_Length - K) mod Length (Item)))),
+ Global => (Proof_In => Max_Length);
private
-- Most of the implementation is in the separate non generic package
@@ -843,7 +2498,8 @@ package Ada.Strings.Bounded is
-- the generic instantiation is compatible with the Super_String
-- type declared in the Superbounded package.
- function From_String (Source : String) return Bounded_String;
+ function From_String (Source : String) return Bounded_String
+ with Pre => Source'Length <= Max_Length;
-- Private routine used only by Stream_Convert
pragma Stream_Convert (Bounded_String, From_String, To_String);
diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads
index 1a5ee9473f2..168a8e0ddda 100644
--- a/gcc/ada/libgnat/a-strfix.ads
+++ b/gcc/ada/libgnat/a-strfix.ads
@@ -382,7 +382,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
=>
Index'Result = 0,
- -- Otherwise, a index in the range of Source is returned
+ -- Otherwise, an index in the range of Source is returned
others
=>
@@ -392,7 +392,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
Index'Result in Source'Range
-- The character at the returned index satisfies the property
- -- Test on Set
+ -- Test on Set.
and then
(Test = Inside)
@@ -433,7 +433,7 @@ package Ada.Strings.Fixed with SPARK_Mode is
=>
Index'Result = 0,
- -- Otherwise, a index in the considered range of Source is returned
+ -- Otherwise, an index in the considered range of Source is returned
others
=>
diff --git a/gcc/ada/libgnat/a-strsea.ads b/gcc/ada/libgnat/a-strsea.ads
index 4396747f704..f4e7d361408 100644
--- a/gcc/ada/libgnat/a-strsea.ads
+++ b/gcc/ada/libgnat/a-strsea.ads
@@ -213,7 +213,7 @@ package Ada.Strings.Search with SPARK_Mode is
=>
Index'Result = 0,
- -- Otherwise, a index in the range of Source is returned
+ -- Otherwise, an index in the range of Source is returned
others =>
@@ -222,7 +222,7 @@ package Ada.Strings.Search with SPARK_Mode is
Index'Result in Source'Range
-- The character at the returned index satisfies the property
- -- Test on Set
+ -- Test on Set.
and then (Test = Inside)
= Ada.Strings.Maps.Is_In (Source (Index'Result), Set)
@@ -377,7 +377,7 @@ package Ada.Strings.Search with SPARK_Mode is
=>
Index'Result = 0,
- -- Otherwise, a index in the considered range of Source is returned
+ -- Otherwise, an index in the considered range of Source is returned
others =>
diff --git a/gcc/ada/libgnat/a-strsup.adb b/gcc/ada/libgnat/a-strsup.adb
index 1e85cc23b19..a94d6cad4e0 100644
--- a/gcc/ada/libgnat/a-strsup.adb
+++ b/gcc/ada/libgnat/a-strsup.adb
@@ -29,10 +29,17 @@
-- --
------------------------------------------------------------------------------
-with Ada.Strings.Maps; use Ada.Strings.Maps;
-with Ada.Strings.Search;
+-- Ghost code, loop invariants and assertions in this unit are meant for
+-- analysis only, not for run-time checking, as it would be too costly
+-- otherwise. This is enforced by setting the assertion policy to Ignore.
-package body Ada.Strings.Superbounded is
+pragma Assertion_Policy (Ghost => Ignore,
+ Loop_Invariant => Ignore,
+ Assert => Ignore);
+
+with Ada.Strings.Maps; use Ada.Strings.Maps;
+
+package body Ada.Strings.Superbounded with SPARK_Mode is
------------
-- Concat --
@@ -53,9 +60,13 @@ package body Ada.Strings.Superbounded is
raise Ada.Strings.Length_Error;
end if;
- Result.Current_Length := Nlen;
Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
- Result.Data (Llen + 1 .. Nlen) := Right.Data (1 .. Rlen);
+
+ if Rlen > 0 then
+ Result.Data (Llen + 1 .. Nlen) := Right.Data (1 .. Rlen);
+ end if;
+
+ Result.Current_Length := Nlen;
end;
end return;
end Concat;
@@ -74,9 +85,13 @@ package body Ada.Strings.Superbounded is
raise Ada.Strings.Length_Error;
end if;
- Result.Current_Length := Nlen;
Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
- Result.Data (Llen + 1 .. Nlen) := Right;
+
+ if Right'Length > 0 then
+ Result.Data (Llen + 1 .. Nlen) := Super_String_Data (Right);
+ end if;
+
+ Result.Current_Length := Nlen;
end;
end return;
end Concat;
@@ -97,9 +112,13 @@ package body Ada.Strings.Superbounded is
raise Ada.Strings.Length_Error;
end if;
+ Result.Data (1 .. Llen) := Super_String_Data (Left);
+
+ if Rlen > 0 then
+ Result.Data (Llen + 1 .. Nlen) := Right.Data (1 .. Rlen);
+ end if;
+
Result.Current_Length := Nlen;
- Result.Data (1 .. Llen) := Left;
- Result.Data (Llen + 1 .. Nlen) := Right.Data (1 .. Rlen);
end;
end return;
end Concat;
@@ -117,9 +136,9 @@ package body Ada.Strings.Superbounded is
raise Ada.Strings.Length_Error;
end if;
- Result.Current_Length := Llen + 1;
Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
- Result.Data (Result.Current_Length) := Right;
+ Result.Data (Llen + 1) := Right;
+ Result.Current_Length := Llen + 1;
end;
end return;
end Concat;
@@ -137,10 +156,9 @@ package body Ada.Strings.Superbounded is
raise Ada.Strings.Length_Error;
end if;
- Result.Current_Length := Rlen + 1;
Result.Data (1) := Left;
- Result.Data (2 .. Result.Current_Length) :=
- Right.Data (1 .. Rlen);
+ Result.Data (2 .. Rlen + 1) := Right.Data (1 .. Rlen);
+ Result.Current_Length := Rlen + 1;
end;
end return;
end Concat;
@@ -154,9 +172,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Boolean
is
begin
- return Left.Current_Length = Right.Current_Length
- and then Left.Data (1 .. Left.Current_Length) =
- Right.Data (1 .. Right.Current_Length);
+ return Super_To_String (Left) = Super_To_String (Right);
end "=";
function Equal
@@ -164,8 +180,7 @@ package body Ada.Strings.Superbounded is
Right : String) return Boolean
is
begin
- return Left.Current_Length = Right'Length
- and then Left.Data (1 .. Left.Current_Length) = Right;
+ return Super_To_String (Left) = Right;
end Equal;
function Equal
@@ -173,8 +188,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Boolean
is
begin
- return Left'Length = Right.Current_Length
- and then Left = Right.Data (1 .. Right.Current_Length);
+ return Left = Super_To_String (Right);
end Equal;
-------------
@@ -186,8 +200,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Boolean
is
begin
- return Left.Data (1 .. Left.Current_Length) >
- Right.Data (1 .. Right.Current_Length);
+ return Super_To_String (Left) > Super_To_String (Right);
end Greater;
function Greater
@@ -195,7 +208,7 @@ package body Ada.Strings.Superbounded is
Right : String) return Boolean
is
begin
- return Left.Data (1 .. Left.Current_Length) > Right;
+ return Super_To_String (Left) > Right;
end Greater;
function Greater
@@ -203,7 +216,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Boolean
is
begin
- return Left > Right.Data (1 .. Right.Current_Length);
+ return Left > Super_To_String (Right);
end Greater;
----------------------
@@ -215,8 +228,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Boolean
is
begin
- return Left.Data (1 .. Left.Current_Length) >=
- Right.Data (1 .. Right.Current_Length);
+ return Super_To_String (Left) >= Super_To_String (Right);
end Greater_Or_Equal;
function Greater_Or_Equal
@@ -224,7 +236,7 @@ package body Ada.Strings.Superbounded is
Right : String) return Boolean
is
begin
- return Left.Data (1 .. Left.Current_Length) >= Right;
+ return Super_To_String (Left) >= Right;
end Greater_Or_Equal;
function Greater_Or_Equal
@@ -232,7 +244,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Boolean
is
begin
- return Left >= Right.Data (1 .. Right.Current_Length);
+ return Left >= Super_To_String (Right);
end Greater_Or_Equal;
----------
@@ -244,8 +256,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Boolean
is
begin
- return Left.Data (1 .. Left.Current_Length) <
- Right.Data (1 .. Right.Current_Length);
+ return Super_To_String (Left) < Super_To_String (Right);
end Less;
function Less
@@ -253,7 +264,7 @@ package body Ada.Strings.Superbounded is
Right : String) return Boolean
is
begin
- return Left.Data (1 .. Left.Current_Length) < Right;
+ return Super_To_String (Left) < Right;
end Less;
function Less
@@ -261,7 +272,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Boolean
is
begin
- return Left < Right.Data (1 .. Right.Current_Length);
+ return Left < Super_To_String (Right);
end Less;
-------------------
@@ -273,8 +284,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Boolean
is
begin
- return Left.Data (1 .. Left.Current_Length) <=
- Right.Data (1 .. Right.Current_Length);
+ return Super_To_String (Left) <= Super_To_String (Right);
end Less_Or_Equal;
function Less_Or_Equal
@@ -282,7 +292,7 @@ package body Ada.Strings.Superbounded is
Right : String) return Boolean
is
begin
- return Left.Data (1 .. Left.Current_Length) <= Right;
+ return Super_To_String (Left) <= Right;
end Less_Or_Equal;
function Less_Or_Equal
@@ -290,7 +300,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Boolean
is
begin
- return Left <= Right.Data (1 .. Right.Current_Length);
+ return Left <= Super_To_String (Right);
end Less_Or_Equal;
----------------------
@@ -307,20 +317,20 @@ package body Ada.Strings.Superbounded is
begin
if Slen <= Max_Length then
+ Target.Data (1 .. Slen) := Super_String_Data (Source);
Target.Current_Length := Slen;
- Target.Data (1 .. Slen) := Source;
else
case Drop is
when Strings.Right =>
+ Target.Data (1 .. Max_Length) := Super_String_Data
+ (Source (Source'First .. Source'First - 1 + Max_Length));
Target.Current_Length := Max_Length;
- Target.Data (1 .. Max_Length) :=
- Source (Source'First .. Source'First - 1 + Max_Length);
when Strings.Left =>
+ Target.Data (1 .. Max_Length) := Super_String_Data
+ (Source (Source'Last - (Max_Length - 1) .. Source'Last));
Target.Current_Length := Max_Length;
- Target.Data (1 .. Max_Length) :=
- Source (Source'Last - (Max_Length - 1) .. Source'Last);
when Strings.Error =>
raise Ada.Strings.Length_Error;
@@ -343,17 +353,18 @@ package body Ada.Strings.Superbounded is
Result : Super_String (Max_Length);
Llen : constant Natural := Left.Current_Length;
Rlen : constant Natural := Right.Current_Length;
- Nlen : constant Natural := Llen + Rlen;
begin
- if Nlen <= Max_Length then
- Result.Current_Length := Nlen;
+ if Llen <= Max_Length - Rlen then
Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
- Result.Data (Llen + 1 .. Nlen) := Right.Data (1 .. Rlen);
- else
- Result.Current_Length := Max_Length;
+ if Rlen > 0 then
+ Result.Data (Llen + 1 .. Llen + Rlen) := Right.Data (1 .. Rlen);
+ end if;
+
+ Result.Current_Length := Llen + Rlen;
+ else
case Drop is
when Strings.Right =>
if Llen >= Max_Length then -- only case is Llen = Max_Length
@@ -379,6 +390,8 @@ package body Ada.Strings.Superbounded is
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Result.Current_Length := Max_Length;
end if;
return Result;
@@ -392,16 +405,15 @@ package body Ada.Strings.Superbounded is
Max_Length : constant Positive := Source.Max_Length;
Llen : constant Natural := Source.Current_Length;
Rlen : constant Natural := New_Item.Current_Length;
- Nlen : constant Natural := Llen + Rlen;
begin
- if Nlen <= Max_Length then
- Source.Current_Length := Nlen;
- Source.Data (Llen + 1 .. Nlen) := New_Item.Data (1 .. Rlen);
+ if Llen <= Max_Length - Rlen then
+ if Rlen > 0 then
+ Source.Data (Llen + 1 .. Llen + Rlen) := New_Item.Data (1 .. Rlen);
+ Source.Current_Length := Llen + Rlen;
+ end if;
else
- Source.Current_Length := Max_Length;
-
case Drop is
when Strings.Right =>
if Llen < Max_Length then
@@ -423,6 +435,8 @@ package body Ada.Strings.Superbounded is
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Source.Current_Length := Max_Length;
end if;
end Super_Append;
@@ -438,17 +452,18 @@ package body Ada.Strings.Superbounded is
Result : Super_String (Max_Length);
Llen : constant Natural := Left.Current_Length;
Rlen : constant Natural := Right'Length;
- Nlen : constant Natural := Llen + Rlen;
begin
- if Nlen <= Max_Length then
- Result.Current_Length := Nlen;
+ if Llen <= Max_Length - Rlen then
Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
- Result.Data (Llen + 1 .. Nlen) := Right;
- else
- Result.Current_Length := Max_Length;
+ if Rlen > 0 then
+ Result.Data (Llen + 1 .. Llen + Rlen) := Super_String_Data (Right);
+ end if;
+
+ Result.Current_Length := Llen + Rlen;
+ else
case Drop is
when Strings.Right =>
if Llen >= Max_Length then -- only case is Llen = Max_Length
@@ -456,27 +471,29 @@ package body Ada.Strings.Superbounded is
else
Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
- Result.Data (Llen + 1 .. Max_Length) :=
- Right (Right'First .. Right'First - 1 +
- Max_Length - Llen);
+ Result.Data (Llen + 1 .. Max_Length) := Super_String_Data
+ (Right
+ (Right'First .. Right'First - 1 - Llen + Max_Length));
end if;
when Strings.Left =>
if Rlen >= Max_Length then
- Result.Data (1 .. Max_Length) :=
- Right (Right'Last - (Max_Length - 1) .. Right'Last);
+ Result.Data (1 .. Max_Length) := Super_String_Data
+ (Right (Right'Last - (Max_Length - 1) .. Right'Last));
else
Result.Data (1 .. Max_Length - Rlen) :=
Left.Data (Llen - (Max_Length - Rlen - 1) .. Llen);
Result.Data (Max_Length - Rlen + 1 .. Max_Length) :=
- Right;
+ Super_String_Data (Right);
end if;
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Result.Current_Length := Max_Length;
end if;
return Result;
@@ -490,40 +507,42 @@ package body Ada.Strings.Superbounded is
Max_Length : constant Positive := Source.Max_Length;
Llen : constant Natural := Source.Current_Length;
Rlen : constant Natural := New_Item'Length;
- Nlen : constant Natural := Llen + Rlen;
begin
- if Nlen <= Max_Length then
- Source.Current_Length := Nlen;
- Source.Data (Llen + 1 .. Nlen) := New_Item;
+ if Llen <= Max_Length - Rlen then
+ if Rlen > 0 then
+ Source.Data (Llen + 1 .. Llen + Rlen) :=
+ Super_String_Data (New_Item);
+ Source.Current_Length := Llen + Rlen;
+ end if;
else
- Source.Current_Length := Max_Length;
-
case Drop is
when Strings.Right =>
if Llen < Max_Length then
- Source.Data (Llen + 1 .. Max_Length) :=
- New_Item (New_Item'First ..
- New_Item'First - 1 + Max_Length - Llen);
+ Source.Data (Llen + 1 .. Max_Length) := Super_String_Data
+ (New_Item (New_Item'First ..
+ New_Item'First - 1 - Llen + Max_Length));
end if;
when Strings.Left =>
if Rlen >= Max_Length then
- Source.Data (1 .. Max_Length) :=
- New_Item (New_Item'Last - (Max_Length - 1) ..
- New_Item'Last);
+ Source.Data (1 .. Max_Length) := Super_String_Data
+ (New_Item (New_Item'Last - (Max_Length - 1) ..
+ New_Item'Last));
else
Source.Data (1 .. Max_Length - Rlen) :=
Source.Data (Llen - (Max_Length - Rlen - 1) .. Llen);
Source.Data (Max_Length - Rlen + 1 .. Max_Length) :=
- New_Item;
+ Super_String_Data (New_Item);
end if;
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Source.Current_Length := Max_Length;
end if;
end Super_Append;
@@ -539,25 +558,25 @@ package body Ada.Strings.Superbounded is
Result : Super_String (Max_Length);
Llen : constant Natural := Left'Length;
Rlen : constant Natural := Right.Current_Length;
- Nlen : constant Natural := Llen + Rlen;
begin
- if Nlen <= Max_Length then
- Result.Current_Length := Nlen;
- Result.Data (1 .. Llen) := Left;
- Result.Data (Llen + 1 .. Llen + Rlen) := Right.Data (1 .. Rlen);
+ if Llen <= Max_Length - Rlen then
+ Result.Data (1 .. Llen) := Super_String_Data (Left);
- else
- Result.Current_Length := Max_Length;
+ if Rlen > 0 then
+ Result.Data (Llen + 1 .. Llen + Rlen) := Right.Data (1 .. Rlen);
+ end if;
+ Result.Current_Length := Llen + Rlen;
+ else
case Drop is
when Strings.Right =>
if Llen >= Max_Length then
- Result.Data (1 .. Max_Length) :=
- Left (Left'First .. Left'First + (Max_Length - 1));
+ Result.Data (1 .. Max_Length) := Super_String_Data
+ (Left (Left'First .. Left'First + (Max_Length - 1)));
else
- Result.Data (1 .. Llen) := Left;
+ Result.Data (1 .. Llen) := Super_String_Data (Left);
Result.Data (Llen + 1 .. Max_Length) :=
Right.Data (1 .. Max_Length - Llen);
end if;
@@ -568,8 +587,8 @@ package body Ada.Strings.Superbounded is
Right.Data (Rlen - (Max_Length - 1) .. Rlen);
else
- Result.Data (1 .. Max_Length - Rlen) :=
- Left (Left'Last - (Max_Length - Rlen - 1) .. Left'Last);
+ Result.Data (1 .. Max_Length - Rlen) := Super_String_Data
+ (Left (Left'Last - (Max_Length - Rlen - 1) .. Left'Last));
Result.Data (Max_Length - Rlen + 1 .. Max_Length) :=
Right.Data (1 .. Rlen);
end if;
@@ -577,6 +596,8 @@ package body Ada.Strings.Superbounded is
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Result.Current_Length := Max_Length;
end if;
return Result;
@@ -595,9 +616,9 @@ package body Ada.Strings.Superbounded is
begin
if Llen < Max_Length then
- Result.Current_Length := Llen + 1;
Result.Data (1 .. Llen) := Left.Data (1 .. Llen);
Result.Data (Llen + 1) := Right;
+ Result.Current_Length := Llen + 1;
return Result;
else
@@ -606,10 +627,10 @@ package body Ada.Strings.Superbounded is
return Left;
when Strings.Left =>
- Result.Current_Length := Max_Length;
Result.Data (1 .. Max_Length - 1) :=
Left.Data (2 .. Max_Length);
Result.Data (Max_Length) := Right;
+ Result.Current_Length := Max_Length;
return Result;
when Strings.Error =>
@@ -628,12 +649,10 @@ package body Ada.Strings.Superbounded is
begin
if Llen < Max_Length then
- Source.Current_Length := Llen + 1;
Source.Data (Llen + 1) := New_Item;
+ Source.Current_Length := Llen + 1;
else
- Source.Current_Length := Max_Length;
-
case Drop is
when Strings.Right =>
null;
@@ -663,18 +682,18 @@ package body Ada.Strings.Superbounded is
begin
if Rlen < Max_Length then
- Result.Current_Length := Rlen + 1;
Result.Data (1) := Left;
Result.Data (2 .. Rlen + 1) := Right.Data (1 .. Rlen);
+ Result.Current_Length := Rlen + 1;
return Result;
else
case Drop is
when Strings.Right =>
- Result.Current_Length := Max_Length;
Result.Data (1) := Left;
Result.Data (2 .. Max_Length) :=
Right.Data (1 .. Max_Length - 1);
+ Result.Current_Length := Max_Length;
return Result;
when Strings.Left =>
@@ -696,9 +715,7 @@ package body Ada.Strings.Superbounded is
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
is
begin
- return
- Search.Count
- (Source.Data (1 .. Source.Current_Length), Pattern, Mapping);
+ return Search.Count (Super_To_String (Source), Pattern, Mapping);
end Super_Count;
function Super_Count
@@ -707,9 +724,7 @@ package body Ada.Strings.Superbounded is
Mapping : Maps.Character_Mapping_Function) return Natural
is
begin
- return
- Search.Count
- (Source.Data (1 .. Source.Current_Length), Pattern, Mapping);
+ return Search.Count (Super_To_String (Source), Pattern, Mapping);
end Super_Count;
function Super_Count
@@ -717,7 +732,7 @@ package body Ada.Strings.Superbounded is
Set : Maps.Character_Set) return Natural
is
begin
- return Search.Count (Source.Data (1 .. Source.Current_Length), Set);
+ return Search.Count (Super_To_String (Source), Set);
end Super_Count;
------------------
@@ -737,19 +752,19 @@ package body Ada.Strings.Superbounded is
if Num_Delete <= 0 then
return Source;
- elsif From > Slen + 1 then
+ elsif From - 1 > Slen then
raise Ada.Strings.Index_Error;
elsif Through >= Slen then
- Result.Current_Length := From - 1;
Result.Data (1 .. From - 1) := Source.Data (1 .. From - 1);
+ Result.Current_Length := From - 1;
return Result;
else
- Result.Current_Length := Slen - Num_Delete;
Result.Data (1 .. From - 1) := Source.Data (1 .. From - 1);
- Result.Data (From .. Result.Current_Length) :=
+ Result.Data (From .. Slen - Num_Delete) :=
Source.Data (Through + 1 .. Slen);
+ Result.Current_Length := Slen - Num_Delete;
return Result;
end if;
end Super_Delete;
@@ -766,7 +781,7 @@ package body Ada.Strings.Superbounded is
if Num_Delete <= 0 then
return;
- elsif From > Slen + 1 then
+ elsif From - 1 > Slen then
raise Ada.Strings.Index_Error;
elsif Through >= Slen then
@@ -779,22 +794,6 @@ package body Ada.Strings.Superbounded is
end if;
end Super_Delete;
- -------------------
- -- Super_Element --
- -------------------
-
- function Super_Element
- (Source : Super_String;
- Index : Positive) return Character
- is
- begin
- if Index <= Source.Current_Length then
- return Source.Data (Index);
- else
- raise Strings.Index_Error;
- end if;
- end Super_Element;
-
----------------------
-- Super_Find_Token --
----------------------
@@ -809,7 +808,7 @@ package body Ada.Strings.Superbounded is
is
begin
Search.Find_Token
- (Source.Data (From .. Source.Current_Length), Set, Test, First, Last);
+ (Super_To_String (Source), Set, From, Test, First, Last);
end Super_Find_Token;
procedure Super_Find_Token
@@ -820,8 +819,7 @@ package body Ada.Strings.Superbounded is
Last : out Natural)
is
begin
- Search.Find_Token
- (Source.Data (1 .. Source.Current_Length), Set, Test, First, Last);
+ Search.Find_Token (Super_To_String (Source), Set, Test, First, Last);
end Super_Find_Token;
----------------
@@ -841,21 +839,22 @@ package body Ada.Strings.Superbounded is
begin
if Npad <= 0 then
- Result.Current_Length := Count;
Result.Data (1 .. Count) := Source.Data (1 .. Count);
+ Result.Current_Length := Count;
elsif Count <= Max_Length then
- Result.Current_Length := Count;
Result.Data (1 .. Slen) := Source.Data (1 .. Slen);
Result.Data (Slen + 1 .. Count) := (others => Pad);
+ Result.Current_Length := Count;
else
- Result.Current_Length := Max_Length;
-
case Drop is
when Strings.Right =>
Result.Data (1 .. Slen) := Source.Data (1 .. Slen);
- Result.Data (Slen + 1 .. Max_Length) := (others => Pad);
+
+ if Slen < Max_Length then
+ Result.Data (Slen + 1 .. Max_Length) := (others => Pad);
+ end if;
when Strings.Left =>
if Npad >= Max_Length then
@@ -871,6 +870,8 @@ package body Ada.Strings.Superbounded is
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Result.Current_Length := Max_Length;
end if;
return Result;
@@ -885,22 +886,22 @@ package body Ada.Strings.Superbounded is
Max_Length : constant Positive := Source.Max_Length;
Slen : constant Natural := Source.Current_Length;
Npad : constant Integer := Count - Slen;
- Temp : String (1 .. Max_Length);
+ Temp : Super_String_Data (1 .. Max_Length);
begin
if Npad <= 0 then
Source.Current_Length := Count;
elsif Count <= Max_Length then
- Source.Current_Length := Count;
Source.Data (Slen + 1 .. Count) := (others => Pad);
+ Source.Current_Length := Count;
else
- Source.Current_Length := Max_Length;
-
case Drop is
when Strings.Right =>
- Source.Data (Slen + 1 .. Max_Length) := (others => Pad);
+ if Slen < Max_Length then
+ Source.Data (Slen + 1 .. Max_Length) := (others => Pad);
+ end if;
when Strings.Left =>
if Npad > Max_Length then
@@ -910,15 +911,15 @@ package body Ada.Strings.Superbounded is
Temp := Source.Data;
Source.Data (1 .. Max_Length - Npad) :=
Temp (Count - Max_Length + 1 .. Slen);
-
- for J in Max_Length - Npad + 1 .. Max_Length loop
- Source.Data (J) := Pad;
- end loop;
+ Source.Data (Max_Length - Npad + 1 .. Max_Length) :=
+ (others => Pad);
end if;
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Source.Current_Length := Max_Length;
end if;
end Super_Head;
@@ -933,8 +934,7 @@ package body Ada.Strings.Superbounded is
Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
is
begin
- return Search.Index
- (Source.Data (1 .. Source.Current_Length), Pattern, Going, Mapping);
+ return Search.Index (Super_To_String (Source), Pattern, Going, Mapping);
end Super_Index;
function Super_Index
@@ -944,8 +944,7 @@ package body Ada.Strings.Superbounded is
Mapping : Maps.Character_Mapping_Function) return Natural
is
begin
- return Search.Index
- (Source.Data (1 .. Source.Current_Length), Pattern, Going, Mapping);
+ return Search.Index (Super_To_String (Source), Pattern, Going, Mapping);
end Super_Index;
function Super_Index
@@ -955,8 +954,7 @@ package body Ada.Strings.Superbounded is
Going : Strings.Direction := Strings.Forward) return Natural
is
begin
- return Search.Index
- (Source.Data (1 .. Source.Current_Length), Set, Test, Going);
+ return Search.Index (Super_To_String (Source), Set, Test, Going);
end Super_Index;
function Super_Index
@@ -968,8 +966,7 @@ package body Ada.Strings.Superbounded is
is
begin
return Search.Index
- (Source.Data (1 .. Source.Current_Length),
- Pattern, From, Going, Mapping);
+ (Super_To_String (Source), Pattern, From, Going, Mapping);
end Super_Index;
function Super_Index
@@ -981,8 +978,7 @@ package body Ada.Strings.Superbounded is
is
begin
return Search.Index
- (Source.Data (1 .. Source.Current_Length),
- Pattern, From, Going, Mapping);
+ (Super_To_String (Source), Pattern, From, Going, Mapping);
end Super_Index;
function Super_Index
@@ -993,8 +989,15 @@ package body Ada.Strings.Superbounded is
Going : Direction := Forward) return Natural
is
begin
- return Search.Index
- (Source.Data (1 .. Source.Current_Length), Set, From, Test, Going);
+ return Result : Natural do
+ Result :=
+ Search.Index (Super_To_String (Source), Set, From, Test, Going);
+ pragma Assert
+ (if (for all J in 1 .. Super_Length (Source) =>
+ (if J = From or else (J > From) = (Going = Forward) then
+ (Test = Inside) /= Maps.Is_In (Source.Data (J), Set)))
+ then Result = 0);
+ end return;
end Super_Index;
---------------------------
@@ -1006,9 +1009,7 @@ package body Ada.Strings.Superbounded is
Going : Strings.Direction := Strings.Forward) return Natural
is
begin
- return
- Search.Index_Non_Blank
- (Source.Data (1 .. Source.Current_Length), Going);
+ return Search.Index_Non_Blank (Super_To_String (Source), Going);
end Super_Index_Non_Blank;
function Super_Index_Non_Blank
@@ -1017,9 +1018,7 @@ package body Ada.Strings.Superbounded is
Going : Direction := Forward) return Natural
is
begin
- return
- Search.Index_Non_Blank
- (Source.Data (1 .. Source.Current_Length), From, Going);
+ return Search.Index_Non_Blank (Super_To_String (Source), From, Going);
end Super_Index_Non_Blank;
------------------
@@ -1031,60 +1030,71 @@ package body Ada.Strings.Superbounded is
Before : Positive;
New_Item : String;
Drop : Strings.Truncation := Strings.Error) return Super_String
+ with SPARK_Mode => Off
is
Max_Length : constant Positive := Source.Max_Length;
Result : Super_String (Max_Length);
Slen : constant Natural := Source.Current_Length;
Nlen : constant Natural := New_Item'Length;
- Tlen : constant Natural := Slen + Nlen;
Blen : constant Natural := Before - 1;
Alen : constant Integer := Slen - Blen;
- Droplen : constant Integer := Tlen - Max_Length;
+ Droplen : constant Integer := Slen - Max_Length + Nlen;
- -- Tlen is the length of the total string before possible truncation.
-- Blen, Alen are the lengths of the before and after pieces of the
- -- source string.
+ -- source string. The number of dropped characters is Natural'Max (0,
+ -- Droplen).
begin
if Alen < 0 then
raise Ada.Strings.Index_Error;
elsif Droplen <= 0 then
- Result.Current_Length := Tlen;
Result.Data (1 .. Blen) := Source.Data (1 .. Blen);
- Result.Data (Before .. Before + Nlen - 1) := New_Item;
- Result.Data (Before + Nlen .. Tlen) :=
- Source.Data (Before .. Slen);
+ Result.Data (Before .. Before - 1 + Nlen) :=
+ Super_String_Data (New_Item);
- else
- Result.Current_Length := Max_Length;
+ if Before <= Slen then
+ Result.Data (Before + Nlen .. Slen + Nlen) :=
+ Source.Data (Before .. Slen);
+ end if;
+ Result.Current_Length := Slen + Nlen;
+
+ else
case Drop is
when Strings.Right =>
Result.Data (1 .. Blen) := Source.Data (1 .. Blen);
- if Droplen > Alen then
- Result.Data (Before .. Max_Length) :=
- New_Item (New_Item'First
- .. New_Item'First + Max_Length - Before);
+ if Droplen >= Alen then
+ Result.Data (Before .. Max_Length) := Super_String_Data
+ (New_Item (New_Item'First
+ .. New_Item'First - Before + Max_Length));
+ pragma Assert
+ (String (Result.Data (Before .. Max_Length)) =
+ New_Item (New_Item'First
+ .. New_Item'First - Before + Max_Length));
else
- Result.Data (Before .. Before + Nlen - 1) := New_Item;
+ Result.Data (Before .. Before - 1 + Nlen) :=
+ Super_String_Data (New_Item);
Result.Data (Before + Nlen .. Max_Length) :=
Source.Data (Before .. Slen - Droplen);
end if;
when Strings.Left =>
- Result.Data (Max_Length - (Alen - 1) .. Max_Length) :=
- Source.Data (Before .. Slen);
+ if Alen > 0 then
+ Result.Data (Max_Length - (Alen - 1) .. Max_Length) :=
+ Source.Data (Before .. Slen);
+ end if;
- if Droplen >= Blen then
- Result.Data (1 .. Max_Length - Alen) :=
- New_Item (New_Item'Last - (Max_Length - Alen) + 1
- .. New_Item'Last);
+ if Droplen > Blen then
+ if Alen < Max_Length then
+ Result.Data (1 .. Max_Length - Alen) := Super_String_Data
+ (New_Item (New_Item'Last - (Max_Length - Alen) + 1
+ .. New_Item'Last));
+ end if;
else
- Result.Data
- (Blen - Droplen + 1 .. Max_Length - Alen) :=
- New_Item;
+ Result.Data (Blen - Droplen + 1 .. Max_Length - Alen) :=
+ Super_String_Data (New_Item);
Result.Data (1 .. Blen - Droplen) :=
Source.Data (Droplen + 1 .. Blen);
end if;
@@ -1092,6 +1102,8 @@ package body Ada.Strings.Superbounded is
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Result.Current_Length := Max_Length;
end if;
return Result;
@@ -1111,15 +1123,6 @@ package body Ada.Strings.Superbounded is
Source := Super_Insert (Source, Before, New_Item, Drop);
end Super_Insert;
- ------------------
- -- Super_Length --
- ------------------
-
- function Super_Length (Source : Super_String) return Natural is
- begin
- return Source.Current_Length;
- end Super_Length;
-
---------------------
-- Super_Overwrite --
---------------------
@@ -1132,61 +1135,61 @@ package body Ada.Strings.Superbounded is
is
Max_Length : constant Positive := Source.Max_Length;
Result : Super_String (Max_Length);
- Endpos : constant Natural := Position + New_Item'Length - 1;
Slen : constant Natural := Source.Current_Length;
Droplen : Natural;
begin
- if Position > Slen + 1 then
+ if Position - 1 > Slen then
raise Ada.Strings.Index_Error;
elsif New_Item'Length = 0 then
return Source;
- elsif Endpos <= Slen then
- Result.Current_Length := Source.Current_Length;
+ elsif Position - 1 <= Slen - New_Item'Length then
Result.Data (1 .. Slen) := Source.Data (1 .. Slen);
- Result.Data (Position .. Endpos) := New_Item;
+ Result.Data (Position .. Position - 1 + New_Item'Length) :=
+ Super_String_Data (New_Item);
+ Result.Current_Length := Source.Current_Length;
return Result;
- elsif Endpos <= Max_Length then
- Result.Current_Length := Endpos;
+ elsif Position - 1 <= Max_Length - New_Item'Length then
Result.Data (1 .. Position - 1) := Source.Data (1 .. Position - 1);
- Result.Data (Position .. Endpos) := New_Item;
+ Result.Data (Position .. Position - 1 + New_Item'Length) :=
+ Super_String_Data (New_Item);
+ Result.Current_Length := Position - 1 + New_Item'Length;
return Result;
else
- Result.Current_Length := Max_Length;
- Droplen := Endpos - Max_Length;
+ Droplen := Position - 1 - Max_Length + New_Item'Length;
case Drop is
when Strings.Right =>
Result.Data (1 .. Position - 1) :=
Source.Data (1 .. Position - 1);
- Result.Data (Position .. Max_Length) :=
- New_Item (New_Item'First .. New_Item'Last - Droplen);
- return Result;
+ Result.Data (Position .. Max_Length) := Super_String_Data
+ (New_Item (New_Item'First .. New_Item'Last - Droplen));
when Strings.Left =>
if New_Item'Length >= Max_Length then
- Result.Data (1 .. Max_Length) :=
- New_Item (New_Item'Last - Max_Length + 1 ..
- New_Item'Last);
- return Result;
+ Result.Data (1 .. Max_Length) := Super_String_Data
+ (New_Item (New_Item'Last - Max_Length + 1 ..
+ New_Item'Last));
else
Result.Data (1 .. Max_Length - New_Item'Length) :=
Source.Data (Droplen + 1 .. Position - 1);
Result.Data
(Max_Length - New_Item'Length + 1 .. Max_Length) :=
- New_Item;
- return Result;
+ Super_String_Data (New_Item);
end if;
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Result.Current_Length := Max_Length;
+ return Result;
end if;
end Super_Overwrite;
@@ -1195,50 +1198,52 @@ package body Ada.Strings.Superbounded is
Position : Positive;
New_Item : String;
Drop : Strings.Truncation := Strings.Error)
+ with SPARK_Mode => Off
is
Max_Length : constant Positive := Source.Max_Length;
- Endpos : constant Positive := Position + New_Item'Length - 1;
Slen : constant Natural := Source.Current_Length;
Droplen : Natural;
begin
- if Position > Slen + 1 then
+ if Position - 1 > Slen then
raise Ada.Strings.Index_Error;
- elsif Endpos <= Slen then
- Source.Data (Position .. Endpos) := New_Item;
+ elsif Position - 1 <= Slen - New_Item'Length then
+ Source.Data (Position .. Position - 1 + New_Item'Length) :=
+ Super_String_Data (New_Item);
- elsif Endpos <= Max_Length then
- Source.Data (Position .. Endpos) := New_Item;
- Source.Current_Length := Endpos;
+ elsif Position - 1 <= Max_Length - New_Item'Length then
+ Source.Data (Position .. Position - 1 + New_Item'Length) :=
+ Super_String_Data (New_Item);
+ Source.Current_Length := Position - 1 + New_Item'Length;
else
- Source.Current_Length := Max_Length;
- Droplen := Endpos - Max_Length;
+ Droplen := Position - 1 - Max_Length + New_Item'Length;
case Drop is
when Strings.Right =>
- Source.Data (Position .. Max_Length) :=
- New_Item (New_Item'First .. New_Item'Last - Droplen);
+ Source.Data (Position .. Max_Length) := Super_String_Data
+ (New_Item (New_Item'First .. New_Item'Last - Droplen));
when Strings.Left =>
if New_Item'Length > Max_Length then
- Source.Data (1 .. Max_Length) :=
- New_Item (New_Item'Last - Max_Length + 1 ..
- New_Item'Last);
+ Source.Data (1 .. Max_Length) := Super_String_Data
+ (New_Item
+ (New_Item'Last - Max_Length + 1 .. New_Item'Last));
else
Source.Data (1 .. Max_Length - New_Item'Length) :=
Source.Data (Droplen + 1 .. Position - 1);
-
Source.Data
(Max_Length - New_Item'Length + 1 .. Max_Length) :=
- New_Item;
+ Super_String_Data (New_Item);
end if;
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Source.Current_Length := Max_Length;
end if;
end Super_Overwrite;
@@ -1269,12 +1274,13 @@ package body Ada.Strings.Superbounded is
High : Natural;
By : String;
Drop : Strings.Truncation := Strings.Error) return Super_String
+ with SPARK_Mode => Off
is
Max_Length : constant Positive := Source.Max_Length;
Slen : constant Natural := Source.Current_Length;
begin
- if Low > Slen + 1 then
+ if Low - 1 > Slen then
raise Strings.Index_Error;
elsif High < Low then
@@ -1282,51 +1288,58 @@ package body Ada.Strings.Superbounded is
else
declare
- Blen : constant Natural := Natural'Max (0, Low - 1);
+ Blen : constant Natural := Low - 1;
Alen : constant Natural := Natural'Max (0, Slen - High);
- Tlen : constant Natural := Blen + By'Length + Alen;
- Droplen : constant Integer := Tlen - Max_Length;
+ Droplen : constant Integer := Blen + Alen - Max_Length + By'Length;
Result : Super_String (Max_Length);
- -- Tlen is the total length of the result string before any
- -- truncation. Blen and Alen are the lengths of the pieces
- -- of the original string that end up in the result string
- -- before and after the replaced slice.
+ -- Blen and Alen are the lengths of the pieces of the original
+ -- string that end up in the result string before and after the
+ -- replaced slice. The number of dropped characters is Natural'Max
+ -- (0, Droplen).
begin
if Droplen <= 0 then
- Result.Current_Length := Tlen;
Result.Data (1 .. Blen) := Source.Data (1 .. Blen);
- Result.Data (Low .. Low + By'Length - 1) := By;
- Result.Data (Low + By'Length .. Tlen) :=
- Source.Data (High + 1 .. Slen);
+ Result.Data (Low .. Blen + By'Length) :=
+ Super_String_Data (By);
- else
- Result.Current_Length := Max_Length;
+ if Alen > 0 then
+ Result.Data (Low + By'Length .. Blen + By'Length + Alen) :=
+ Source.Data (High + 1 .. Slen);
+ end if;
+ Result.Current_Length := Blen + By'Length + Alen;
+
+ else
case Drop is
when Strings.Right =>
Result.Data (1 .. Blen) := Source.Data (1 .. Blen);
- if Droplen > Alen then
- Result.Data (Low .. Max_Length) :=
- By (By'First .. By'First + Max_Length - Low);
+ if Droplen >= Alen then
+ Result.Data (Low .. Max_Length) := Super_String_Data
+ (By (By'First .. By'First - Low + Max_Length));
else
- Result.Data (Low .. Low + By'Length - 1) := By;
+ Result.Data (Low .. Low - 1 + By'Length) :=
+ Super_String_Data (By);
Result.Data (Low + By'Length .. Max_Length) :=
Source.Data (High + 1 .. Slen - Droplen);
end if;
when Strings.Left =>
- Result.Data (Max_Length - (Alen - 1) .. Max_Length) :=
- Source.Data (High + 1 .. Slen);
+ if Alen > 0 then
+ Result.Data (Max_Length - (Alen - 1) .. Max_Length) :=
+ Source.Data (High + 1 .. Slen);
+ end if;
if Droplen >= Blen then
Result.Data (1 .. Max_Length - Alen) :=
- By (By'Last - (Max_Length - Alen) + 1 .. By'Last);
+ Super_String_Data (By
+ (By'Last - (Max_Length - Alen) + 1 .. By'Last));
else
Result.Data
- (Blen - Droplen + 1 .. Max_Length - Alen) := By;
+ (Blen - Droplen + 1 .. Max_Length - Alen) :=
+ Super_String_Data (By);
Result.Data (1 .. Blen - Droplen) :=
Source.Data (Droplen + 1 .. Blen);
end if;
@@ -1334,6 +1347,8 @@ package body Ada.Strings.Superbounded is
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Result.Current_Length := Max_Length;
end if;
return Result;
@@ -1370,16 +1385,17 @@ package body Ada.Strings.Superbounded is
begin
if Count <= Max_Length then
+ Result.Data (1 .. Count) := (others => Item);
Result.Current_Length := Count;
elsif Drop = Strings.Error then
raise Ada.Strings.Length_Error;
else
+ Result.Data (1 .. Max_Length) := (others => Item);
Result.Current_Length := Max_Length;
end if;
- Result.Data (1 .. Result.Current_Length) := (others => Item);
return Result;
end Super_Replicate;
@@ -1389,52 +1405,203 @@ package body Ada.Strings.Superbounded is
Drop : Truncation := Error;
Max_Length : Positive) return Super_String
is
- Length : constant Integer := Count * Item'Length;
Result : Super_String (Max_Length);
- Indx : Positive;
+ Indx : Natural;
+ Ilen : constant Natural := Item'Length;
+
+ -- Parts of the proof involving manipulations with the modulo operator
+ -- are complicated for the prover and can't be done automatically in
+ -- the global subprogram. That's why we isolate them in these two ghost
+ -- lemmas.
+
+ procedure Lemma_Mod (K : Natural; Q : Natural) with
+ Ghost,
+ Pre => Ilen /= 0
+ and then Q mod Ilen = 0
+ and then K - Q in 0 .. Ilen - 1,
+ Post => K mod Ilen = K - Q;
+ -- Lemma_Mod is applied to an index considered in Lemma_Split to prove
+ -- that it has the right value modulo Item'Length.
+
+ procedure Lemma_Mod_Zero (X : Natural) with
+ Ghost,
+ Pre => Ilen /= 0
+ and then X mod Ilen = 0
+ and then X <= Natural'Last - Ilen,
+ Post => (X + Ilen) mod Ilen = 0;
+ -- Lemma_Mod_Zero is applied to prove that the length of the range
+ -- of indexes considered in the loop, when dropping on the Left, is
+ -- a multiple of Item'Length.
+
+ procedure Lemma_Split (Going : Direction) with
+ Ghost,
+ Pre =>
+ Ilen /= 0
+ and then Indx in 0 .. Max_Length - Ilen
+ and then
+ (if Going = Forward
+ then Indx mod Ilen = 0
+ else (Max_Length - Indx - Ilen) mod Ilen = 0)
+ and then Result.Data (Indx + 1 .. Indx + Ilen)'Initialized
+ and then String (Result.Data (Indx + 1 .. Indx + Ilen)) = Item,
+ Post =>
+ (if Going = Forward then
+ (for all J in Indx + 1 .. Indx + Ilen =>
+ Result.Data (J) = Item (Item'First + (J - 1) mod Ilen))
+ else
+ (for all J in Indx + 1 .. Indx + Ilen =>
+ Result.Data (J) =
+ Item (Item'Last - (Max_Length - J) mod Ilen)));
+ -- Lemma_Split is used after Result.Data (Indx + 1 .. Indx + Ilen) is
+ -- updated to Item and concludes that the characters match for each
+ -- index when taken modulo Item'Length, as the considered slice starts
+ -- at index 1 (or ends at index Max_Length, if Going = Backward) modulo
+ -- Item'Length.
+
+ ---------------
+ -- Lemma_Mod --
+ ---------------
+
+ procedure Lemma_Mod (K : Natural; Q : Natural) is null;
+
+ --------------------
+ -- Lemma_Mod_Zero --
+ --------------------
+
+ procedure Lemma_Mod_Zero (X : Natural) is null;
+
+ -----------------
+ -- Lemma_Split --
+ -----------------
+
+ procedure Lemma_Split (Going : Direction) is
+ begin
+ if Going = Forward then
+ for K in Indx + 1 .. Indx + Ilen loop
+ Lemma_Mod (K - 1, Indx);
+ pragma Loop_Invariant
+ (for all J in Indx + 1 .. K =>
+ Result.Data (J) = Item (Item'First + (J - 1) mod Ilen));
+ end loop;
+ else
+ for K in Indx + 1 .. Indx + Ilen loop
+ Lemma_Mod (Max_Length - K, Max_Length - Indx - Ilen);
+ pragma Loop_Invariant
+ (for all J in Indx + 1 .. K =>
+ Result.Data (J) =
+ Item (Item'Last - (Max_Length - J) mod Ilen));
+ end loop;
+ end if;
+ end Lemma_Split;
begin
- if Length <= Max_Length then
- Result.Current_Length := Length;
-
- if Length > 0 then
- Indx := 1;
+ if Count = 0 or else Ilen <= Max_Length / Count then
+ if Count * Ilen > 0 then
+ Indx := 0;
for J in 1 .. Count loop
- Result.Data (Indx .. Indx + Item'Length - 1) := Item;
- Indx := Indx + Item'Length;
+ Result.Data (Indx + 1 .. Indx + Ilen) :=
+ Super_String_Data (Item);
+ pragma Assert
+ (for all K in 1 .. Ilen =>
+ Result.Data (Indx + K) = Item (Item'First - 1 + K));
+ pragma Assert
+ (String (Result.Data (Indx + 1 .. Indx + Ilen)) = Item);
+ Lemma_Split (Forward);
+ Indx := Indx + Ilen;
+ pragma Loop_Invariant (Indx = J * Ilen);
+ pragma Loop_Invariant (Result.Data (1 .. Indx)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. Indx =>
+ Result.Data (K) =
+ Item (Item'First + (K - 1) mod Ilen));
end loop;
end if;
- else
- Result.Current_Length := Max_Length;
+ Result.Current_Length := Count * Ilen;
+ else
case Drop is
when Strings.Right =>
- Indx := 1;
-
- while Indx + Item'Length <= Max_Length + 1 loop
- Result.Data (Indx .. Indx + Item'Length - 1) := Item;
- Indx := Indx + Item'Length;
+ Indx := 0;
+
+ while Indx < Max_Length - Ilen loop
+ Result.Data (Indx + 1 .. Indx + Ilen) :=
+ Super_String_Data (Item);
+ pragma Assert
+ (for all K in 1 .. Ilen =>
+ Result.Data (Indx + K) = Item (Item'First - 1 + K));
+ pragma Assert
+ (String (Result.Data (Indx + 1 .. Indx + Ilen)) = Item);
+ Lemma_Split (Forward);
+ Indx := Indx + Ilen;
+ pragma Loop_Invariant (Indx mod Ilen = 0);
+ pragma Loop_Invariant (Indx in 0 .. Max_Length - 1);
+ pragma Loop_Invariant (Result.Data (1 .. Indx)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. Indx =>
+ Result.Data (K) =
+ Item (Item'First + (K - 1) mod Ilen));
end loop;
- Result.Data (Indx .. Max_Length) :=
- Item (Item'First .. Item'First + Max_Length - Indx);
+ Result.Data (Indx + 1 .. Max_Length) := Super_String_Data
+ (Item (Item'First .. Item'First + (Max_Length - Indx - 1)));
+ pragma Assert
+ (for all J in Indx + 1 .. Max_Length =>
+ Result.Data (J) = Item (Item'First - 1 - Indx + J));
+
+ for J in Indx + 1 .. Max_Length loop
+ Lemma_Mod (J - 1, Indx);
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ Result.Data (K) =
+ Item (Item'First + (K - 1) mod Ilen));
+ end loop;
when Strings.Left =>
Indx := Max_Length;
- while Indx - Item'Length >= 1 loop
- Result.Data (Indx - (Item'Length - 1) .. Indx) := Item;
- Indx := Indx - Item'Length;
+ while Indx > Ilen loop
+ Indx := Indx - Ilen;
+ Result.Data (Indx + 1 .. Indx + Ilen) :=
+ Super_String_Data (Item);
+ pragma Assert
+ (for all K in 1 .. Ilen =>
+ Result.Data (Indx + K) = Item (Item'First - 1 + K));
+ pragma Assert
+ (String (Result.Data (Indx + 1 .. Indx + Ilen)) = Item);
+ Lemma_Split (Backward);
+ Lemma_Mod_Zero (Max_Length - Indx - Ilen);
+ pragma Loop_Invariant
+ ((Max_Length - Indx) mod Ilen = 0);
+ pragma Loop_Invariant (Indx in 1 .. Max_Length);
+ pragma Loop_Invariant
+ (Result.Data (Indx + 1 .. Max_Length)'Initialized);
+ pragma Loop_Invariant
+ (for all K in Indx + 1 .. Max_Length =>
+ Result.Data (K) =
+ Item (Item'Last - (Max_Length - K) mod Ilen));
end loop;
Result.Data (1 .. Indx) :=
- Item (Item'Last - Indx + 1 .. Item'Last);
+ Super_String_Data (Item (Item'Last - Indx + 1 .. Item'Last));
+ pragma Assert
+ (for all J in 1 .. Indx =>
+ Result.Data (J) = Item (Item'Last - Indx + J));
+
+ for J in reverse 1 .. Indx loop
+ Lemma_Mod (Max_Length - J, Max_Length - Indx);
+ pragma Loop_Invariant
+ (for all K in J .. Max_Length =>
+ Result.Data (K) =
+ Item (Item'Last - (Max_Length - K) mod Ilen));
+ end loop;
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Result.Current_Length := Max_Length;
end if;
return Result;
@@ -1447,39 +1614,13 @@ package body Ada.Strings.Superbounded is
is
begin
return
- Super_Replicate
- (Count,
- Item.Data (1 .. Item.Current_Length),
- Drop,
- Item.Max_Length);
+ Super_Replicate (Count, Super_To_String (Item), Drop, Item.Max_Length);
end Super_Replicate;
-----------------
-- Super_Slice --
-----------------
- function Super_Slice
- (Source : Super_String;
- Low : Positive;
- High : Natural) return String
- is
- begin
- -- Note: test of High > Length is in accordance with AI95-00128
-
- return R : String (Low .. High) do
- if Low > Source.Current_Length + 1
- or else High > Source.Current_Length
- then
- raise Index_Error;
- end if;
-
- -- Note: in this case, superflat bounds are not a problem, we just
- -- get the null string in accordance with normal Ada slice rules.
-
- R := Source.Data (Low .. High);
- end return;
- end Super_Slice;
-
function Super_Slice
(Source : Super_String;
Low : Positive;
@@ -1487,16 +1628,16 @@ package body Ada.Strings.Superbounded is
is
begin
return Result : Super_String (Source.Max_Length) do
- if Low > Source.Current_Length + 1
+ if Low - 1 > Source.Current_Length
or else High > Source.Current_Length
then
raise Index_Error;
end if;
- -- Note: the Max operation here deals with the superflat case
-
- Result.Current_Length := Integer'Max (0, High - Low + 1);
- Result.Data (1 .. Result.Current_Length) := Source.Data (Low .. High);
+ if High >= Low then
+ Result.Data (1 .. High - Low + 1) := Source.Data (Low .. High);
+ Result.Current_Length := High - Low + 1;
+ end if;
end return;
end Super_Slice;
@@ -1507,16 +1648,18 @@ package body Ada.Strings.Superbounded is
High : Natural)
is
begin
- if Low > Source.Current_Length + 1
+ if Low - 1 > Source.Current_Length
or else High > Source.Current_Length
then
raise Index_Error;
end if;
- -- Note: the Max operation here deals with the superflat case
-
- Target.Current_Length := Integer'Max (0, High - Low + 1);
- Target.Data (1 .. Target.Current_Length) := Source.Data (Low .. High);
+ if High >= Low then
+ Target.Data (1 .. High - Low + 1) := Source.Data (Low .. High);
+ Target.Current_Length := High - Low + 1;
+ else
+ Target.Current_Length := 0;
+ end if;
end Super_Slice;
----------------
@@ -1536,18 +1679,22 @@ package body Ada.Strings.Superbounded is
begin
if Npad <= 0 then
- Result.Current_Length := Count;
- Result.Data (1 .. Count) :=
- Source.Data (Slen - (Count - 1) .. Slen);
+ if Count > 0 then
+ Result.Data (1 .. Count) :=
+ Source.Data (Slen - (Count - 1) .. Slen);
+ Result.Current_Length := Count;
+ end if;
elsif Count <= Max_Length then
- Result.Current_Length := Count;
Result.Data (1 .. Npad) := (others => Pad);
- Result.Data (Npad + 1 .. Count) := Source.Data (1 .. Slen);
- else
- Result.Current_Length := Max_Length;
+ if Slen > 0 then
+ Result.Data (Npad + 1 .. Count) := Source.Data (1 .. Slen);
+ end if;
+
+ Result.Current_Length := Count;
+ else
case Drop is
when Strings.Right =>
if Npad >= Max_Length then
@@ -1567,6 +1714,8 @@ package body Ada.Strings.Superbounded is
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Result.Current_Length := Max_Length;
end if;
return Result;
@@ -1582,22 +1731,27 @@ package body Ada.Strings.Superbounded is
Slen : constant Natural := Source.Current_Length;
Npad : constant Integer := Count - Slen;
- Temp : constant String (1 .. Max_Length) := Source.Data;
+ Temp : constant Super_String_Data (1 .. Max_Length) := Source.Data;
begin
if Npad <= 0 then
Source.Current_Length := Count;
- Source.Data (1 .. Count) :=
- Temp (Slen - (Count - 1) .. Slen);
+
+ if Count > 0 then
+ Source.Data (1 .. Count) :=
+ Temp (Slen - (Count - 1) .. Slen);
+ end if;
elsif Count <= Max_Length then
- Source.Current_Length := Count;
Source.Data (1 .. Npad) := (others => Pad);
- Source.Data (Npad + 1 .. Count) := Temp (1 .. Slen);
- else
- Source.Current_Length := Max_Length;
+ if Slen > 0 then
+ Source.Data (Npad + 1 .. Count) := Temp (1 .. Slen);
+ end if;
+ Source.Current_Length := Count;
+
+ else
case Drop is
when Strings.Right =>
if Npad >= Max_Length then
@@ -1610,30 +1764,18 @@ package body Ada.Strings.Superbounded is
end if;
when Strings.Left =>
- for J in 1 .. Max_Length - Slen loop
- Source.Data (J) := Pad;
- end loop;
-
+ Source.Data (1 .. Max_Length - Slen) := (others => Pad);
Source.Data (Max_Length - Slen + 1 .. Max_Length) :=
Temp (1 .. Slen);
when Strings.Error =>
raise Ada.Strings.Length_Error;
end case;
+
+ Source.Current_Length := Max_Length;
end if;
end Super_Tail;
- ---------------------
- -- Super_To_String --
- ---------------------
-
- function Super_To_String (Source : Super_String) return String is
- begin
- return R : String (1 .. Source.Current_Length) do
- R := Source.Data (1 .. Source.Current_Length);
- end return;
- end Super_To_String;
-
---------------------
-- Super_Translate --
---------------------
@@ -1645,12 +1787,15 @@ package body Ada.Strings.Superbounded is
Result : Super_String (Source.Max_Length);
begin
- Result.Current_Length := Source.Current_Length;
-
for J in 1 .. Source.Current_Length loop
Result.Data (J) := Value (Mapping, Source.Data (J));
+ pragma Loop_Invariant (Result.Data (1 .. J)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ Result.Data (K) = Value (Mapping, Source.Data (K)));
end loop;
+ Result.Current_Length := Source.Current_Length;
return Result;
end Super_Translate;
@@ -1661,6 +1806,9 @@ package body Ada.Strings.Superbounded is
begin
for J in 1 .. Source.Current_Length loop
Source.Data (J) := Value (Mapping, Source.Data (J));
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ Source.Data (K) = Value (Mapping, Source'Loop_Entry.Data (K)));
end loop;
end Super_Translate;
@@ -1671,12 +1819,15 @@ package body Ada.Strings.Superbounded is
Result : Super_String (Source.Max_Length);
begin
- Result.Current_Length := Source.Current_Length;
-
for J in 1 .. Source.Current_Length loop
Result.Data (J) := Mapping.all (Source.Data (J));
+ pragma Loop_Invariant (Result.Data (1 .. J)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ Result.Data (K) = Mapping (Source.Data (K)));
end loop;
+ Result.Current_Length := Source.Current_Length;
return Result;
end Super_Translate;
@@ -1687,6 +1838,9 @@ package body Ada.Strings.Superbounded is
begin
for J in 1 .. Source.Current_Length loop
Source.Data (J) := Mapping.all (Source.Data (J));
+ pragma Loop_Invariant
+ (for all K in 1 .. J =>
+ Source.Data (K) = Mapping (Source'Loop_Entry.Data (K)));
end loop;
end Super_Translate;
@@ -1699,24 +1853,62 @@ package body Ada.Strings.Superbounded is
Side : Trim_End) return Super_String
is
Result : Super_String (Source.Max_Length);
- Last : Natural := Source.Current_Length;
- First : Positive := 1;
+ Last : constant Natural := Source.Current_Length;
begin
- if Side = Left or else Side = Both then
- while First <= Last and then Source.Data (First) = ' ' loop
- First := First + 1;
- end loop;
- end if;
+ case Side is
+ when Strings.Left =>
+ declare
+ Low : constant Natural :=
+ Super_Index_Non_Blank (Source, Forward);
+ begin
+ -- All blanks case
- if Side = Right or else Side = Both then
- while Last >= First and then Source.Data (Last) = ' ' loop
- Last := Last - 1;
- end loop;
- end if;
+ if Low = 0 then
+ return Result;
+ end if;
+
+ Result.Data (1 .. Last - Low + 1) := Source.Data (Low .. Last);
+ Result.Current_Length := Last - Low + 1;
+ end;
+
+ when Strings.Right =>
+ declare
+ High : constant Natural :=
+ Super_Index_Non_Blank (Source, Backward);
+ begin
+ -- All blanks case
+
+ if High = 0 then
+ return Result;
+ end if;
+
+ Result.Data (1 .. High) := Source.Data (1 .. High);
+ Result.Current_Length := High;
+ end;
+
+ when Strings.Both =>
+ declare
+ Low : constant Natural :=
+ Super_Index_Non_Blank (Source, Forward);
+ begin
+ -- All blanks case
+
+ if Low = 0 then
+ return Result;
+ end if;
+
+ declare
+ High : constant Natural :=
+ Super_Index_Non_Blank (Source, Backward);
+ begin
+ Result.Data (1 .. High - Low + 1) :=
+ Source.Data (Low .. High);
+ Result.Current_Length := High - Low + 1;
+ end;
+ end;
+ end case;
- Result.Current_Length := Last - First + 1;
- Result.Data (1 .. Result.Current_Length) := Source.Data (First .. Last);
return Result;
end Super_Trim;
@@ -1724,28 +1916,54 @@ package body Ada.Strings.Superbounded is
(Source : in out Super_String;
Side : Trim_End)
is
- Max_Length : constant Positive := Source.Max_Length;
- Last : Natural := Source.Current_Length;
- First : Positive := 1;
- Temp : String (1 .. Max_Length);
-
+ Last : constant Natural := Source.Current_Length;
begin
- Temp (1 .. Last) := Source.Data (1 .. Last);
-
- if Side = Left or else Side = Both then
- while First <= Last and then Temp (First) = ' ' loop
- First := First + 1;
- end loop;
- end if;
+ case Side is
+ when Strings.Left =>
+ declare
+ Low : constant Natural :=
+ Super_Index_Non_Blank (Source, Forward);
+ begin
+ -- All blanks case
- if Side = Right or else Side = Both then
- while Last >= First and then Temp (Last) = ' ' loop
- Last := Last - 1;
- end loop;
- end if;
-
- Source.Current_Length := Last - First + 1;
- Source.Data (1 .. Source.Current_Length) := Temp (First .. Last);
+ if Low = 0 then
+ Source.Current_Length := 0;
+ else
+ Source.Data (1 .. Last - Low + 1) :=
+ Source.Data (Low .. Last);
+ Source.Current_Length := Last - Low + 1;
+ end if;
+ end;
+
+ when Strings.Right =>
+ declare
+ High : constant Natural :=
+ Super_Index_Non_Blank (Source, Backward);
+ begin
+ Source.Current_Length := High;
+ end;
+
+ when Strings.Both =>
+ declare
+ Low : constant Natural :=
+ Super_Index_Non_Blank (Source, Forward);
+ begin
+ -- All blanks case
+
+ if Low = 0 then
+ Source.Current_Length := 0;
+ else
+ declare
+ High : constant Natural :=
+ Super_Index_Non_Blank (Source, Backward);
+ begin
+ Source.Data (1 .. High - Low + 1) :=
+ Source.Data (Low .. High);
+ Source.Current_Length := High - Low + 1;
+ end;
+ end if;
+ end;
+ end case;
end Super_Trim;
function Super_Trim
@@ -1754,22 +1972,31 @@ package body Ada.Strings.Superbounded is
Right : Maps.Character_Set) return Super_String
is
Result : Super_String (Source.Max_Length);
+ Low : Natural;
+ High : Natural;
begin
- for First in 1 .. Source.Current_Length loop
- if not Is_In (Source.Data (First), Left) then
- for Last in reverse First .. Source.Current_Length loop
- if not Is_In (Source.Data (Last), Right) then
- Result.Current_Length := Last - First + 1;
- Result.Data (1 .. Result.Current_Length) :=
- Source.Data (First .. Last);
- return Result;
- end if;
- end loop;
- end if;
- end loop;
+ Low := Super_Index (Source, Left, Outside, Forward);
+
+ -- Case where source comprises only characters in Left
+
+ if Low = 0 then
+ return Result;
+ end if;
+
+ High := Super_Index (Source, Right, Outside, Backward);
+
+ -- Case where source comprises only characters in Right
+
+ if High = 0 then
+ return Result;
+ end if;
+
+ if High >= Low then
+ Result.Data (1 .. High - Low + 1) := Source.Data (Low .. High);
+ Result.Current_Length := High - Low + 1;
+ end if;
- Result.Current_Length := 0;
return Result;
end Super_Trim;
@@ -1778,29 +2005,39 @@ package body Ada.Strings.Superbounded is
Left : Maps.Character_Set;
Right : Maps.Character_Set)
is
+ Last : constant Natural := Source.Current_Length;
+ Temp : Super_String_Data (1 .. Last);
+ Low : Natural;
+ High : Natural;
+
begin
- for First in 1 .. Source.Current_Length loop
- if not Is_In (Source.Data (First), Left) then
- for Last in reverse First .. Source.Current_Length loop
- if not Is_In (Source.Data (Last), Right) then
- if First = 1 then
- Source.Current_Length := Last;
- return;
- else
- Source.Current_Length := Last - First + 1;
- Source.Data (1 .. Source.Current_Length) :=
- Source.Data (First .. Last);
- return;
- end if;
- end if;
- end loop;
+ Temp := Source.Data (1 .. Last);
+ Low := Super_Index (Source, Left, Outside, Forward);
+
+ -- Case where source comprises only characters in Left
+
+ if Low = 0 then
+ Source.Current_Length := 0;
+
+ else
+ High := Super_Index (Source, Right, Outside, Backward);
+ -- Case where source comprises only characters in Right
+
+ if High = 0 then
Source.Current_Length := 0;
- return;
- end if;
- end loop;
- Source.Current_Length := 0;
+ elsif Low = 1 then
+ Source.Current_Length := High;
+
+ elsif High < Low then
+ Source.Current_Length := 0;
+
+ else
+ Source.Data (1 .. High - Low + 1) := Temp (Low .. High);
+ Source.Current_Length := High - Low + 1;
+ end if;
+ end if;
end Super_Trim;
-----------
@@ -1819,11 +2056,14 @@ package body Ada.Strings.Superbounded is
raise Ada.Strings.Length_Error;
else
- Result.Current_Length := Left;
-
for J in 1 .. Left loop
Result.Data (J) := Right;
+ pragma Loop_Invariant (Result.Data (1 .. J)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. J => Result.Data (K) = Right);
end loop;
+
+ Result.Current_Length := Left;
end if;
return Result;
@@ -1835,23 +2075,88 @@ package body Ada.Strings.Superbounded is
Max_Length : Positive) return Super_String
is
Result : Super_String (Max_Length);
- Pos : Positive := 1;
+ Pos : Natural := 0;
Rlen : constant Natural := Right'Length;
Nlen : constant Natural := Left * Rlen;
+ -- Parts of the proof involving manipulations with the modulo operator
+ -- are complicated for the prover and can't be done automatically in
+ -- the global subprogram. That's why we isolate them in these two ghost
+ -- lemmas.
+
+ procedure Lemma_Mod (K : Integer) with
+ Ghost,
+ Pre =>
+ Rlen /= 0
+ and then Pos mod Rlen = 0
+ and then Pos in 0 .. Max_Length - Rlen
+ and then K in Pos .. Pos + Rlen - 1,
+ Post => K mod Rlen = K - Pos;
+ -- Lemma_Mod is applied to an index considered in Lemma_Split to prove
+ -- that it has the right value modulo Right'Length.
+
+ procedure Lemma_Split with
+ Ghost,
+ Pre =>
+ Rlen /= 0
+ and then Pos mod Rlen = 0
+ and then Pos in 0 .. Max_Length - Rlen
+ and then Result.Data (1 .. Pos + Rlen)'Initialized
+ and then String (Result.Data (Pos + 1 .. Pos + Rlen)) = Right,
+ Post =>
+ (for all K in Pos + 1 .. Pos + Rlen =>
+ Result.Data (K) = Right (Right'First + (K - 1) mod Rlen));
+ -- Lemma_Split is used after Result.Data (Pos + 1 .. Pos + Rlen) is
+ -- updated to Right and concludes that the characters match for each
+ -- index when taken modulo Right'Length, as the considered slice starts
+ -- at index 1 modulo Right'Length.
+
+ ---------------
+ -- Lemma_Mod --
+ ---------------
+
+ procedure Lemma_Mod (K : Integer) is null;
+
+ -----------------
+ -- Lemma_Split --
+ -----------------
+
+ procedure Lemma_Split is
+ begin
+ for K in Pos + 1 .. Pos + Rlen loop
+ Lemma_Mod (K - 1);
+ pragma Loop_Invariant
+ (for all J in Pos + 1 .. K =>
+ Result.Data (J) = Right (Right'First + (J - 1) mod Rlen));
+ end loop;
+ end Lemma_Split;
+
begin
if Nlen > Max_Length then
raise Ada.Strings.Length_Error;
else
- Result.Current_Length := Nlen;
-
if Nlen > 0 then
for J in 1 .. Left loop
- Result.Data (Pos .. Pos + Rlen - 1) := Right;
+ Result.Data (Pos + 1 .. Pos + Rlen) :=
+ Super_String_Data (Right);
+ pragma Assert
+ (for all K in 1 .. Rlen => Result.Data (Pos + K) =
+ Right (Right'First - 1 + K));
+ pragma Assert
+ (String (Result.Data (Pos + 1 .. Pos + Rlen)) = Right);
+ Lemma_Split;
Pos := Pos + Rlen;
+ pragma Loop_Invariant (Pos = J * Rlen);
+ pragma Loop_Invariant (Result.Data (1 .. Pos)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. Pos =>
+ Result.Data (K) =
+ Right (Right'First + (K - 1) mod Rlen));
end loop;
end if;
+
+ Result.Current_Length := Nlen;
end if;
return Result;
@@ -1862,7 +2167,7 @@ package body Ada.Strings.Superbounded is
Right : Super_String) return Super_String
is
Result : Super_String (Right.Max_Length);
- Pos : Positive := 1;
+ Pos : Natural := 0;
Rlen : constant Natural := Right.Current_Length;
Nlen : constant Natural := Left * Rlen;
@@ -1871,15 +2176,21 @@ package body Ada.Strings.Superbounded is
raise Ada.Strings.Length_Error;
else
- Result.Current_Length := Nlen;
-
if Nlen > 0 then
for J in 1 .. Left loop
- Result.Data (Pos .. Pos + Rlen - 1) :=
+ Result.Data (Pos + 1 .. Pos + Rlen) :=
Right.Data (1 .. Rlen);
Pos := Pos + Rlen;
+ pragma Loop_Invariant (Pos = J * Rlen);
+ pragma Loop_Invariant (Result.Data (1 .. Pos)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. Pos =>
+ Result.Data (K) =
+ Right.Data (1 + (K - 1) mod Rlen));
end loop;
end if;
+
+ Result.Current_Length := Nlen;
end if;
return Result;
@@ -1891,7 +2202,7 @@ package body Ada.Strings.Superbounded is
function To_Super_String
(Source : String;
- Max_Length : Natural;
+ Max_Length : Positive;
Drop : Truncation := Error) return Super_String
is
Result : Super_String (Max_Length);
@@ -1899,20 +2210,20 @@ package body Ada.Strings.Superbounded is
begin
if Slen <= Max_Length then
+ Result.Data (1 .. Slen) := Super_String_Data (Source);
Result.Current_Length := Slen;
- Result.Data (1 .. Slen) := Source;
else
case Drop is
when Strings.Right =>
+ Result.Data (1 .. Max_Length) := Super_String_Data
+ (Source (Source'First .. Source'First - 1 + Max_Length));
Result.Current_Length := Max_Length;
- Result.Data (1 .. Max_Length) :=
- Source (Source'First .. Source'First - 1 + Max_Length);
when Strings.Left =>
+ Result.Data (1 .. Max_Length) := Super_String_Data
+ (Source (Source'Last - (Max_Length - 1) .. Source'Last));
Result.Current_Length := Max_Length;
- Result.Data (1 .. Max_Length) :=
- Source (Source'Last - (Max_Length - 1) .. Source'Last);
when Strings.Error =>
raise Ada.Strings.Length_Error;
diff --git a/gcc/ada/libgnat/a-strsup.ads b/gcc/ada/libgnat/a-strsup.ads
index 9e568a82975..7428e9c2cd7 100644
--- a/gcc/ada/libgnat/a-strsup.ads
+++ b/gcc/ada/libgnat/a-strsup.ads
@@ -36,28 +36,47 @@
-- length as the discriminant. Individual instantiations of Strings.Bounded
-- use this type with an appropriate discriminant value set.
-with Ada.Strings.Maps;
+-- Preconditions in this unit are meant for analysis only, not for run-time
+-- checking, so that the expected exceptions are raised. This is enforced by
+-- setting the corresponding assertion policy to Ignore. Postconditions and
+-- contract cases should not be executed at runtime as well, in order not to
+-- slow down the execution of these functions.
-package Ada.Strings.Superbounded is
+pragma Assertion_Policy (Pre => Ignore,
+ Post => Ignore,
+ Contract_Cases => Ignore,
+ Ghost => Ignore);
+
+with Ada.Strings.Maps; use type Ada.Strings.Maps.Character_Mapping_Function;
+with Ada.Strings.Search;
+
+package Ada.Strings.Superbounded with SPARK_Mode is
pragma Preelaborate;
-- Type Bounded_String in Ada.Strings.Bounded.Generic_Bounded_Length is
-- derived from Super_String, with the constraint of the maximum length.
+ type Super_String_Data is new String with Relaxed_Initialization;
+
type Super_String (Max_Length : Positive) is record
Current_Length : Natural := 0;
- Data : String (1 .. Max_Length);
+ Data : Super_String_Data (1 .. Max_Length);
-- A previous version had a default initial value for Data, which is
-- no longer necessary, because we now special-case this type in the
-- compiler, so "=" composes properly for descendants of this type.
-- Leaving it out is more efficient.
- end record;
+ end record
+ with
+ Predicate =>
+ Current_Length <= Max_Length
+ and then Data (1 .. Current_Length)'Initialized;
-- The subprograms defined for Super_String are similar to those
-- defined for Bounded_String, except that they have different names, so
-- that they can be renamed in Ada.Strings.Bounded.Generic_Bounded_Length.
- function Super_Length (Source : Super_String) return Natural;
+ function Super_Length (Source : Super_String) return Natural
+ is (Source.Current_Length);
--------------------------------------------------------
-- Conversion, Concatenation, and Selection Functions --
@@ -65,109 +84,606 @@ package Ada.Strings.Superbounded is
function To_Super_String
(Source : String;
- Max_Length : Natural;
- Drop : Truncation := Error) return Super_String;
+ Max_Length : Positive;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre => (if Source'Length > Max_Length then Drop /= Error),
+ Post => To_Super_String'Result.Max_Length = Max_Length,
+ Contract_Cases =>
+ (Source'Length <= Max_Length
+ =>
+ Super_To_String (To_Super_String'Result) = Source,
+
+ Source'Length > Max_Length and then Drop = Left
+ =>
+ Super_To_String (To_Super_String'Result) =
+ Source (Source'Last - Max_Length + 1 .. Source'Last),
+
+ others -- Drop = Right
+ =>
+ Super_To_String (To_Super_String'Result) =
+ Source (Source'First .. Source'First - 1 + Max_Length)),
+ Global => null;
-- Note the additional parameter Max_Length, which specifies the maximum
-- length setting of the resulting Super_String value.
-- The following procedures have declarations (and semantics) that are
-- exactly analogous to those declared in Ada.Strings.Bounded.
- function Super_To_String (Source : Super_String) return String;
+ function Super_To_String (Source : Super_String) return String
+ is (String (Source.Data (1 .. Source.Current_Length)));
procedure Set_Super_String
(Target : out Super_String;
Source : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ (if Source'Length > Target.Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Source'Length <= Target.Max_Length
+ =>
+ Super_To_String (Target) = Source,
+
+ Source'Length > Target.Max_Length and then Drop = Left
+ =>
+ Super_To_String (Target) =
+ Source (Source'Last - Target.Max_Length + 1 .. Source'Last),
+
+ others -- Drop = Right
+ =>
+ Super_To_String (Target) =
+ Source (Source'First .. Source'First - 1 + Target.Max_Length)),
+ Global => null;
function Super_Append
(Left : Super_String;
Right : Super_String;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre =>
+ Left.Max_Length = Right.Max_Length
+ and then
+ (if Super_Length (Left) > Left.Max_Length - Super_Length (Right)
+ then Drop /= Error),
+ Post => Super_Append'Result.Max_Length = Left.Max_Length,
+ Contract_Cases =>
+ (Super_Length (Left) <= Left.Max_Length - Super_Length (Right)
+ =>
+ Super_Length (Super_Append'Result) =
+ Super_Length (Left) + Super_Length (Right)
+ and then
+ Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
+ Super_To_String (Left)
+ and then
+ (if Super_Length (Right) > 0 then
+ Super_Slice (Super_Append'Result,
+ Super_Length (Left) + 1,
+ Super_Length (Super_Append'Result)) =
+ Super_To_String (Right)),
+
+ Super_Length (Left) > Left.Max_Length - Super_Length (Right)
+ and then Drop = Strings.Left
+ =>
+ Super_Length (Super_Append'Result) = Left.Max_Length
+ and then
+ (if Super_Length (Right) < Left.Max_Length then
+ String'(Super_Slice (Super_Append'Result,
+ 1, Left.Max_Length - Super_Length (Right))) =
+ Super_Slice (Left,
+ Super_Length (Left) - Left.Max_Length
+ + Super_Length (Right) + 1,
+ Super_Length (Left)))
+ and then
+ Super_Slice (Super_Append'Result,
+ Left.Max_Length - Super_Length (Right) + 1, Left.Max_Length) =
+ Super_To_String (Right),
+
+ others -- Drop = Right
+ =>
+ Super_Length (Super_Append'Result) = Left.Max_Length
+ and then
+ Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
+ Super_To_String (Left)
+ and then
+ (if Super_Length (Left) < Left.Max_Length then
+ String'(Super_Slice (Super_Append'Result,
+ Super_Length (Left) + 1, Left.Max_Length)) =
+ Super_Slice (Right,
+ 1, Left.Max_Length - Super_Length (Left)))),
+ Global => null;
function Super_Append
(Left : Super_String;
Right : String;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre =>
+ (if Right'Length > Left.Max_Length - Super_Length (Left)
+ then Drop /= Error),
+ Post => Super_Append'Result.Max_Length = Left.Max_Length,
+ Contract_Cases =>
+ (Super_Length (Left) <= Left.Max_Length - Right'Length
+ =>
+ Super_Length (Super_Append'Result) =
+ Super_Length (Left) + Right'Length
+ and then
+ Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
+ Super_To_String (Left)
+ and then
+ (if Right'Length > 0 then
+ Super_Slice (Super_Append'Result,
+ Super_Length (Left) + 1,
+ Super_Length (Super_Append'Result)) =
+ Right),
+
+ Super_Length (Left) > Left.Max_Length - Right'Length
+ and then Drop = Strings.Left
+ =>
+ Super_Length (Super_Append'Result) = Left.Max_Length
+ and then
+ (if Right'Length < Left.Max_Length then
+
+ -- The result is the end of Left followed by Right
+
+ String'(Super_Slice (Super_Append'Result,
+ 1, Left.Max_Length - Right'Length)) =
+ Super_Slice (Left,
+ Super_Length (Left) - Left.Max_Length + Right'Length
+ + 1,
+ Super_Length (Left))
+ and then
+ Super_Slice (Super_Append'Result,
+ Left.Max_Length - Right'Length + 1, Left.Max_Length) =
+ Right
+ else
+ -- The result is the last Max_Length characters of Right
+
+ Super_To_String (Super_Append'Result) =
+ Right (Right'Last - Left.Max_Length + 1 .. Right'Last)),
+
+ others -- Drop = Right
+ =>
+ Super_Length (Super_Append'Result) = Left.Max_Length
+ and then
+ Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
+ Super_To_String (Left)
+ and then
+ (if Super_Length (Left) < Left.Max_Length then
+ Super_Slice (Super_Append'Result,
+ Super_Length (Left) + 1, Left.Max_Length) =
+ Right (Right'First
+ .. Left.Max_Length - Super_Length (Left)
+ - 1 + Right'First))),
+ Global => null;
function Super_Append
(Left : String;
Right : Super_String;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre =>
+ (if Left'Length > Right.Max_Length - Super_Length (Right)
+ then Drop /= Error),
+ Post => Super_Append'Result.Max_Length = Right.Max_Length,
+ Contract_Cases =>
+ (Left'Length <= Right.Max_Length - Super_Length (Right)
+ =>
+ Super_Length (Super_Append'Result) =
+ Left'Length + Super_Length (Right)
+ and then Super_Slice (Super_Append'Result, 1, Left'Length) = Left
+ and then
+ (if Super_Length (Right) > 0 then
+ Super_Slice (Super_Append'Result,
+ Left'Length + 1, Super_Length (Super_Append'Result)) =
+ Super_To_String (Right)),
+
+ Left'Length > Right.Max_Length - Super_Length (Right)
+ and then Drop = Strings.Left
+ =>
+ Super_Length (Super_Append'Result) = Right.Max_Length
+ and then
+ (if Super_Length (Right) < Right.Max_Length then
+ Super_Slice (Super_Append'Result,
+ 1, Right.Max_Length - Super_Length (Right)) =
+ Left
+ (Left'Last - Right.Max_Length + Super_Length (Right) + 1
+ .. Left'Last))
+ and then
+ Super_Slice (Super_Append'Result,
+ Right.Max_Length - Super_Length (Right) + 1,
+ Right.Max_Length) =
+ Super_To_String (Right),
+
+ others -- Drop = Right
+ =>
+ Super_Length (Super_Append'Result) = Right.Max_Length
+ and then
+ (if Left'Length < Right.Max_Length then
+
+ -- The result is Left followed by the beginning of Right
+
+ Super_Slice (Super_Append'Result, 1, Left'Length) = Left
+ and then
+ String'(Super_Slice (Super_Append'Result,
+ Left'Length + 1, Right.Max_Length)) =
+ Super_Slice (Right, 1, Right.Max_Length - Left'Length)
+ else
+ -- The result is the first Max_Length characters of Left
+
+ Super_To_String (Super_Append'Result) =
+ Left (Left'First .. Right.Max_Length - 1 + Left'First))),
+ Global => null;
function Super_Append
(Left : Super_String;
Right : Character;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre =>
+ (if Super_Length (Left) = Left.Max_Length then Drop /= Error),
+ Post => Super_Append'Result.Max_Length = Left.Max_Length,
+ Contract_Cases =>
+ (Super_Length (Left) < Left.Max_Length
+ =>
+ Super_Length (Super_Append'Result) = Super_Length (Left) + 1
+ and then
+ Super_Slice (Super_Append'Result, 1, Super_Length (Left)) =
+ Super_To_String (Left)
+ and then
+ Super_Element (Super_Append'Result, Super_Length (Left) + 1) =
+ Right,
+
+ Super_Length (Left) = Left.Max_Length and then Drop = Strings.Right
+ =>
+ Super_Length (Super_Append'Result) = Left.Max_Length
+ and then
+ Super_To_String (Super_Append'Result) = Super_To_String (Left),
+
+ others -- Drop = Left
+ =>
+ Super_Length (Super_Append'Result) = Left.Max_Length
+ and then
+ String'(Super_Slice (Super_Append'Result,
+ 1, Left.Max_Length - 1)) =
+ Super_Slice (Left, 2, Left.Max_Length)
+ and then
+ Super_Element (Super_Append'Result, Left.Max_Length) = Right),
+ Global => null;
function Super_Append
(Left : Character;
Right : Super_String;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre =>
+ (if Super_Length (Right) = Right.Max_Length then Drop /= Error),
+ Post => Super_Append'Result.Max_Length = Right.Max_Length,
+ Contract_Cases =>
+ (Super_Length (Right) < Right.Max_Length
+ =>
+ Super_Length (Super_Append'Result) = Super_Length (Right) + 1
+ and then
+ Super_Slice (Super_Append'Result, 2, Super_Length (Right) + 1) =
+ Super_To_String (Right)
+ and then Super_Element (Super_Append'Result, 1) = Left,
+
+ Super_Length (Right) = Right.Max_Length and then Drop = Strings.Left
+ =>
+ Super_Length (Super_Append'Result) = Right.Max_Length
+ and then
+ Super_To_String (Super_Append'Result) = Super_To_String (Right),
+
+ others -- Drop = Right
+ =>
+ Super_Length (Super_Append'Result) = Right.Max_Length
+ and then
+ String'(Super_Slice (Super_Append'Result, 2, Right.Max_Length)) =
+ Super_Slice (Right, 1, Right.Max_Length - 1)
+ and then Super_Element (Super_Append'Result, 1) = Left),
+ Global => null;
procedure Super_Append
(Source : in out Super_String;
New_Item : Super_String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ Source.Max_Length = New_Item.Max_Length
+ and then
+ (if Super_Length (Source) >
+ Source.Max_Length - Super_Length (New_Item)
+ then Drop /= Error),
+ Contract_Cases =>
+ (Super_Length (Source) <= Source.Max_Length - Super_Length (New_Item)
+ =>
+ Super_Length (Source) =
+ Super_Length (Source'Old) + Super_Length (New_Item)
+ and then
+ Super_Slice (Source, 1, Super_Length (Source'Old)) =
+ Super_To_String (Source'Old)
+ and then
+ (if Super_Length (New_Item) > 0 then
+ Super_Slice (Source,
+ Super_Length (Source'Old) + 1, Super_Length (Source)) =
+ Super_To_String (New_Item)),
+
+ Super_Length (Source) > Source.Max_Length - Super_Length (New_Item)
+ and then Drop = Left
+ =>
+ Super_Length (Source) = Source.Max_Length
+ and then
+ (if Super_Length (New_Item) < Source.Max_Length then
+ String'(Super_Slice (Source,
+ 1, Source.Max_Length - Super_Length (New_Item))) =
+ Super_Slice (Source'Old,
+ Super_Length (Source'Old) - Source.Max_Length
+ + Super_Length (New_Item) + 1,
+ Super_Length (Source'Old)))
+ and then
+ Super_Slice (Source,
+ Source.Max_Length - Super_Length (New_Item) + 1,
+ Source.Max_Length) =
+ Super_To_String (New_Item),
+
+ others -- Drop = Right
+ =>
+ Super_Length (Source) = Source.Max_Length
+ and then
+ Super_Slice (Source, 1, Super_Length (Source'Old)) =
+ Super_To_String (Source'Old)
+ and then
+ (if Super_Length (Source'Old) < Source.Max_Length then
+ String'(Super_Slice (Source,
+ Super_Length (Source'Old) + 1, Source.Max_Length)) =
+ Super_Slice (New_Item,
+ 1, Source.Max_Length - Super_Length (Source'Old)))),
+ Global => null;
procedure Super_Append
(Source : in out Super_String;
New_Item : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ (if New_Item'Length > Source.Max_Length - Super_Length (Source)
+ then Drop /= Error),
+ Contract_Cases =>
+ (Super_Length (Source) <= Source.Max_Length - New_Item'Length
+ =>
+ Super_Length (Source) = Super_Length (Source'Old) + New_Item'Length
+ and then
+ Super_Slice (Source, 1, Super_Length (Source'Old)) =
+ Super_To_String (Source'Old)
+ and then
+ (if New_Item'Length > 0 then
+ Super_Slice (Source,
+ Super_Length (Source'Old) + 1, Super_Length (Source)) =
+ New_Item),
+
+ Super_Length (Source) > Source.Max_Length - New_Item'Length
+ and then Drop = Left
+ =>
+ Super_Length (Source) = Source.Max_Length
+ and then
+ (if New_Item'Length < Source.Max_Length then
+
+ -- The result is the end of Source followed by New_Item
+
+ String'(Super_Slice (Source,
+ 1, Source.Max_Length - New_Item'Length)) =
+ Super_Slice (Source'Old,
+ Super_Length (Source'Old) - Source.Max_Length
+ + New_Item'Length + 1,
+ Super_Length (Source'Old))
+ and then
+ Super_Slice (Source,
+ Source.Max_Length - New_Item'Length + 1,
+ Source.Max_Length) =
+ New_Item
+ else
+ -- The result is the last Max_Length characters of
+ -- New_Item.
+
+ Super_To_String (Source) = New_Item
+ (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)),
+
+ others -- Drop = Right
+ =>
+ Super_Length (Source) = Source.Max_Length
+ and then
+ Super_Slice (Source, 1, Super_Length (Source'Old)) =
+ Super_To_String (Source'Old)
+ and then
+ (if Super_Length (Source'Old) < Source.Max_Length then
+ Super_Slice (Source,
+ Super_Length (Source'Old) + 1, Source.Max_Length) =
+ New_Item (New_Item'First
+ .. Source.Max_Length - Super_Length (Source'Old) - 1
+ + New_Item'First))),
+ Global => null;
procedure Super_Append
(Source : in out Super_String;
New_Item : Character;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ (if Super_Length (Source) = Source.Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Super_Length (Source) < Source.Max_Length
+ =>
+ Super_Length (Source) = Super_Length (Source'Old) + 1
+ and then
+ Super_Slice (Source, 1, Super_Length (Source'Old)) =
+ Super_To_String (Source'Old)
+ and then
+ Super_Element (Source, Super_Length (Source'Old) + 1) = New_Item,
+
+ Super_Length (Source) = Source.Max_Length and then Drop = Right
+ =>
+ Super_Length (Source) = Source.Max_Length
+ and then Super_To_String (Source) = Super_To_String (Source'Old),
+
+ others -- Drop = Left
+ =>
+ Super_Length (Source) = Source.Max_Length
+ and then
+ String'(Super_Slice (Source, 1, Source.Max_Length - 1)) =
+ Super_Slice (Source'Old, 2, Source.Max_Length)
+ and then Super_Element (Source, Source.Max_Length) = New_Item),
+ Global => null;
function Concat
(Left : Super_String;
- Right : Super_String) return Super_String;
+ Right : Super_String) return Super_String
+ with
+ Pre => Left.Max_Length = Right.Max_Length
+ and then Super_Length (Left) <= Left.Max_Length - Super_Length (Right),
+ Post => Concat'Result.Max_Length = Left.Max_Length
+ and then
+ Super_Length (Concat'Result) =
+ Super_Length (Left) + Super_Length (Right)
+ and then
+ Super_Slice (Concat'Result, 1, Super_Length (Left)) =
+ Super_To_String (Left)
+ and then
+ (if Super_Length (Right) > 0 then
+ Super_Slice (Concat'Result,
+ Super_Length (Left) + 1, Super_Length (Concat'Result)) =
+ Super_To_String (Right)),
+ Global => null;
function Concat
(Left : Super_String;
- Right : String) return Super_String;
+ Right : String) return Super_String
+ with
+ Pre => Right'Length <= Left.Max_Length - Super_Length (Left),
+ Post => Concat'Result.Max_Length = Left.Max_Length
+ and then
+ Super_Length (Concat'Result) = Super_Length (Left) + Right'Length
+ and then
+ Super_Slice (Concat'Result, 1, Super_Length (Left)) =
+ Super_To_String (Left)
+ and then
+ (if Right'Length > 0 then
+ Super_Slice (Concat'Result,
+ Super_Length (Left) + 1, Super_Length (Concat'Result)) =
+ Right),
+ Global => null;
function Concat
(Left : String;
- Right : Super_String) return Super_String;
+ Right : Super_String) return Super_String
+ with
+ Pre => Left'Length <= Right.Max_Length - Super_Length (Right),
+ Post => Concat'Result.Max_Length = Right.Max_Length
+ and then
+ Super_Length (Concat'Result) = Left'Length + Super_Length (Right)
+ and then Super_Slice (Concat'Result, 1, Left'Length) = Left
+ and then
+ (if Super_Length (Right) > 0 then
+ Super_Slice (Concat'Result,
+ Left'Length + 1, Super_Length (Concat'Result)) =
+ Super_To_String (Right)),
+ Global => null;
function Concat
(Left : Super_String;
- Right : Character) return Super_String;
+ Right : Character) return Super_String
+ with
+ Pre => Super_Length (Left) < Left.Max_Length,
+ Post => Concat'Result.Max_Length = Left.Max_Length
+ and then Super_Length (Concat'Result) = Super_Length (Left) + 1
+ and then
+ Super_Slice (Concat'Result, 1, Super_Length (Left)) =
+ Super_To_String (Left)
+ and then Super_Element (Concat'Result, Super_Length (Left) + 1) = Right,
+ Global => null;
function Concat
(Left : Character;
- Right : Super_String) return Super_String;
+ Right : Super_String) return Super_String
+ with
+ Pre => Super_Length (Right) < Right.Max_Length,
+ Post => Concat'Result.Max_Length = Right.Max_Length
+ and then Super_Length (Concat'Result) = 1 + Super_Length (Right)
+ and then Super_Element (Concat'Result, 1) = Left
+ and then
+ Super_Slice (Concat'Result, 2, Super_Length (Concat'Result)) =
+ Super_To_String (Right),
+ Global => null;
function Super_Element
(Source : Super_String;
- Index : Positive) return Character;
+ Index : Positive) return Character
+ is (if Index <= Source.Current_Length
+ then Source.Data (Index)
+ else raise Index_Error)
+ with Pre => Index <= Super_Length (Source);
procedure Super_Replace_Element
(Source : in out Super_String;
Index : Positive;
- By : Character);
+ By : Character)
+ with
+ Pre => Index <= Super_Length (Source),
+ Post => Super_Length (Source) = Super_Length (Source'Old)
+ and then
+ (for all K in 1 .. Super_Length (Source) =>
+ Super_Element (Source, K) =
+ (if K = Index then By else Super_Element (Source'Old, K))),
+ Global => null;
function Super_Slice
(Source : Super_String;
Low : Positive;
- High : Natural) return String;
+ High : Natural) return String
+ is (if Low - 1 > Source.Current_Length or else High > Source.Current_Length
+
+ -- Note: test of High > Length is in accordance with AI95-00128
+
+ then raise Index_Error
+ else
+ -- Note: in this case, superflat bounds are not a problem, we just
+ -- get the null string in accordance with normal Ada slice rules.
+
+ String (Source.Data (Low .. High)))
+ with Pre => Low - 1 <= Super_Length (Source)
+ and then High <= Super_Length (Source);
function Super_Slice
(Source : Super_String;
Low : Positive;
- High : Natural) return Super_String;
+ High : Natural) return Super_String
+ with
+ Pre =>
+ Low - 1 <= Super_Length (Source) and then High <= Super_Length (Source),
+ Post => Super_Slice'Result.Max_Length = Source.Max_Length
+ and then
+ Super_To_String (Super_Slice'Result) =
+ Super_Slice (Source, Low, High),
+ Global => null;
procedure Super_Slice
(Source : Super_String;
Target : out Super_String;
Low : Positive;
- High : Natural);
+ High : Natural)
+ with
+ Pre => Source.Max_Length = Target.Max_Length
+ and then Low - 1 <= Super_Length (Source)
+ and then High <= Super_Length (Source),
+ Post => Super_To_String (Target) = Super_Slice (Source, Low, High),
+ Global => null;
function "="
(Left : Super_String;
- Right : Super_String) return Boolean;
+ Right : Super_String) return Boolean
+ with
+ Pre => Left.Max_Length = Right.Max_Length,
+ Post => "="'Result = (Super_To_String (Left) = Super_To_String (Right)),
+ Global => null;
function Equal
(Left : Super_String;
@@ -175,59 +691,111 @@ package Ada.Strings.Superbounded is
function Equal
(Left : Super_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Post => Equal'Result = (Super_To_String (Left) = Right),
+ Global => null;
function Equal
(Left : String;
- Right : Super_String) return Boolean;
+ Right : Super_String) return Boolean
+ with
+ Post => Equal'Result = (Left = Super_To_String (Right)),
+ Global => null;
function Less
(Left : Super_String;
- Right : Super_String) return Boolean;
+ Right : Super_String) return Boolean
+ with
+ Pre => Left.Max_Length = Right.Max_Length,
+ Post =>
+ Less'Result = (Super_To_String (Left) < Super_To_String (Right)),
+ Global => null;
function Less
(Left : Super_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Post => Less'Result = (Super_To_String (Left) < Right),
+ Global => null;
function Less
(Left : String;
- Right : Super_String) return Boolean;
+ Right : Super_String) return Boolean
+ with
+ Post => Less'Result = (Left < Super_To_String (Right)),
+ Global => null;
function Less_Or_Equal
(Left : Super_String;
- Right : Super_String) return Boolean;
+ Right : Super_String) return Boolean
+ with
+ Pre => Left.Max_Length = Right.Max_Length,
+ Post =>
+ Less_Or_Equal'Result =
+ (Super_To_String (Left) <= Super_To_String (Right)),
+ Global => null;
function Less_Or_Equal
(Left : Super_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Post => Less_Or_Equal'Result = (Super_To_String (Left) <= Right),
+ Global => null;
function Less_Or_Equal
(Left : String;
- Right : Super_String) return Boolean;
+ Right : Super_String) return Boolean
+ with
+ Post => Less_Or_Equal'Result = (Left <= Super_To_String (Right)),
+ Global => null;
function Greater
(Left : Super_String;
- Right : Super_String) return Boolean;
+ Right : Super_String) return Boolean
+ with
+ Pre => Left.Max_Length = Right.Max_Length,
+ Post =>
+ Greater'Result = (Super_To_String (Left) > Super_To_String (Right)),
+ Global => null;
function Greater
(Left : Super_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Post => Greater'Result = (Super_To_String (Left) > Right),
+ Global => null;
function Greater
(Left : String;
- Right : Super_String) return Boolean;
+ Right : Super_String) return Boolean
+ with
+ Post => Greater'Result = (Left > Super_To_String (Right)),
+ Global => null;
function Greater_Or_Equal
(Left : Super_String;
- Right : Super_String) return Boolean;
+ Right : Super_String) return Boolean
+ with
+ Pre => Left.Max_Length = Right.Max_Length,
+ Post =>
+ Greater_Or_Equal'Result =
+ (Super_To_String (Left) >= Super_To_String (Right)),
+ Global => null;
function Greater_Or_Equal
(Left : Super_String;
- Right : String) return Boolean;
+ Right : String) return Boolean
+ with
+ Post => Greater_Or_Equal'Result = (Super_To_String (Left) >= Right),
+ Global => null;
function Greater_Or_Equal
(Left : String;
- Right : Super_String) return Boolean;
+ Right : Super_String) return Boolean
+ with
+ Post => Greater_Or_Equal'Result = (Left >= Super_To_String (Right)),
+ Global => null;
----------------------
-- Search Functions --
@@ -237,63 +805,449 @@ package Ada.Strings.Superbounded is
(Source : Super_String;
Pattern : String;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => Pattern'Length > 0,
+ Post => Super_Index'Result <= Super_Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Super_Length (Source) = 0
+ =>
+ Super_Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Super_Length (Source) > 0
+ and then
+ (for some J in 1 .. Super_Length (Source) - (Pattern'Length - 1) =>
+ Search.Match (Super_To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Super_Index'Result in
+ 1 .. Super_Length (Source) - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (Super_To_String (Source), Pattern, Mapping, Super_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 .. Super_Length (Source) =>
+ (if (if Going = Forward
+ then J <= Super_Index'Result - 1
+ else J - 1 in Super_Index'Result
+ .. Super_Length (Source) - Pattern'Length)
+ then not (Search.Match
+ (Super_To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Super_Index'Result = 0),
+ Global => null;
function Super_Index
(Source : Super_String;
Pattern : String;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => Pattern'Length /= 0 and then Mapping /= null,
+ Post => Super_Index'Result <= Super_Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Super_Length (Source) = 0
+ =>
+ Super_Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Super_Length (Source) > 0
+ and then
+ (for some J in 1 .. Super_Length (Source) - (Pattern'Length - 1) =>
+ Search.Match (Super_To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Super_Index'Result in
+ 1 .. Super_Length (Source) - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (Super_To_String (Source), Pattern, Mapping, Super_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 .. Super_Length (Source) =>
+ (if (if Going = Forward
+ then J <= Super_Index'Result - 1
+ else J - 1 in Super_Index'Result
+ .. Super_Length (Source) - Pattern'Length)
+ then not (Search.Match
+ (Super_To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Super_Index'Result = 0),
+ Global => null;
function Super_Index
(Source : Super_String;
Set : Maps.Character_Set;
Test : Membership := Inside;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Post => Super_Index'Result <= Super_Length (Source),
+ Contract_Cases =>
+
+ -- If no character of Source satisfies the property Test on Set,
+ -- then 0 is returned.
+
+ ((for all C of Super_To_String (Source) =>
+ (Test = Inside) /= Maps.Is_In (C, Set))
+ =>
+ Super_Index'Result = 0,
+
+ -- Otherwise, an index in the range of Source is returned
+
+ others
+ =>
+ -- The result is in the range of Source
+
+ Super_Index'Result in 1 .. Super_Length (Source)
+
+ -- The character at the returned index satisfies the property
+ -- Test on Set.
+
+ and then
+ (Test = Inside) =
+ Maps.Is_In (Super_Element (Source, Super_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 .. Super_Length (Source) =>
+ (if J /= Super_Index'Result
+ and then (J < Super_Index'Result) = (Going = Forward)
+ then (Test = Inside)
+ /= Maps.Is_In (Super_Element (Source, J), Set)))),
+ Global => null;
function Super_Index
(Source : Super_String;
Pattern : String;
From : Positive;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre =>
+ (if Super_Length (Source) /= 0 then From <= Super_Length (Source))
+ and then Pattern'Length /= 0,
+ Post => Super_Index'Result <= Super_Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Super_Length (Source) = 0
+ =>
+ Super_Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Super_Length (Source) > 0
+ and then
+ (for some J in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Super_Length (Source) else From)
+ - (Pattern'Length - 1) =>
+ Search.Match (Super_To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Super_Index'Result in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Super_Length (Source) else From)
+ - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (Super_To_String (Source), Pattern, Mapping, Super_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 .. Super_Length (Source) =>
+ (if (if Going = Forward
+ then J in From .. Super_Index'Result - 1
+ else J - 1 in Super_Index'Result
+ .. From - Pattern'Length)
+ then not (Search.Match
+ (Super_To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Super_Index'Result = 0),
+ Global => null;
function Super_Index
(Source : Super_String;
Pattern : String;
From : Positive;
Going : Direction := Forward;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre =>
+ (if Super_Length (Source) /= 0 then From <= Super_Length (Source))
+ and then Pattern'Length /= 0
+ and then Mapping /= null,
+ Post => Super_Index'Result <= Super_Length (Source),
+ Contract_Cases =>
+
+ -- If Source is the empty string, then 0 is returned
+
+ (Super_Length (Source) = 0
+ =>
+ Super_Index'Result = 0,
+
+ -- If some slice of Source matches Pattern, then a valid index is
+ -- returned.
+
+ Super_Length (Source) > 0
+ and then
+ (for some J in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Super_Length (Source) else From)
+ - (Pattern'Length - 1) =>
+ Search.Match (Super_To_String (Source), Pattern, Mapping, J))
+ =>
+ -- The result is in the considered range of Source
+
+ Super_Index'Result in
+ (if Going = Forward then From else 1)
+ .. (if Going = Forward then Super_Length (Source) else From)
+ - (Pattern'Length - 1)
+
+ -- The slice beginning at the returned index matches Pattern
+
+ and then Search.Match
+ (Super_To_String (Source), Pattern, Mapping, Super_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 .. Super_Length (Source) =>
+ (if (if Going = Forward
+ then J in From .. Super_Index'Result - 1
+ else J - 1 in Super_Index'Result
+ .. From - Pattern'Length)
+ then not (Search.Match
+ (Super_To_String (Source), Pattern, Mapping, J)))),
+
+ -- Otherwise, 0 is returned
+
+ others
+ =>
+ Super_Index'Result = 0),
+ Global => null;
function Super_Index
(Source : Super_String;
Set : Maps.Character_Set;
From : Positive;
Test : Membership := Inside;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Pre =>
+ (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
+ Post => Super_Index'Result <= Super_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.
+
+ (Super_Length (Source) = 0
+ or else
+ (for all J in 1 .. Super_Length (Source) =>
+ (if J = From or else (J > From) = (Going = Forward) then
+ (Test = Inside) /=
+ Maps.Is_In (Super_Element (Source, J), Set)))
+ =>
+ Super_Index'Result = 0,
+
+ -- Otherwise, an index in the considered range of Source is returned
+
+ others
+ =>
+ -- The result is in the considered range of Source
+
+ Super_Index'Result in 1 .. Super_Length (Source)
+ and then
+ (Super_Index'Result = From
+ or else (Super_Index'Result > From) = (Going = Forward))
+
+ -- The character at the returned index satisfies the property
+ -- Test on Set.
+
+ and then
+ (Test = Inside) =
+ Maps.Is_In (Super_Element (Source, Super_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 .. Super_Length (Source) =>
+ (if J /= Super_Index'Result
+ and then (J < Super_Index'Result) = (Going = Forward)
+ and then (J = From
+ or else (J > From) = (Going = Forward))
+ then (Test = Inside)
+ /= Maps.Is_In (Super_Element (Source, J), Set)))),
+ Global => null;
function Super_Index_Non_Blank
(Source : Super_String;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Post => Super_Index_Non_Blank'Result <= Super_Length (Source),
+ Contract_Cases =>
+
+ -- If all characters of Source are Space characters, then 0 is
+ -- returned.
+
+ ((for all C of Super_To_String (Source) => C = ' ')
+ =>
+ Super_Index_Non_Blank'Result = 0,
+
+ -- Otherwise, an index in the range of Source is returned
+
+ others
+ =>
+ -- The result is in the range of Source
+
+ Super_Index_Non_Blank'Result in 1 .. Super_Length (Source)
+
+ -- The character at the returned index is not a Space character
+
+ and then
+ Super_Element (Source, Super_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 .. Super_Length (Source) =>
+ (if J /= Super_Index_Non_Blank'Result
+ and then
+ (J < Super_Index_Non_Blank'Result) = (Going = Forward)
+ then Super_Element (Source, J) = ' '))),
+ Global => null;
function Super_Index_Non_Blank
(Source : Super_String;
From : Positive;
- Going : Direction := Forward) return Natural;
+ Going : Direction := Forward) return Natural
+ with
+ Pre =>
+ (if Super_Length (Source) /= 0 then From <= Super_Length (Source)),
+ Post => Super_Index_Non_Blank'Result <= Super_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.
+
+ (Super_Length (Source) = 0
+ or else
+ (for all J in 1 .. Super_Length (Source) =>
+ (if J = From or else (J > From) = (Going = Forward) then
+ Super_Element (Source, J) = ' '))
+ =>
+ Super_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
+
+ Super_Index_Non_Blank'Result in 1 .. Super_Length (Source)
+ and then
+ (Super_Index_Non_Blank'Result = From
+ or else
+ (Super_Index_Non_Blank'Result > From) = (Going = Forward))
+
+ -- The character at the returned index is not a Space character
+
+ and then
+ Super_Element (Source, Super_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 .. Super_Length (Source) =>
+ (if J /= Super_Index_Non_Blank'Result
+ and then
+ (J < Super_Index_Non_Blank'Result) = (Going = Forward)
+ and then (J = From
+ or else (J > From) = (Going = Forward))
+ then Super_Element (Source, J) = ' '))),
+ Global => null;
function Super_Count
(Source : Super_String;
Pattern : String;
- Mapping : Maps.Character_Mapping := Maps.Identity) return Natural;
+ Mapping : Maps.Character_Mapping := Maps.Identity) return Natural
+ with
+ Pre => Pattern'Length /= 0,
+ Global => null;
function Super_Count
(Source : Super_String;
Pattern : String;
- Mapping : Maps.Character_Mapping_Function) return Natural;
+ Mapping : Maps.Character_Mapping_Function) return Natural
+ with
+ Pre => Pattern'Length /= 0 and then Mapping /= null,
+ Global => null;
function Super_Count
(Source : Super_String;
- Set : Maps.Character_Set) return Natural;
+ Set : Maps.Character_Set) return Natural
+ with
+ Global => null;
procedure Super_Find_Token
(Source : Super_String;
@@ -301,14 +1255,112 @@ package Ada.Strings.Superbounded is
From : Positive;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ Last : out Natural)
+ with
+ Pre =>
+ (if Super_Length (Source) /= 0 then From <= Super_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.
+
+ (Super_Length (Source) = 0
+ or else
+ (for all J in From .. Super_Length (Source) =>
+ (Test = Inside) /= Maps.Is_In (Super_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 .. Super_Length (Source)
+ and then Last in First .. Super_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 (Super_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 (Super_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 < Super_Length (Source)
+ then
+ (Test = Inside) /=
+ Maps.Is_In (Super_Element (Source, Last + 1), Set))),
+ Global => null;
procedure Super_Find_Token
(Source : Super_String;
Set : Maps.Character_Set;
Test : Membership;
First : out Positive;
- Last : out Natural);
+ Last : out Natural)
+ with
+ 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.
+
+ (Super_Length (Source) = 0
+ or else
+ (for all J in 1 .. Super_Length (Source) =>
+ (Test = Inside) /= Maps.Is_In (Super_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 .. Super_Length (Source)
+ and then Last in First .. Super_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 (Super_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 (Super_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 < Super_Length (Source)
+ then
+ (Test = Inside) /=
+ Maps.Is_In (Super_Element (Source, Last + 1), Set))),
+ Global => null;
------------------------------------
-- String Translation Subprograms --
@@ -316,19 +1368,51 @@ package Ada.Strings.Superbounded is
function Super_Translate
(Source : Super_String;
- Mapping : Maps.Character_Mapping) return Super_String;
+ Mapping : Maps.Character_Mapping) return Super_String
+ with
+ Post => Super_Translate'Result.Max_Length = Source.Max_Length
+ and then Super_Length (Super_Translate'Result) = Super_Length (Source)
+ and then
+ (for all K in 1 .. Super_Length (Source) =>
+ Super_Element (Super_Translate'Result, K) =
+ Ada.Strings.Maps.Value (Mapping, Super_Element (Source, K))),
+ Global => null;
procedure Super_Translate
(Source : in out Super_String;
- Mapping : Maps.Character_Mapping);
+ Mapping : Maps.Character_Mapping)
+ with
+ Post => Super_Length (Source) = Super_Length (Source'Old)
+ and then
+ (for all K in 1 .. Super_Length (Source) =>
+ Super_Element (Source, K) =
+ Ada.Strings.Maps.Value (Mapping, Super_Element (Source'Old, K))),
+ Global => null;
function Super_Translate
(Source : Super_String;
- Mapping : Maps.Character_Mapping_Function) return Super_String;
+ Mapping : Maps.Character_Mapping_Function) return Super_String
+ with
+ Pre => Mapping /= null,
+ Post => Super_Translate'Result.Max_Length = Source.Max_Length
+ and then Super_Length (Super_Translate'Result) = Super_Length (Source)
+ and then
+ (for all K in 1 .. Super_Length (Source) =>
+ Super_Element (Super_Translate'Result, K) =
+ Mapping (Super_Element (Source, K))),
+ Global => null;
procedure Super_Translate
(Source : in out Super_String;
- Mapping : Maps.Character_Mapping_Function);
+ Mapping : Maps.Character_Mapping_Function)
+ with
+ Pre => Mapping /= null,
+ Post => Super_Length (Source) = Super_Length (Source'Old)
+ and then
+ (for all K in 1 .. Super_Length (Source) =>
+ Super_Element (Source, K) =
+ Mapping (Super_Element (Source'Old, K))),
+ Global => null;
---------------------------------------
-- String Transformation Subprograms --
@@ -339,48 +1423,756 @@ package Ada.Strings.Superbounded is
Low : Positive;
High : Natural;
By : String;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre =>
+ Low - 1 <= Super_Length (Source)
+ and then
+ (if Drop = Error
+ then (if High >= Low
+ then Low - 1
+ <= Source.Max_Length - By'Length
+ - Integer'Max (Super_Length (Source) - High, 0)
+ else Super_Length (Source) <=
+ Source.Max_Length - By'Length)),
+ Post =>
+ Super_Replace_Slice'Result.Max_Length = Source.Max_Length,
+ Contract_Cases =>
+ (Low - 1 <= Source.Max_Length - By'Length - Integer'Max
+ (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
+ =>
+ -- Total length is lower than Max_Length: nothing is dropped
+
+ -- Note that if High < Low, the insertion is done before Low, so in
+ -- all cases the starting position of the slice of Source remaining
+ -- after the replaced Slice is Integer'Max (High + 1, Low).
+
+ Super_Length (Super_Replace_Slice'Result) =
+ Low - 1 + By'Length + Integer'Max
+ (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
+ and then
+ String'(Super_Slice (Super_Replace_Slice'Result, 1, Low - 1)) =
+ Super_Slice (Source, 1, Low - 1)
+ and then
+ Super_Slice (Super_Replace_Slice'Result,
+ Low, Low - 1 + By'Length) = By
+ and then
+ (if Integer'Max (High, Low - 1) < Super_Length (Source) then
+ String'(Super_Slice (Super_Replace_Slice'Result,
+ Low + By'Length,
+ Super_Length (Super_Replace_Slice'Result))) =
+ Super_Slice (Source,
+ Integer'Max (High + 1, Low), Super_Length (Source))),
+
+ Low - 1 > Source.Max_Length - By'Length - Integer'Max
+ (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
+ and then Drop = Left
+ =>
+ -- Final_Super_Slice is the length of the slice of Source remaining
+ -- after the replaced part.
+ (declare
+ Final_Super_Slice : constant Natural :=
+ Integer'Max
+ (Super_Length (Source) - Integer'Max (High, Low - 1), 0);
+ begin
+ -- The result is of maximal length and ends by the last
+ -- Final_Super_Slice characters of Source.
+
+ Super_Length (Super_Replace_Slice'Result) = Source.Max_Length
+ and then
+ (if Final_Super_Slice > 0 then
+ String'(Super_Slice (Super_Replace_Slice'Result,
+ Source.Max_Length - Final_Super_Slice + 1,
+ Source.Max_Length)) =
+ Super_Slice (Source,
+ Integer'Max (High + 1, Low), Super_Length (Source)))
+
+ -- Depending on when we reach Max_Length, either the first
+ -- part of Source is fully dropped and By is partly dropped,
+ -- or By is fully added and the first part of Source is partly
+ -- dropped.
+
+ and then
+ (if Source.Max_Length - Final_Super_Slice - By'Length <= 0 then
+
+ -- The first (possibly zero) characters of By are dropped
+
+ (if Final_Super_Slice < Source.Max_Length then
+ Super_Slice (Super_Replace_Slice'Result,
+ 1, Source.Max_Length - Final_Super_Slice) =
+ By (By'Last - Source.Max_Length + Final_Super_Slice
+ + 1
+ .. By'Last))
+
+ else -- By is added to the result
+
+ Super_Slice (Super_Replace_Slice'Result,
+ Source.Max_Length - Final_Super_Slice - By'Length + 1,
+ Source.Max_Length - Final_Super_Slice) =
+ By
+
+ -- The first characters of Source (1 .. Low - 1) are
+ -- dropped.
+
+ and then
+ String'(Super_Slice (Super_Replace_Slice'Result, 1,
+ Source.Max_Length - Final_Super_Slice - By'Length)) =
+ Super_Slice (Source,
+ Low - Source.Max_Length
+ + Final_Super_Slice + By'Length,
+ Low - 1))),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first Low - 1
+ -- characters of Source.
+
+ Super_Length (Super_Replace_Slice'Result) = Source.Max_Length
+ and then
+ String'(Super_Slice (Super_Replace_Slice'Result, 1, Low - 1)) =
+ Super_Slice (Source, 1, Low - 1)
+
+ -- Depending on when we reach Max_Length, either the last part
+ -- of Source is fully dropped and By is partly dropped, or By
+ -- is fully added and the last part of Source is partly dropped.
+
+ and then
+ (if Low - 1 >= Source.Max_Length - By'Length then
+
+ -- The last characters of By are dropped
+
+ Super_Slice (Super_Replace_Slice'Result,
+ Low, Source.Max_Length) =
+ By (By'First .. Source.Max_Length - Low + By'First)
+
+ else -- By is fully added
+
+ Super_Slice (Super_Replace_Slice'Result,
+ Low, Low + By'Length - 1) = By
+
+ -- Then Source starting from Natural'Max (High + 1, Low)
+ -- is added but the last characters are dropped.
+
+ and then
+ String'(Super_Slice (Super_Replace_Slice'Result,
+ Low + By'Length, Source.Max_Length)) =
+ Super_Slice (Source, Integer'Max (High + 1, Low),
+ Integer'Max (High + 1, Low) +
+ (Source.Max_Length - Low - By'Length)))),
+ Global => null;
procedure Super_Replace_Slice
(Source : in out Super_String;
Low : Positive;
High : Natural;
By : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ Low - 1 <= Super_Length (Source)
+ and then
+ (if Drop = Error
+ then (if High >= Low
+ then Low - 1
+ <= Source.Max_Length - By'Length
+ - Natural'Max (Super_Length (Source) - High, 0)
+ else Super_Length (Source) <=
+ Source.Max_Length - By'Length)),
+ Contract_Cases =>
+ (Low - 1 <= Source.Max_Length - By'Length - Integer'Max
+ (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
+ =>
+ -- Total length is lower than Max_Length: nothing is dropped
+
+ -- Note that if High < Low, the insertion is done before Low, so in
+ -- all cases the starting position of the slice of Source remaining
+ -- after the replaced Slice is Integer'Max (High + 1, Low).
+
+ Super_Length (Source) = Low - 1 + By'Length + Integer'Max
+ (Super_Length (Source'Old) - Integer'Max (High, Low - 1), 0)
+ and then
+ String'(Super_Slice (Source, 1, Low - 1)) =
+ Super_Slice (Source'Old, 1, Low - 1)
+ and then Super_Slice (Source, Low, Low - 1 + By'Length) = By
+ and then
+ (if Integer'Max (High, Low - 1) < Super_Length (Source'Old) then
+ String'(Super_Slice (Source,
+ Low + By'Length, Super_Length (Source))) =
+ Super_Slice (Source'Old,
+ Integer'Max (High + 1, Low),
+ Super_Length (Source'Old))),
+
+ Low - 1 > Source.Max_Length - By'Length - Integer'Max
+ (Super_Length (Source) - Integer'Max (High, Low - 1), 0)
+ and then Drop = Left
+ =>
+ -- Final_Super_Slice is the length of the slice of Source remaining
+ -- after the replaced part.
+ (declare
+ Final_Super_Slice : constant Natural :=
+ Integer'Max (0,
+ Super_Length (Source'Old) - Integer'Max (High, Low - 1));
+ begin
+ -- The result is of maximal length and ends by the last
+ -- Final_Super_Slice characters of Source.
+
+ Super_Length (Source) = Source.Max_Length
+ and then
+ (if Final_Super_Slice > 0 then
+ String'(Super_Slice (Source,
+ Source.Max_Length - Final_Super_Slice + 1,
+ Source.Max_Length)) =
+ Super_Slice (Source'Old,
+ Integer'Max (High + 1, Low),
+ Super_Length (Source'Old)))
+
+ -- Depending on when we reach Max_Length, either the first
+ -- part of Source is fully dropped and By is partly dropped,
+ -- or By is fully added and the first part of Source is partly
+ -- dropped.
+
+ and then
+ (if Source.Max_Length - Final_Super_Slice - By'Length <= 0
+ then
+ -- The first characters of By are dropped
+
+ (if Final_Super_Slice < Source.Max_Length then
+ Super_Slice (Source,
+ 1, Source.Max_Length - Final_Super_Slice) =
+ By (By'Last - Source.Max_Length + Final_Super_Slice
+ + 1
+ .. By'Last))
+
+ else -- By is added to the result
+
+ Super_Slice (Source,
+ Source.Max_Length - Final_Super_Slice - By'Length + 1,
+ Source.Max_Length - Final_Super_Slice) = By
+
+ -- The first characters of Source (1 .. Low - 1) are
+ -- dropped.
+
+ and then
+ String'(Super_Slice (Source, 1,
+ Source.Max_Length - Final_Super_Slice - By'Length)) =
+ Super_Slice (Source'Old,
+ Low - Source.Max_Length + Final_Super_Slice
+ + By'Length,
+ Low - 1))),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first Low - 1
+ -- characters of Source.
+
+ Super_Length (Source) = Source.Max_Length
+ and then
+ String'(Super_Slice (Source, 1, Low - 1)) =
+ Super_Slice (Source'Old, 1, Low - 1)
+
+ -- Depending on when we reach Max_Length, either the last part
+ -- of Source is fully dropped and By is partly dropped, or By
+ -- is fully added and the last part of Source is partly dropped.
+
+ and then
+ (if Low - 1 >= Source.Max_Length - By'Length then
+
+ -- The last characters of By are dropped
+
+ Super_Slice (Source, Low, Source.Max_Length) =
+ By (By'First .. Source.Max_Length - Low + By'First)
+
+ else -- By is fully added
+
+ Super_Slice (Source, Low, Low + By'Length - 1) = By
+
+ -- Then Source starting from Natural'Max (High + 1, Low)
+ -- is added but the last characters are dropped.
+
+ and then
+ String'(Super_Slice (Source,
+ Low + By'Length, Source.Max_Length)) =
+ Super_Slice (Source'Old, Integer'Max (High + 1, Low),
+ Integer'Max (High + 1, Low) +
+ (Source.Max_Length - Low - By'Length)))),
+ Global => null;
function Super_Insert
(Source : Super_String;
Before : Positive;
New_Item : String;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre =>
+ Before - 1 <= Super_Length (Source)
+ and then
+ (if New_Item'Length > Source.Max_Length - Super_Length (Source)
+ then Drop /= Error),
+ Post => Super_Insert'Result.Max_Length = Source.Max_Length,
+ Contract_Cases =>
+ (Super_Length (Source) <= Source.Max_Length - New_Item'Length
+ =>
+ -- Total length is lower than Max_Length: nothing is dropped
+
+ Super_Length (Super_Insert'Result) =
+ Super_Length (Source) + New_Item'Length
+ and then
+ String'(Super_Slice (Super_Insert'Result, 1, Before - 1)) =
+ Super_Slice (Source, 1, Before - 1)
+ and then
+ Super_Slice (Super_Insert'Result,
+ Before, Before - 1 + New_Item'Length) =
+ New_Item
+ and then
+ (if Before <= Super_Length (Source) then
+ String'(Super_Slice (Super_Insert'Result,
+ Before + New_Item'Length,
+ Super_Length (Super_Insert'Result))) =
+ Super_Slice (Source, Before, Super_Length (Source))),
+
+ Super_Length (Source) > Source.Max_Length - New_Item'Length
+ and then Drop = Left
+ =>
+ -- The result is of maximal length and ends by the last characters
+ -- of Source.
+
+ Super_Length (Super_Insert'Result) = Source.Max_Length
+ and then
+ (if Before <= Super_Length (Source) then
+ String'(Super_Slice (Super_Insert'Result,
+ Source.Max_Length - Super_Length (Source) + Before,
+ Source.Max_Length)) =
+ Super_Slice (Source, Before, Super_Length (Source)))
+
+ -- Depending on when we reach Max_Length, either the first part
+ -- of Source is fully dropped and New_Item is partly dropped, or
+ -- New_Item is fully added and the first part of Source is partly
+ -- dropped.
+
+ and then
+ (if Source.Max_Length - Super_Length (Source) - 1 + Before
+ < New_Item'Length
+ then
+ -- The first characters of New_Item are dropped
+
+ (if Super_Length (Source) - Before + 1 < Source.Max_Length
+ then
+ Super_Slice (Super_Insert'Result, 1,
+ Source.Max_Length - Super_Length (Source) - 1 + Before) =
+ New_Item
+ (New_Item'Last - Source.Max_Length
+ + Super_Length (Source) - Before + 2
+ .. New_Item'Last))
+
+ else -- New_Item is added to the result
+
+ Super_Slice (Super_Insert'Result,
+ Source.Max_Length - Super_Length (Source) - New_Item'Length
+ + Before,
+ Source.Max_Length - Super_Length (Source) - 1 + Before) =
+ New_Item
+
+ -- The first characters of Source (1 .. Before - 1) are
+ -- dropped.
+
+ and then
+ String'(Super_Slice (Super_Insert'Result,
+ 1, Source.Max_Length - Super_Length (Source)
+ - New_Item'Length - 1 + Before)) =
+ Super_Slice (Source,
+ Super_Length (Source) - Source.Max_Length
+ + New_Item'Length + 1,
+ Before - 1)),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first
+ -- characters of Source.
+
+ Super_Length (Super_Insert'Result) = Source.Max_Length
+ and then
+ String'(Super_Slice (Super_Insert'Result, 1, Before - 1)) =
+ Super_Slice (Source, 1, Before - 1)
+
+ -- Depending on when we reach Max_Length, either the last part
+ -- of Source is fully dropped and New_Item is partly dropped, or
+ -- New_Item is fully added and the last part of Source is partly
+ -- dropped.
+
+ and then
+ (if Before - 1 >= Source.Max_Length - New_Item'Length then
+
+ -- The last characters of New_Item are dropped
+
+ Super_Slice (Super_Insert'Result, Before, Source.Max_Length) =
+ New_Item (New_Item'First
+ .. Source.Max_Length - Before + New_Item'First)
+
+ else -- New_Item is fully added
+
+ Super_Slice (Super_Insert'Result,
+ Before, Before + New_Item'Length - 1) =
+ New_Item
+
+ -- Then Source starting from Before is added but the
+ -- last characters are dropped.
+
+ and then
+ String'(Super_Slice (Super_Insert'Result,
+ Before + New_Item'Length, Source.Max_Length)) =
+ Super_Slice (Source,
+ Before, Source.Max_Length - New_Item'Length))),
+ Global => null;
procedure Super_Insert
(Source : in out Super_String;
Before : Positive;
New_Item : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ Before - 1 <= Super_Length (Source)
+ and then
+ (if New_Item'Length > Source.Max_Length - Super_Length (Source)
+ then Drop /= Error),
+ Contract_Cases =>
+ (Super_Length (Source) <= Source.Max_Length - New_Item'Length
+ =>
+ -- Total length is lower than Max_Length: nothing is dropped
+
+ Super_Length (Source) = Super_Length (Source'Old) + New_Item'Length
+ and then
+ String'(Super_Slice (Source, 1, Before - 1)) =
+ Super_Slice (Source'Old, 1, Before - 1)
+ and then
+ Super_Slice (Source, Before, Before - 1 + New_Item'Length) =
+ New_Item
+ and then
+ (if Before <= Super_Length (Source'Old) then
+ String'(Super_Slice (Source,
+ Before + New_Item'Length, Super_Length (Source))) =
+ Super_Slice (Source'Old,
+ Before, Super_Length (Source'Old))),
+
+ Super_Length (Source) > Source.Max_Length - New_Item'Length
+ and then Drop = Left
+ =>
+ -- The result is of maximal length and ends by the last characters
+ -- of Source.
+
+ Super_Length (Source) = Source.Max_Length
+ and then
+ (if Before <= Super_Length (Source'Old) then
+ String'(Super_Slice (Source,
+ Source.Max_Length - Super_Length (Source'Old) + Before,
+ Source.Max_Length)) =
+ Super_Slice (Source'Old,
+ Before, Super_Length (Source'Old)))
+
+ -- Depending on when we reach Max_Length, either the first part
+ -- of Source is fully dropped and New_Item is partly dropped, or
+ -- New_Item is fully added and the first part of Source is partly
+ -- dropped.
+
+ and then
+ (if Source.Max_Length - Super_Length (Source'Old) - 1 + Before
+ < New_Item'Length
+ then
+ -- The first characters of New_Item are dropped
+
+ (if Super_Length (Source'Old) - Before + 1 < Source.Max_Length
+ then
+ Super_Slice (Source,
+ 1, Source.Max_Length - Super_Length (Source'Old)
+ - 1 + Before) =
+ New_Item
+ (New_Item'Last - Source.Max_Length
+ + Super_Length (Source'Old) - Before + 2
+ .. New_Item'Last))
+
+ else -- New_Item is added to the result
+
+ Super_Slice (Source,
+ Source.Max_Length - Super_Length (Source'Old)
+ - New_Item'Length + Before,
+ Source.Max_Length - Super_Length (Source'Old) - 1 + Before)
+ = New_Item
+
+ -- The first characters of Source (1 .. Before - 1) are
+ -- dropped.
+
+ and then
+ String'(Super_Slice (Source, 1,
+ Source.Max_Length - Super_Length (Source'Old)
+ - New_Item'Length - 1 + Before)) =
+ Super_Slice (Source'Old,
+ Super_Length (Source'Old)
+ - Source.Max_Length + New_Item'Length + 1,
+ Before - 1)),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first
+ -- characters of Source.
+
+ Super_Length (Source) = Source.Max_Length
+ and then
+ String'(Super_Slice (Source, 1, Before - 1)) =
+ Super_Slice (Source'Old, 1, Before - 1)
+
+ -- Depending on when we reach Max_Length, either the last part
+ -- of Source is fully dropped and New_Item is partly dropped, or
+ -- New_Item is fully added and the last part of Source is partly
+ -- dropped.
+
+ and then
+ (if Before - 1 >= Source.Max_Length - New_Item'Length then
+
+ -- The last characters of New_Item are dropped
+
+ Super_Slice (Source, Before, Source.Max_Length) =
+ New_Item (New_Item'First
+ .. Source.Max_Length - Before + New_Item'First)
+
+ else -- New_Item is fully added
+
+ Super_Slice (Source, Before, Before + New_Item'Length - 1) =
+ New_Item
+
+ -- Then Source starting from Before is added but the
+ -- last characters are dropped.
+
+ and then
+ String'(Super_Slice (Source,
+ Before + New_Item'Length, Source.Max_Length)) =
+ Super_Slice (Source'Old,
+ Before, Source.Max_Length - New_Item'Length))),
+ Global => null;
function Super_Overwrite
(Source : Super_String;
Position : Positive;
New_Item : String;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre =>
+ Position - 1 <= Super_Length (Source)
+ and then (if New_Item'Length > Source.Max_Length - (Position - 1)
+ then Drop /= Error),
+ Post => Super_Overwrite'Result.Max_Length = Source.Max_Length,
+ Contract_Cases =>
+ (Position - 1 <= Source.Max_Length - New_Item'Length
+ =>
+ -- The length is unchanged, unless New_Item overwrites further than
+ -- the end of Source. In this contract case, we suppose New_Item
+ -- doesn't overwrite further than Max_Length.
+
+ Super_Length (Super_Overwrite'Result) =
+ Integer'Max (Super_Length (Source), Position - 1 + New_Item'Length)
+ and then
+ String'(Super_Slice (Super_Overwrite'Result, 1, Position - 1)) =
+ Super_Slice (Source, 1, Position - 1)
+ and then Super_Slice (Super_Overwrite'Result,
+ Position, Position - 1 + New_Item'Length) =
+ New_Item
+ and then
+ (if Position - 1 + New_Item'Length < Super_Length (Source) then
+
+ -- There are some unchanged characters of Source remaining
+ -- after New_Item.
+
+ String'(Super_Slice (Super_Overwrite'Result,
+ Position + New_Item'Length, Super_Length (Source))) =
+ Super_Slice (Source,
+ Position + New_Item'Length, Super_Length (Source))),
+
+ Position - 1 > Source.Max_Length - New_Item'Length and then Drop = Left
+ =>
+ Super_Length (Super_Overwrite'Result) = Source.Max_Length
+
+ -- If a part of the result has to be dropped, it means New_Item is
+ -- overwriting further than the end of Source. Thus the result is
+ -- necessarily ending by New_Item. However, we don't know whether
+ -- New_Item covers all Max_Length characters or some characters of
+ -- Source are remaining at the left.
+
+ and then
+ (if New_Item'Length > Source.Max_Length then
+
+ -- New_Item covers all Max_Length characters
+
+ Super_To_String (Super_Overwrite'Result) =
+ New_Item
+ (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)
+ else
+ -- New_Item fully appears at the end
+
+ Super_Slice (Super_Overwrite'Result,
+ Source.Max_Length - New_Item'Length + 1,
+ Source.Max_Length) =
+ New_Item
+
+ -- The left of Source is cut
+
+ and then
+ String'(Super_Slice (Super_Overwrite'Result,
+ 1, Source.Max_Length - New_Item'Length)) =
+ Super_Slice (Source,
+ Position - Source.Max_Length + New_Item'Length,
+ Position - 1)),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first
+ -- characters of Source.
+
+ Super_Length (Super_Overwrite'Result) = Source.Max_Length
+ and then
+ String'(Super_Slice (Super_Overwrite'Result, 1, Position - 1)) =
+ Super_Slice (Source, 1, Position - 1)
+
+ -- Then New_Item is written until Max_Length
+
+ and then Super_Slice (Super_Overwrite'Result,
+ Position, Source.Max_Length) =
+ New_Item (New_Item'First
+ .. Source.Max_Length - Position + New_Item'First)),
+ Global => null;
procedure Super_Overwrite
(Source : in out Super_String;
Position : Positive;
New_Item : String;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre =>
+ Position - 1 <= Super_Length (Source)
+ and then (if New_Item'Length > Source.Max_Length - (Position - 1)
+ then Drop /= Error),
+ Contract_Cases =>
+ (Position - 1 <= Source.Max_Length - New_Item'Length
+ =>
+ -- The length is unchanged, unless New_Item overwrites further than
+ -- the end of Source. In this contract case, we suppose New_Item
+ -- doesn't overwrite further than Max_Length.
+
+ Super_Length (Source) = Integer'Max
+ (Super_Length (Source'Old), Position - 1 + New_Item'Length)
+ and then
+ String'(Super_Slice (Source, 1, Position - 1)) =
+ Super_Slice (Source'Old, 1, Position - 1)
+ and then Super_Slice (Source,
+ Position, Position - 1 + New_Item'Length) =
+ New_Item
+ and then
+ (if Position - 1 + New_Item'Length < Super_Length (Source'Old)
+ then
+ -- There are some unchanged characters of Source remaining
+ -- after New_Item.
+
+ String'(Super_Slice (Source,
+ Position + New_Item'Length, Super_Length (Source'Old))) =
+ Super_Slice (Source'Old,
+ Position + New_Item'Length, Super_Length (Source'Old))),
+
+ Position - 1 > Source.Max_Length - New_Item'Length and then Drop = Left
+ =>
+ Super_Length (Source) = Source.Max_Length
+
+ -- If a part of the result has to be dropped, it means New_Item is
+ -- overwriting further than the end of Source. Thus the result is
+ -- necessarily ending by New_Item. However, we don't know whether
+ -- New_Item covers all Max_Length characters or some characters of
+ -- Source are remaining at the left.
+
+ and then
+ (if New_Item'Length > Source.Max_Length then
+
+ -- New_Item covers all Max_Length characters
+
+ Super_To_String (Source) =
+ New_Item
+ (New_Item'Last - Source.Max_Length + 1 .. New_Item'Last)
+ else
+ -- New_Item fully appears at the end
+
+ Super_Slice (Source,
+ Source.Max_Length - New_Item'Length + 1,
+ Source.Max_Length) =
+ New_Item
+
+ -- The left of Source is cut
+
+ and then
+ String'(Super_Slice (Source,
+ 1, Source.Max_Length - New_Item'Length)) =
+ Super_Slice (Source'Old,
+ Position - Source.Max_Length + New_Item'Length,
+ Position - 1)),
+
+ others -- Drop = Right
+ =>
+ -- The result is of maximal length and starts by the first
+ -- characters of Source.
+
+ Super_Length (Source) = Source.Max_Length
+ and then
+ String'(Super_Slice (Source, 1, Position - 1)) =
+ Super_Slice (Source'Old, 1, Position - 1)
+
+ -- New_Item is written until Max_Length
+
+ and then Super_Slice (Source, Position, Source.Max_Length) =
+ New_Item (New_Item'First
+ .. Source.Max_Length - Position + New_Item'First)),
+ Global => null;
function Super_Delete
(Source : Super_String;
From : Positive;
- Through : Natural) return Super_String;
+ Through : Natural) return Super_String
+ with
+ Pre =>
+ (if Through >= From then From - 1 <= Super_Length (Source)),
+ Post => Super_Delete'Result.Max_Length = Source.Max_Length,
+ Contract_Cases =>
+ (Through >= From =>
+ Super_Length (Super_Delete'Result) =
+ From - 1 + Natural'Max (Super_Length (Source) - Through, 0)
+ and then
+ String'(Super_Slice (Super_Delete'Result, 1, From - 1)) =
+ Super_Slice (Source, 1, From - 1)
+ and then
+ (if Through < Super_Length (Source) then
+ String'(Super_Slice (Super_Delete'Result,
+ From, Super_Length (Super_Delete'Result))) =
+ Super_Slice (Source, Through + 1, Super_Length (Source))),
+ others =>
+ Super_Delete'Result = Source),
+ Global => null;
procedure Super_Delete
(Source : in out Super_String;
From : Positive;
- Through : Natural);
+ Through : Natural)
+ with
+ Pre =>
+ (if Through >= From then From - 1 <= Super_Length (Source)),
+ Contract_Cases =>
+ (Through >= From =>
+ Super_Length (Source) =
+ From - 1 + Natural'Max (Super_Length (Source'Old) - Through, 0)
+ and then
+ String'(Super_Slice (Source, 1, From - 1)) =
+ Super_Slice (Source'Old, 1, From - 1)
+ and then
+ (if Through < Super_Length (Source) then
+ String'(Super_Slice (Source, From, Super_Length (Source))) =
+ Super_Slice (Source'Old,
+ Through + 1, Super_Length (Source'Old))),
+ others =>
+ Source = Source'Old),
+ Global => null;
---------------------------------
-- String Selector Subprograms --
@@ -388,45 +2180,376 @@ package Ada.Strings.Superbounded is
function Super_Trim
(Source : Super_String;
- Side : Trim_End) return Super_String;
+ Side : Trim_End) return Super_String
+ with
+ Post => Super_Trim'Result.Max_Length = Source.Max_Length,
+ Contract_Cases =>
+
+ -- If all characters in Source are Space, the returned string is empty
+
+ ((for all C of Super_To_String (Source) => C = ' ')
+ =>
+ Super_Length (Super_Trim'Result) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ (if Side = Right then 1
+ else Super_Index_Non_Blank (Source, Forward));
+ High : constant Positive :=
+ (if Side = Left then Super_Length (Source)
+ else Super_Index_Non_Blank (Source, Backward));
+ begin
+ Super_To_String (Super_Trim'Result) =
+ Super_Slice (Source, Low, High))),
+ Global => null;
procedure Super_Trim
(Source : in out Super_String;
- Side : Trim_End);
+ Side : Trim_End)
+ with
+ Contract_Cases =>
+
+ -- If all characters in Source are Space, the returned string is empty
+
+ ((for all C of Super_To_String (Source) => C = ' ')
+ =>
+ Super_Length (Source) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ (if Side = Right then 1
+ else Super_Index_Non_Blank (Source'Old, Forward));
+ High : constant Positive :=
+ (if Side = Left then Super_Length (Source'Old)
+ else Super_Index_Non_Blank (Source'Old, Backward));
+ begin
+ Super_To_String (Source) = Super_Slice (Source'Old, Low, High))),
+ Global => null;
function Super_Trim
(Source : Super_String;
Left : Maps.Character_Set;
- Right : Maps.Character_Set) return Super_String;
+ Right : Maps.Character_Set) return Super_String
+ with
+ Post => Super_Trim'Result.Max_Length = Source.Max_Length,
+ 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 Super_To_String (Source) => Maps.Is_In (C, Left))
+ or else
+ (for all C of Super_To_String (Source) => Maps.Is_In (C, Right))
+ =>
+ Super_Length (Super_Trim'Result) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ Super_Index (Source, Left, Outside, Forward);
+ High : constant Positive :=
+ Super_Index (Source, Right, Outside, Backward);
+ begin
+ Super_To_String (Super_Trim'Result) =
+ Super_Slice (Source, Low, High))),
+ Global => null;
procedure Super_Trim
(Source : in out Super_String;
Left : Maps.Character_Set;
- Right : Maps.Character_Set);
+ Right : Maps.Character_Set)
+ with
+ 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 Super_To_String (Source) => Maps.Is_In (C, Left))
+ or else
+ (for all C of Super_To_String (Source) => Maps.Is_In (C, Right))
+ =>
+ Super_Length (Source) = 0,
+
+ -- Otherwise, the returned string is a slice of Source
+
+ others
+ =>
+ (declare
+ Low : constant Positive :=
+ Super_Index (Source'Old, Left, Outside, Forward);
+ High : constant Positive :=
+ Super_Index (Source'Old, Right, Outside, Backward);
+ begin
+ Super_To_String (Source) = Super_Slice (Source'Old, Low, High))),
+ Global => null;
function Super_Head
(Source : Super_String;
Count : Natural;
Pad : Character := Space;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre => (if Count > Source.Max_Length then Drop /= Error),
+ Post => Super_Head'Result.Max_Length = Source.Max_Length,
+ Contract_Cases =>
+ (Count <= Super_Length (Source)
+ =>
+ -- Source is cut
+
+ Super_To_String (Super_Head'Result) = Super_Slice (Source, 1, Count),
+ Count > Super_Length (Source) and then Count <= Source.Max_Length
+ =>
+ -- Source is followed by Pad characters
+
+ Super_Length (Super_Head'Result) = Count
+ and then
+ Super_Slice (Super_Head'Result, 1, Super_Length (Source)) =
+ Super_To_String (Source)
+ and then
+ String'(Super_Slice (Super_Head'Result,
+ Super_Length (Source) + 1, Count)) =
+ (1 .. Count - Super_Length (Source) => Pad),
+ Count > Source.Max_Length and then Drop = Right
+ =>
+ -- Source is followed by Pad characters
+
+ Super_Length (Super_Head'Result) = Source.Max_Length
+ and then
+ Super_Slice (Super_Head'Result, 1, Super_Length (Source)) =
+ Super_To_String (Source)
+ and then
+ String'(Super_Slice (Super_Head'Result,
+ Super_Length (Source) + 1, Source.Max_Length)) =
+ (1 .. Source.Max_Length - Super_Length (Source) => Pad),
+ Count - Super_Length (Source) > Source.Max_Length and then Drop = Left
+ =>
+ -- Source is fully dropped on the left
+
+ Super_To_String (Super_Head'Result) =
+ (1 .. Source.Max_Length => Pad),
+ others
+ =>
+ -- Source is partly dropped on the left
+
+ Super_Length (Super_Head'Result) = Source.Max_Length
+ and then
+ String'(Super_Slice (Super_Head'Result,
+ 1, Source.Max_Length - Count + Super_Length (Source))) =
+ Super_Slice (Source,
+ Count - Source.Max_Length + 1, Super_Length (Source))
+ and then
+ String'(Super_Slice (Super_Head'Result,
+ Source.Max_Length - Count + Super_Length (Source) + 1,
+ Source.Max_Length)) =
+ (1 .. Count - Super_Length (Source) => Pad)),
+ Global => null;
procedure Super_Head
(Source : in out Super_String;
Count : Natural;
Pad : Character := Space;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre => (if Count > Source.Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Count <= Super_Length (Source)
+ =>
+ -- Source is cut
+
+ Super_To_String (Source) = Super_Slice (Source'Old, 1, Count),
+ Count > Super_Length (Source) and then Count <= Source.Max_Length
+ =>
+ -- Source is followed by Pad characters
+
+ Super_Length (Source) = Count
+ and then
+ Super_Slice (Source, 1, Super_Length (Source'Old)) =
+ Super_To_String (Source'Old)
+ and then
+ String'(Super_Slice (Source,
+ Super_Length (Source'Old) + 1, Count)) =
+ (1 .. Count - Super_Length (Source'Old) => Pad),
+ Count > Source.Max_Length and then Drop = Right
+ =>
+ -- Source is followed by Pad characters
+
+ Super_Length (Source) = Source.Max_Length
+ and then
+ Super_Slice (Source, 1, Super_Length (Source'Old)) =
+ Super_To_String (Source'Old)
+ and then
+ String'(Super_Slice (Source,
+ Super_Length (Source'Old) + 1, Source.Max_Length)) =
+ (1 .. Source.Max_Length - Super_Length (Source'Old) => Pad),
+ Count - Super_Length (Source) > Source.Max_Length and then Drop = Left
+ =>
+ -- Source is fully dropped on the left
+
+ Super_To_String (Source) = (1 .. Source.Max_Length => Pad),
+ others
+ =>
+ -- Source is partly dropped on the left
+
+ Super_Length (Source) = Source.Max_Length
+ and then
+ String'(Super_Slice (Source,
+ 1, Source.Max_Length - Count + Super_Length (Source'Old))) =
+ Super_Slice (Source'Old,
+ Count - Source.Max_Length + 1, Super_Length (Source'Old))
+ and then
+ String'(Super_Slice (Source,
+ Source.Max_Length - Count + Super_Length (Source'Old) + 1,
+ Source.Max_Length)) =
+ (1 .. Count - Super_Length (Source'Old) => Pad)),
+ Global => null;
function Super_Tail
(Source : Super_String;
Count : Natural;
Pad : Character := Space;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre => (if Count > Source.Max_Length then Drop /= Error),
+ Post => Super_Tail'Result.Max_Length = Source.Max_Length,
+ Contract_Cases =>
+ (Count < Super_Length (Source)
+ =>
+ -- Source is cut
+
+ (if Count > 0 then
+ Super_To_String (Super_Tail'Result) =
+ Super_Slice (Source,
+ Super_Length (Source) - Count + 1, Super_Length (Source))
+ else Super_Length (Super_Tail'Result) = 0),
+ Count >= Super_Length (Source) and then Count < Source.Max_Length
+ =>
+ -- Source is preceded by Pad characters
+
+ Super_Length (Super_Tail'Result) = Count
+ and then
+ String'(Super_Slice (Super_Tail'Result,
+ 1, Count - Super_Length (Source))) =
+ (1 .. Count - Super_Length (Source) => Pad)
+ and then
+ Super_Slice (Super_Tail'Result,
+ Count - Super_Length (Source) + 1, Count) =
+ Super_To_String (Source),
+ Count >= Source.Max_Length and then Drop = Left
+ =>
+ -- Source is preceded by Pad characters
+
+ Super_Length (Super_Tail'Result) = Source.Max_Length
+ and then
+ String'(Super_Slice (Super_Tail'Result,
+ 1, Source.Max_Length - Super_Length (Source))) =
+ (1 .. Source.Max_Length - Super_Length (Source) => Pad)
+ and then
+ (if Super_Length (Source) > 0 then
+ Super_Slice (Super_Tail'Result,
+ Source.Max_Length - Super_Length (Source) + 1,
+ Source.Max_Length) =
+ Super_To_String (Source)),
+ Count - Super_Length (Source) >= Source.Max_Length
+ and then Drop /= Left
+ =>
+ -- Source is fully dropped on the right
+
+ Super_To_String (Super_Tail'Result) =
+ (1 .. Source.Max_Length => Pad),
+ others
+ =>
+ -- Source is partly dropped on the right
+
+ Super_Length (Super_Tail'Result) = Source.Max_Length
+ and then
+ String'(Super_Slice (Super_Tail'Result,
+ 1, Count - Super_Length (Source))) =
+ (1 .. Count - Super_Length (Source) => Pad)
+ and then
+ String'(Super_Slice (Super_Tail'Result,
+ Count - Super_Length (Source) + 1, Source.Max_Length)) =
+ Super_Slice (Source,
+ 1, Source.Max_Length - Count + Super_Length (Source))),
+ Global => null;
procedure Super_Tail
(Source : in out Super_String;
Count : Natural;
Pad : Character := Space;
- Drop : Truncation := Error);
+ Drop : Truncation := Error)
+ with
+ Pre => (if Count > Source.Max_Length then Drop /= Error),
+ Contract_Cases =>
+ (Count < Super_Length (Source)
+ =>
+ -- Source is cut
+
+ (if Count > 0 then
+ Super_To_String (Source) =
+ Super_Slice (Source'Old,
+ Super_Length (Source'Old) - Count + 1,
+ Super_Length (Source'Old))
+ else Super_Length (Source) = 0),
+ Count >= Super_Length (Source) and then Count < Source.Max_Length
+ =>
+ -- Source is preceded by Pad characters
+
+ Super_Length (Source) = Count
+ and then
+ String'(Super_Slice (Source,
+ 1, Count - Super_Length (Source'Old))) =
+ (1 .. Count - Super_Length (Source'Old) => Pad)
+ and then
+ Super_Slice (Source,
+ Count - Super_Length (Source'Old) + 1, Count) =
+ Super_To_String (Source'Old),
+ Count >= Source.Max_Length and then Drop = Left
+ =>
+ -- Source is preceded by Pad characters
+
+ Super_Length (Source) = Source.Max_Length
+ and then
+ String'(Super_Slice (Source,
+ 1, Source.Max_Length - Super_Length (Source'Old))) =
+ (1 .. Source.Max_Length - Super_Length (Source'Old) => Pad)
+ and then
+ (if Super_Length (Source'Old) > 0 then
+ Super_Slice (Source,
+ Source.Max_Length - Super_Length (Source'Old) + 1,
+ Source.Max_Length) =
+ Super_To_String (Source'Old)),
+ Count - Super_Length (Source) >= Source.Max_Length
+ and then Drop /= Left
+ =>
+ -- Source is fully dropped on the right
+
+ Super_To_String (Source) = (1 .. Source.Max_Length => Pad),
+ others
+ =>
+ -- Source is partly dropped on the right
+
+ Super_Length (Source) = Source.Max_Length
+ and then
+ String'(Super_Slice (Source,
+ 1, Count - Super_Length (Source'Old))) =
+ (1 .. Count - Super_Length (Source'Old) => Pad)
+ and then
+ String'(Super_Slice (Source,
+ Count - Super_Length (Source'Old) + 1, Source.Max_Length)) =
+ Super_Slice (Source'Old,
+ 1, Source.Max_Length - Count + Super_Length (Source'Old))),
+ Global => null;
------------------------------------
-- String Constructor Subprograms --
@@ -439,37 +2562,135 @@ package Ada.Strings.Superbounded is
function Times
(Left : Natural;
Right : Character;
- Max_Length : Positive) return Super_String;
+ Max_Length : Positive) return Super_String
+ with
+ Pre => Left <= Max_Length,
+ Post => Times'Result.Max_Length = Max_Length
+ and then Super_To_String (Times'Result) = (1 .. Left => Right),
+ Global => null;
-- Note the additional parameter Max_Length
function Times
(Left : Natural;
Right : String;
- Max_Length : Positive) return Super_String;
+ Max_Length : Positive) return Super_String
+ with
+ Pre => (if Left /= 0 then Right'Length <= Max_Length / Left),
+ Post => Times'Result.Max_Length = Max_Length
+ and then Super_Length (Times'Result) = Left * Right'Length
+ and then
+ (if Right'Length > 0 then
+ (for all K in 1 .. Left * Right'Length =>
+ Super_Element (Times'Result, K) =
+ Right (Right'First + (K - 1) mod Right'Length))),
+ Global => null;
-- Note the additional parameter Max_Length
function Times
(Left : Natural;
- Right : Super_String) return Super_String;
+ Right : Super_String) return Super_String
+ with
+ Pre =>
+ (if Left /= 0 then Super_Length (Right) <= Right.Max_Length / Left),
+ Post => Times'Result.Max_Length = Right.Max_Length
+ and then Super_Length (Times'Result) = Left * Super_Length (Right)
+ and then
+ (if Super_Length (Right) > 0 then
+ (for all K in 1 .. Left * Super_Length (Right) =>
+ Super_Element (Times'Result, K) =
+ Super_Element (Right, 1 + (K - 1) mod Super_Length (Right)))),
+ Global => null;
function Super_Replicate
(Count : Natural;
Item : Character;
Drop : Truncation := Error;
- Max_Length : Positive) return Super_String;
+ Max_Length : Positive) return Super_String
+ with
+ Pre => (if Count > Max_Length then Drop /= Error),
+ Post => Super_Replicate'Result.Max_Length = Max_Length
+ and then Super_To_String (Super_Replicate'Result) =
+ (1 .. Natural'Min (Max_Length, Count) => Item),
+ Global => null;
-- Note the additional parameter Max_Length
function Super_Replicate
(Count : Natural;
Item : String;
Drop : Truncation := Error;
- Max_Length : Positive) return Super_String;
+ Max_Length : Positive) return Super_String
+ with
+ Pre =>
+ (if Count /= 0 and then Item'Length > Max_Length / Count
+ then Drop /= Error),
+ Post => Super_Replicate'Result.Max_Length = Max_Length,
+ Contract_Cases =>
+ (Count = 0 or else Item'Length <= Max_Length / Count
+ =>
+ Super_Length (Super_Replicate'Result) = Count * Item'Length
+ and then
+ (if Item'Length > 0 then
+ (for all K in 1 .. Count * Item'Length =>
+ Super_Element (Super_Replicate'Result, K) =
+ Item (Item'First + (K - 1) mod Item'Length))),
+ Count /= 0
+ and then Item'Length > Max_Length / Count
+ and then Drop = Right
+ =>
+ Super_Length (Super_Replicate'Result) = Max_Length
+ and then
+ (for all K in 1 .. Max_Length =>
+ Super_Element (Super_Replicate'Result, K) =
+ Item (Item'First + (K - 1) mod Item'Length)),
+ others -- Drop = Left
+ =>
+ Super_Length (Super_Replicate'Result) = Max_Length
+ and then
+ (for all K in 1 .. Max_Length =>
+ Super_Element (Super_Replicate'Result, K) =
+ Item (Item'Last - (Max_Length - K) mod Item'Length))),
+ Global => null;
-- Note the additional parameter Max_Length
function Super_Replicate
(Count : Natural;
Item : Super_String;
- Drop : Truncation := Error) return Super_String;
+ Drop : Truncation := Error) return Super_String
+ with
+ Pre =>
+ (if Count /= 0
+ and then Super_Length (Item) > Item.Max_Length / Count
+ then Drop /= Error),
+ Post => Super_Replicate'Result.Max_Length = Item.Max_Length,
+ Contract_Cases =>
+ ((if Count /= 0 then Super_Length (Item) <= Item.Max_Length / Count)
+ =>
+ Super_Length (Super_Replicate'Result) = Count * Super_Length (Item)
+ and then
+ (if Super_Length (Item) > 0 then
+ (for all K in 1 .. Count * Super_Length (Item) =>
+ Super_Element (Super_Replicate'Result, K) =
+ Super_Element (Item,
+ 1 + (K - 1) mod Super_Length (Item)))),
+ Count /= 0
+ and then Super_Length (Item) > Item.Max_Length / Count
+ and then Drop = Right
+ =>
+ Super_Length (Super_Replicate'Result) = Item.Max_Length
+ and then
+ (for all K in 1 .. Item.Max_Length =>
+ Super_Element (Super_Replicate'Result, K) =
+ Super_Element (Item, 1 + (K - 1) mod Super_Length (Item))),
+ others -- Drop = Left
+ =>
+ Super_Length (Super_Replicate'Result) = Item.Max_Length
+ and then
+ (for all K in 1 .. Item.Max_Length =>
+ Super_Element (Super_Replicate'Result, K) =
+ Super_Element (Item,
+ Super_Length (Item)
+ - (Item.Max_Length - K) mod Super_Length (Item)))),
+ Global => null;
private
-- Pragma Inline declarations
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2021-09-22 15:11 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2021-09-22 15:11 [gcc r12-3813] [Ada] Contracts written for the Ada.Strings.Bounded library Pierre-Marie de Rodat
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).