From 571d3fb1f40fa85c769a7dbefd84da6c6e99665d Mon Sep 17 00:00:00 2001 From: Joffrey Huguet Date: Thu, 12 Nov 2020 10:40:16 +0100 Subject: [PATCH] [Ada] Add contracts to Ada.Strings.Fixed gcc/ada/ * libgnat/a-strfix.ads: Add postconditions and contract cases to subprograms. --- gcc/ada/libgnat/a-strfix.ads | 894 +++++++++++++++++++++++++++++++++-- 1 file changed, 848 insertions(+), 46 deletions(-) diff --git a/gcc/ada/libgnat/a-strfix.ads b/gcc/ada/libgnat/a-strfix.ads index 7d6e121c534..42141575011 100644 --- a/gcc/ada/libgnat/a-strfix.ads +++ b/gcc/ada/libgnat/a-strfix.ads @@ -108,10 +108,57 @@ package Ada.Strings.Fixed with SPARK_Mode is Going : Direction := Forward; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => + Pre => Pattern'Length /= 0 and then (if Source'Length /= 0 then From in Source'Range), - Global => null; + + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If no slice in the considered range of Source matches Pattern, + -- then 0 is returned. + + ((for all J in Source'Range => + (if (if Going = Forward + then J in From .. Source'Last - Pattern'Length + 1 + else J <= From - Pattern'Length + 1) + then Translate (Source (J .. J - 1 + Pattern'Length), Mapping) + /= Pattern)) + => + Index'Result = 0, + + -- Otherwise, a valid index is returned + + others + => + + -- The result is in the considered range of Source + + (if Going = Forward + then Index'Result in From .. Source'Last - Pattern'Length + 1 + else Index'Result in Source'First .. From - Pattern'Length + 1) + + -- The slice beginning at the returned index matches Pattern + + and then + Translate (Source (Index'Result + .. Index'Result - 1 + Pattern'Length), + Mapping) + = Pattern + + -- The result is the smallest or largest index which satisfies the + -- matching, respectively when Going = Forward and + -- Going = Backwards. + + and then + (for all J in Source'Range => + (if (if Going = Forward + then J in From .. Index'Result - 1 + else J - 1 in Index'Result .. From - Pattern'Length) + then Translate (Source (J .. J - 1 + Pattern'Length), + Mapping) + /= Pattern))), + Global => null; pragma Ada_05 (Index); function Index @@ -121,10 +168,57 @@ package Ada.Strings.Fixed with SPARK_Mode is Going : Direction := Forward; Mapping : Maps.Character_Mapping := Maps.Identity) return Natural with - Pre => + Pre => Pattern'Length /= 0 and then (if Source'Length /= 0 then From in Source'Range), - Global => null; + + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If no slice in the considered range of Source matches Pattern, + -- then 0 is returned. + + ((for all J in Source'Range => + (if (if Going = Forward + then J in From .. Source'Last - Pattern'Length + 1 + else J <= From - Pattern'Length + 1) + then Translate (Source (J .. J - 1 + Pattern'Length), Mapping) + /= Pattern)) + => + Index'Result = 0, + + -- Otherwise, a valid index is returned + + others + => + + -- The result is in the considered range of Source + + (if Going = Forward + then Index'Result in From .. Source'Last - Pattern'Length + 1 + else Index'Result in Source'First .. From - Pattern'Length + 1) + + -- The slice beginning at the returned index matches Pattern + + and then + Translate (Source (Index'Result + .. Index'Result - 1 + Pattern'Length), + Mapping) + = Pattern + + -- The result is the smallest or largest index which satisfies the + -- matching, respectively when Going = Forward and + -- Going = Backwards. + + and then + (for all J in Source'Range => + (if (if Going = Forward + then J in From .. Index'Result - 1 + else J - 1 in Index'Result .. From - Pattern'Length) + then Translate (Source (J .. J - 1 + Pattern'Length), + Mapping) + /= Pattern))), + Global => null; pragma Ada_05 (Index); -- Each Index function searches, starting from From, for a slice of @@ -146,8 +240,53 @@ package Ada.Strings.Fixed with SPARK_Mode 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 in 0 | Source'Range, + Contract_Cases => + + -- If Source is empty, or if no slice of Source matches Pattern, then + -- 0 is returned. + + (Source'Length = 0 + or else + (for all J in Source'First .. Source'Last - Pattern'Length + 1 => + Translate (Source (J .. J - 1 + Pattern'Length), Mapping) + /= Pattern) + => + Index'Result = 0, + + -- Otherwise, a valid index is returned + + others + => + + -- The result is in the considered range of Source + + Index'Result in Source'First .. Source'Last - Pattern'Length + 1 + + -- The slice beginning at the returned index matches Pattern + + and then + Translate (Source (Index'Result + .. Index'Result - 1 + Pattern'Length), + Mapping) + = Pattern + + -- The result is the smallest or largest index which satisfies the + -- matching, respectively when Going = Forward and + -- Going = Backwards. + + and then + (for all J in Source'Range => + (if (if Going = Forward + then J <= Index'Result - 1 + else J - 1 in Index'Result + .. Source'Last - Pattern'Length) + then Translate (Source (J .. J - 1 + Pattern'Length), + Mapping) + /= Pattern))), + Global => null; function Index (Source : String; @@ -155,8 +294,53 @@ package Ada.Strings.Fixed with SPARK_Mode is Going : Direction := Forward; Mapping : Maps.Character_Mapping_Function) return Natural with - Pre => Pattern'Length /= 0, - Global => null; + Pre => Pattern'Length > 0, + + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If Source is empty, or if no slice of Source matches Pattern, then + -- 0 is returned. + + (Source'Length = 0 + or else + (for all J in Source'First .. Source'Last - Pattern'Length + 1 => + Translate (Source (J .. J - 1 + Pattern'Length), Mapping) + /= Pattern) + => + Index'Result = 0, + + -- Otherwise, a valid index is returned + + others + => + + -- The result is in the considered range of Source + + Index'Result in Source'First .. Source'Last - Pattern'Length + 1 + + -- The slice beginning at the returned index matches Pattern + + and then + Translate (Source (Index'Result + .. Index'Result - 1 + Pattern'Length), + Mapping) + = Pattern + + -- The result is the smallest or largest index which satisfies the + -- matching, respectively when Going = Forward and + -- Going = Backwards. + + and then + (for all J in Source'Range => + (if (if Going = Forward + then J <= Index'Result - 1 + else J - 1 in Index'Result + .. Source'Last - Pattern'Length) + then Translate (Source (J .. J - 1 + Pattern'Length), + Mapping) + /= Pattern))), + Global => null; -- If Going = Forward, returns: -- @@ -172,7 +356,44 @@ package Ada.Strings.Fixed with SPARK_Mode is Test : Membership := Inside; Going : Direction := Forward) return Natural with - Global => null; + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If no character of Source satisfies the property Test on Set, then + -- 0 is returned. + + ((for all C of Source => + (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) + => + Index'Result = 0, + + -- Otherwise, a index in the range of Source is returned + + others + => + + -- The result is in the range of Source + + Index'Result in Source'Range + + -- The character at the returned index satisfies the property + -- Test on Set + + and then + (Test = Inside) + = Ada.Strings.Maps.Is_In (Source (Index'Result), Set) + + -- The result is the smallest or largest index which satisfies the + -- property, respectively when Going = Forward and + -- Going = Backwards. + + and then + (for all J in Source'Range => + (if J /= Index'Result + and then (J < Index'Result) = (Going = Forward) + then (Test = Inside) + /= Ada.Strings.Maps.Is_In (Source (J), Set)))), + Global => null; function Index (Source : String; @@ -181,8 +402,53 @@ package Ada.Strings.Fixed with SPARK_Mode is Test : Membership := Inside; Going : Direction := Forward) return Natural with - Pre => (if Source'Length /= 0 then From in Source'Range), - Global => null; + Pre => (if Source'Length /= 0 then From in Source'Range), + + Post => Index'Result in 0 | Source'Range, + Contract_Cases => + + -- If no character in the considered slice of Source satisfies the + -- property Test on Set, then 0 is returned. + + ((for all I in Source'Range => + (if I = From + or else (I > From) = (Going = Forward) + then (Test = Inside) /= Ada.Strings.Maps.Is_In (Source (I), Set))) + => + Index'Result = 0, + + -- Otherwise, an index in the range of Source is returned + + others + => + + -- The result is in the considered range of Source + + Index'Result in Source'Range + and then (Index'Result = From + or else (Index'Result > From) = (Going = Forward)) + + -- The character at the returned index satisfies the property + -- Test on Set. + + and then + (Test = Inside) + = Ada.Strings.Maps.Is_In (Source (Index'Result), Set) + + -- The result is the smallest or largest index which satisfies the + -- property, respectively when Going = Forward and + -- Going = Backwards. + + and then + (for all J in Source'Range => + (if J /= Index'Result + and then (J < Index'Result) = (Going = Forward) + and then (J = From + or else (J > From) = (Going = Forward)) + then + (Test = Inside) + /= Ada.Strings.Maps.Is_In (Source (J), Set)))), + Global => null; pragma Ada_05 (Index); -- Index searches for the first or last occurrence of any of a set of -- characters (when Test=Inside), or any of the complement of a set of @@ -198,8 +464,49 @@ package Ada.Strings.Fixed with SPARK_Mode is From : Positive; Going : Direction := Forward) return Natural with - Pre => (if Source'Length /= 0 then From in Source'Range), - Global => null; + Pre => (if Source'Length /= 0 then From in Source'Range), + + Post => Index_Non_Blank'Result in 0 | Source'Range, + Contract_Cases => + + -- If all characters in the considered slice of Source are Space + -- characters, then 0 is returned. + + ((for all J in Source'Range => + (if J = From or else (J > From) = (Going = Forward) + then Source (J) = ' ')) + => + Index_Non_Blank'Result = 0, + + -- Otherwise, a valid index is returned + + others + => + + -- The result is in the considered range of Source + + Index_Non_Blank'Result in Source'Range + and then (Index_Non_Blank'Result = From + or else (Index_Non_Blank'Result > From) + = (Going = Forward)) + + -- The character at the returned index is not a Space character + + and then Source (Index_Non_Blank'Result) /= ' ' + + -- The result is the smallest or largest index which is not a + -- Space character, respectively when Going = Forward and + -- Going = Backwards. + + and then + (for all J in Source'Range => + (if J /= Index_Non_Blank'Result + and then (J < Index_Non_Blank'Result) + = (Going = Forward) + and then (J = From or else (J > From) + = (Going = Forward)) + then Source (J) = ' '))), + Global => null; pragma Ada_05 (Index_Non_Blank); -- Returns Index (Source, Maps.To_Set(Space), From, Outside, Going) @@ -207,7 +514,37 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : String; Going : Direction := Forward) return Natural with - Global => null; + Post => Index_Non_Blank'Result in 0 | Source'Range, + Contract_Cases => + + -- If all characters of Source are Space characters, then 0 is + -- returned. + + ((for all C of Source => C = ' ') => Index_Non_Blank'Result = 0, + + -- Otherwise, a valid index is returned + + others => + + -- The result is in the range of Source + + Index_Non_Blank'Result in Source'Range + + -- The character at the returned index is not a Space character + + and then Source (Index_Non_Blank'Result) /= ' ' + + -- The result is the smallest or largest index which is not a + -- Space character, respectively when Going = Forward and + -- Going = Backwards. + + and then + (for all J in Source'Range => + (if J /= Index_Non_Blank'Result + and then (J < Index_Non_Blank'Result) + = (Going = Forward) + then Source (J) = ' '))), + Global => null; -- Returns Index (Source, Maps.To_Set(Space), Outside, Going) function Count @@ -246,8 +583,53 @@ package Ada.Strings.Fixed with SPARK_Mode is First : out Positive; Last : out Natural) with - Pre => (if Source'Length /= 0 then From in Source'Range), - Global => null; + Pre => (if Source'Length /= 0 then From in Source'Range), + Contract_Cases => + + -- If Source is the empty string, or if no character of the considered + -- slice of Source satisfies the property Test on Set, then First is + -- set to From and Last is set to 0. + + (Source'Length = 0 + or else + (for all C of Source (From .. Source'Last) => + (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) + => + First = From and then Last = 0, + + -- Otherwise, First and Last are set to valid indexes + + others + => + + -- First and Last are in the considered range of Source + + First in From .. Source'Last + and then Last in First .. Source'Last + + -- No character between From and First satisfies the property Test + -- on Set. + + and then + (for all C of Source (From .. First - 1) => + (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) + + -- All characters between First and Last satisfy the property Test + -- on Set. + + and then + (for all C of Source (First .. Last) => + (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set)) + + -- If Last is not Source'Last, then the character at position + -- Last + 1 does not satify the property Test on Set. + + and then + (if Last < Source'Last + then + (Test = Inside) + /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), + Global => null; pragma Ada_2012 (Find_Token); -- If Source is not the null string and From is not in Source'Range, then -- Index_Error is raised. Otherwise, First is set to the index of the first @@ -264,6 +646,50 @@ package Ada.Strings.Fixed with SPARK_Mode is First : out Positive; Last : out Natural) with + Contract_Cases => + + -- If Source is the empty string, or if no character of Source + -- satisfies the property Test on Set, then First is set to From and + -- Last is set to 0. + + (Source'Length = 0 + or else + (for all C of Source => + (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) + => + First = Source'First and then Last = 0, + + -- Otherwise, First and Last are set to valid indexes + + others + => + + -- First and Last are in the considered range of Source + + First in Source'Range + and then Last in First .. Source'Last + + -- No character before First satisfies the property Test on Set + + and then + (for all C of Source (Source'First .. First - 1) => + (Test = Inside) /= Ada.Strings.Maps.Is_In (C, Set)) + + -- All characters between First and Last satisfy the property Test + -- on Set. + + and then + (for all C of Source (First .. Last) => + (Test = Inside) = Ada.Strings.Maps.Is_In (C, Set)) + + -- If Last is not Source'Last, then the character at position + -- Last + 1 does not satify the property Test on Set. + + and then + (if Last < Source'Last + then + (Test = Inside) + /= Ada.Strings.Maps.Is_In (Source (Last + 1), Set))), Global => null; -- Equivalent to Find_Token (Source, Set, Source'First, Test, First, Last) @@ -275,14 +701,46 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : String; Mapping : Maps.Character_Mapping_Function) return String with - Post => Translate'Result'Length = Source'Length, + Post => + + -- Lower bound of the returned string is 1 + + Translate'Result'First = 1 + + -- The returned string has the same length as Source + + and then Translate'Result'Last = Source'Length + + -- Each character in the returned string is the translation of the + -- character at the same position in Source through Mapping. + + and then + (for all J in Source'Range => + Translate'Result (J - Source'First + 1) + = Mapping (Source (J))), Global => null; function Translate (Source : String; Mapping : Maps.Character_Mapping) return String with - Post => Translate'Result'Length = Source'Length, + Post => + + -- Lower bound of the returned string is 1 + + Translate'Result'First = 1 + + -- The returned string has the same length as Source + + and then Translate'Result'Last = Source'Length + + -- Each character in the returned string is the translation of the + -- character at the same position in Source through Mapping. + + and then + (for all J in Source'Range => + Translate'Result (J - Source'First + 1) + = Ada.Strings.Maps.Value (Mapping, Source (J))), Global => null; -- Returns the string S whose length is Source'Length and such that S (I) @@ -293,12 +751,25 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : in out String; Mapping : Maps.Character_Mapping_Function) with + Post => + + -- Each character in Source after the call is the translation of + -- the character at the same position before the call, through Mapping. + + (for all J in Source'Range => Source (J) = Mapping (Source'Old (J))), Global => null; procedure Translate (Source : in out String; Mapping : Maps.Character_Mapping) with + Post => + + -- Each character in Source after the call is the translation of + -- the character at the same position before the call, through Mapping. + + (for all J in Source'Range => + Source (J) = Ada.Strings.Maps.Value (Mapping, Source'Old (J))), Global => null; -- Equivalent to Source := Translate(Source, Mapping) @@ -344,17 +815,80 @@ package Ada.Strings.Fixed with SPARK_Mode is and then High >= Source'First - 1 and then (if High >= Low then Natural'Max (0, Low - Source'First) - <= Natural'Last - By'Length - - Natural'Max (Source'Last - High, 0) + <= Natural'Last + - By'Length + - Natural'Max (Source'Last - High, 0) else Source'Length <= Natural'Last - By'Length), + + -- Lower bound of the returned string is 1 + + Post => Replace_Slice'Result'First = 1, Contract_Cases => + + -- If High >= Low, then the returned string comprises + -- Source (Source'First .. Low - 1) & By + -- & Source(High + 1 .. Source'Last). + (High >= Low => + + -- Length of the returned string + Replace_Slice'Result'Length - = Natural'Max (0, Low - Source'First) - + By'Length - + Natural'Max (Source'Last - High, 0), + = Natural'Max (0, Low - Source'First) + + By'Length + + Natural'Max (Source'Last - High, 0) + + -- Elements starting at Low are replaced by elements of By + + and then + Replace_Slice'Result (1 .. Natural'Max (0, Low - Source'First)) + = Source (Source'First .. Low - 1) + and then + Replace_Slice'Result + (Natural'Max (0, Low - Source'First) + 1 + .. Natural'Max (0, Low - Source'First) + By'Length) + = By + + -- When there are remaining characters after the replaced slice, + -- they are appended to the result. + + and then + (if High < Source'Last + then + Replace_Slice'Result + (Natural'Max (0, Low - Source'First) + By'Length + 1 + .. Replace_Slice'Result'Last) + = Source (High + 1 .. Source'Last)), + + -- If High < Low, then the returned string is + -- Insert (Source, Before => Low, New_Item => By). + others => - Replace_Slice'Result'Length = Source'Length + By'Length), + + -- Length of the returned string + + Replace_Slice'Result'Length = Source'Length + By'Length + + -- Elements of By are inserted after the element at Low + + and then + Replace_Slice'Result (1 .. Low - Source'First) + = Source (Source'First .. Low - 1) + and then + Replace_Slice'Result + (Low - Source'First + 1 .. Low - Source'First + By'Length) + = By + + -- When there are remaining characters after Low in Source, they + -- are appended to the result. + + and then + (if Low < Source'Last + then + Replace_Slice'Result + (Low - Source'First + By'Length + 1 + .. Replace_Slice'Result'Last) + = Source (Low .. Source'Last))), Global => null; -- Equivalent to: -- @@ -369,7 +903,38 @@ package Ada.Strings.Fixed with SPARK_Mode is Pre => Before - 1 in Source'First - 1 .. Source'Last and then Source'Length <= Natural'Last - New_Item'Length, - Post => Insert'Result'Length = Source'Length + New_Item'Length, + + Post => + + -- Lower bound of the returned string is 1 + + Insert'Result'First = 1 + + -- Length of the returned string + + and then Insert'Result'Length = Source'Length + New_Item'Length + + -- Elements of New_Item are inserted after element at Before + + and then + Insert'Result (1 .. Before - Source'First) + = Source (Source'First .. Before - 1) + and then + Insert'Result + (Before - Source'First + 1 + .. Before - Source'First + New_Item'Length) + = New_Item + + -- When there are remaining characters after Before in Source, they + -- are appended to the returned string. + + and then + (if Before - 1 < Source'Last + then + Insert'Result + (Before - Source'First + New_Item'Length + 1 + .. Insert'Result'Last) + = Source (Before .. Source'Last)), Global => null; -- Propagates Index_Error if Before is not in -- Source'First .. Source'Last+1; otherwise, returns @@ -397,12 +962,44 @@ package Ada.Strings.Fixed with SPARK_Mode is Pre => Position - 1 in Source'First - 1 .. Source'Last and then - (if Position - Source'First >= Source'Length - New_Item'Length - then Position - Source'First <= Natural'Last - New_Item'Length), + (if Position - Source'First >= Source'Length - New_Item'Length + then Position - Source'First <= Natural'Last - New_Item'Length), + Post => - Overwrite'Result'Length - = Integer'Max (Source'Length, - Position - Source'First + New_Item'Length), + + -- Lower bound of the returned string is 1 + + Overwrite'Result'First = 1 + + -- Length of the returned string + + and then + Overwrite'Result'Length + = Integer'Max (Source'Length, + Position - Source'First + New_Item'Length) + + -- Elements after Position are replaced by elements of New_Item + + and then + Overwrite'Result (1 .. Position - Source'First) + = Source (Source'First .. Position - 1) + and then + Overwrite'Result + (Position - Source'First + 1 + .. Position - Source'First + New_Item'Length) + = New_Item + + -- If the end of Source is reached before the characters in New_Item + -- are exhausted, the remaining characters from New_Item are appended + -- to the string. + + and then + (if Position <= Source'Last - New_Item'Length + then + Overwrite'Result + (Position - Source'First + New_Item'Length + 1 + .. Overwrite'Result'Last) + = Source (Position + New_Item'Length .. Source'Last)), Global => null; -- Propagates Index_Error if Position is not in -- Source'First .. Source'Last + 1; otherwise, returns the string obtained @@ -429,15 +1026,47 @@ package Ada.Strings.Fixed with SPARK_Mode is From : Positive; Through : Natural) return String with - Pre => (if From <= Through - then (From in Source'Range - and then Through <= Source'Last)), - Post => - Delete'Result'Length - = Source'Length - (if From <= Through - then Through - From + 1 - else 0), - Global => null; + Pre => (if From <= Through + then (From in Source'Range + and then Through <= Source'Last)), + + -- Lower bound of the returned string is 1 + + Post => + Delete'Result'First = 1, + + Contract_Cases => + + -- If From <= Through, the characters between From and Through are + -- removed. + + (From <= Through => + + -- Length of the returned string + + Delete'Result'Length = Source'Length - (Through - From + 1) + + -- Elements before From are preserved + + and then + Delete'Result (1 .. From - Source'First) + = Source (Source'First .. From - 1) + + -- If there are remaining characters after Through, they are + -- appended to the returned string. + + and then + (if Through < Source'Last + then Delete'Result + (From - Source'First + 1 .. Delete'Result'Last) + = Source (Through + 1 .. Source'Last)), + + -- Otherwise, the returned string is Source with lower bound 1 + + others => + Delete'Result'Length = Source'Length + and then Delete'Result = Source), + Global => null; -- If From <= Through, the returned string is -- Replace_Slice(Source, From, Through, ""); otherwise, it is Source with -- lower bound 1. @@ -469,7 +1098,47 @@ package Ada.Strings.Fixed with SPARK_Mode is (Source : String; Side : Trim_End) return String with - Post => Trim'Result'Length <= Source'Length, + Post => + + -- Lower bound of the returned string is 1 + + Trim'Result'First = 1 + + -- If all characters in Source are Space, the returned string is + -- empty. + + and then + (if (for all J in Source'Range => Source (J) = ' ') + then Trim'Result = "" + + -- Otherwise, the returned string is a slice of Source + + else + (for some Low in Source'Range => + (for some High in Source'Range => + + -- Trim returns the slice of Source between Low and High + + Trim'Result = Source (Low .. High) + + -- Values of Low and High and the characters at their + -- position depend on Side. + + and then + (if Side = Left then High = Source'Last + else Source (High) /= ' ') + and then + (if Side = Right then Low = Source'First + else Source (Low) /= ' ') + + -- All characters outside range Low .. High are + -- Space characters. + + and then + (for all J in Source'Range => + (if J < Low then Source (J) = ' ') + and then + (if J > High then Source (J) = ' '))))), Global => null; -- Returns the string obtained by removing from Source all leading Space -- characters (if Side = Left), all trailing Space characters (if @@ -495,7 +1164,50 @@ package Ada.Strings.Fixed with SPARK_Mode is Left : Maps.Character_Set; Right : Maps.Character_Set) return String with - Post => Trim'Result'Length <= Source'Length, + Post => + + -- Lower bound of the returned string is 1 + + Trim'Result'First = 1 + + -- If all characters are contained in one of the sets Left and Right, + -- then the returned string is empty. + + and then + (if (for all K in Source'Range => + Ada.Strings.Maps.Is_In (Source (K), Left)) + or + (for all K in Source'Range => + Ada.Strings.Maps.Is_In (Source (K), Right)) + then Trim'Result = "" + + -- Otherwise, the returned string is a slice of Source + + else + (for some Low in Source'Range => + (for some High in Source'Range => + + -- Trim returns the slice of Source between Low and High + + Trim'Result = Source (Low .. High) + + -- Characters at the bounds of the returned string are + -- not contained in Left or Right. + + and then not Ada.Strings.Maps.Is_In (Source (Low), Left) + and then not Ada.Strings.Maps.Is_In (Source (High), Right) + + -- All characters before Low are contained in Left. + -- All characters after High are contained in Right. + + and then + (for all K in Source'Range => + (if K < Low + then + Ada.Strings.Maps.Is_In (Source (K), Left)) + and then + (if K > High then + Ada.Strings.Maps.Is_In (Source (K), Right)))))), Global => null; -- Returns the string obtained by removing from Source all leading -- characters in Left and all trailing characters in Right. @@ -521,8 +1233,33 @@ package Ada.Strings.Fixed with SPARK_Mode is Count : Natural; Pad : Character := Space) return String with - Post => Head'Result'Length = Count, - Global => null; + Post => + + -- Lower bound of the returned string is 1 + + Head'Result'First = 1 + + -- Length of the returned string is Count. + + and then Head'Result'Length = Count, + + Contract_Cases => + + -- If Count <= Source'Length, then the first Count characters of + -- Source are returned. + + (Count <= Source'Length => + Head'Result = Source (Source'First .. Source'First - 1 + Count), + + -- Otherwise, the returned string is Source concatenated with + -- Count - Source'Length Pad characters. + + others => + Head'Result (1 .. Source'Length) = Source + and then + Head'Result (Source'Length + 1 .. Count) + = (1 .. Count - Source'Length => Pad)), + Global => null; -- Returns a string of length Count. If Count <= Source'Length, the string -- comprises the first Count characters of Source. Otherwise, its contents -- are Source concatenated with Count - Source'Length Pad characters. @@ -547,7 +1284,44 @@ package Ada.Strings.Fixed with SPARK_Mode is Count : Natural; Pad : Character := Space) return String with - Post => Tail'Result'Length = Count, + Post => + + -- Lower bound of the returned string is 1 + + Tail'Result'First = 1 + + -- Length of the returned string is Count + + and then Tail'Result'Length = Count, + Contract_Cases => + + -- If Count is zero, then the returned string is empty + + (Count = 0 => + Tail'Result = "", + + -- Otherwise, if Count <= Source'Length, then the last Count + -- characters of Source are returned. + + (Count in 1 .. Source'Length) => + Tail'Result = Source (Source'Last - Count + 1 .. Source'Last), + + -- Otherwise, the returned string is Count - Source'Length Pad + -- characters concatenated with Source. + + others => + + -- If Source is empty, then the returned string is Count Pad + -- characters. + + (if Source'Length = 0 + then Tail'Result = (1 .. Count => Pad) + else + Tail'Result (1 .. Count - Source'Length) + = (1 .. Count - Source'Length => Pad) + and then + Tail'Result (Count - Source'Length + 1 .. Tail'Result'Last) + = Source)), Global => null; -- Returns a string of length Count. If Count <= Source'Length, the string -- comprises the last Count characters of Source. Otherwise, its contents @@ -576,7 +1350,19 @@ package Ada.Strings.Fixed with SPARK_Mode is (Left : Natural; Right : Character) return String with - Post => "*"'Result'Length = Left, + Post => + + -- Lower bound of the returned string is 1 + + "*"'Result'First = 1 + + -- Length of the returned string + + and then "*"'Result'Length = Left + + -- All characters of the returned string are Right + + and then (for all C of "*"'Result => C = Right), Global => null; function "*" @@ -584,7 +1370,23 @@ package Ada.Strings.Fixed with SPARK_Mode is Right : String) return String with Pre => (if Right'Length /= 0 then Left <= Natural'Last / Right'Length), - Post => "*"'Result'Length = Left * Right'Length, + + Post => + + -- Lower bound of the returned string is 1 + + "*"'Result'First = 1 + + -- Length of the returned string + + and then "*"'Result'Length = Left * Right'Length + + -- Content of the string is Right concatenated with itself Left times + + and then + (for all J in 0 .. Left - 1 => + "*"'Result (J * Right'Length + 1 .. (J + 1) * Right'Length) + = Right), Global => null; -- These functions replicate a character or string a specified number of -- 2.30.2