From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id AA8713858422; Wed, 22 Sep 2021 15:11:25 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org AA8713858422 MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r12-3813] [Ada] Contracts written for the Ada.Strings.Bounded library X-Act-Checkin: gcc X-Git-Author: Pierre-Alexandre Bazin X-Git-Refname: refs/heads/master X-Git-Oldrev: 5f325f5e6fd091f73f5be6ef30d27e22e4b59a74 X-Git-Newrev: 1647bc2a78b2182007f011ff0a43f872086ee512 Message-Id: <20210922151125.AA8713858422@sourceware.org> Date: Wed, 22 Sep 2021 15:11:25 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 22 Sep 2021 15:11:25 -0000 https://gcc.gnu.org/g:1647bc2a78b2182007f011ff0a43f872086ee512 commit r12-3813-g1647bc2a78b2182007f011ff0a43f872086ee512 Author: Pierre-Alexandre Bazin 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