From: Yannick Moy Date: Thu, 2 Sep 2021 21:29:38 +0000 (+0200) Subject: [Ada] Proof of Ada.Strings.Maps X-Git-Tag: basepoints/gcc-13~4161 X-Git-Url: http://git.ipfire.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=f46939f9d4091e78e60d8d4d78d023a48a1608aa;p=thirdparty%2Fgcc.git [Ada] Proof of Ada.Strings.Maps gcc/ada/ * libgnat/a-strmap.adb: Add ghost code for proof. (To_Range): This is the most involved proof, as it requires creating the result of the call to To_Domain as a ghost variable, and show the unicity of this result in order to prove the postcondition. * libgnat/a-strmap.ads: (SPARK_Proof_Sorted_Character_Sequence): New ghost function. (To_Domain): Add postcondition regarding sorting of result. (To_Range): Fix postcondition that should compare Length instead of Last for the results of To_Domain and To_Range, as the value of Last for an empty result is not specified in the Ada RM. --- diff --git a/gcc/ada/libgnat/a-strmap.adb b/gcc/ada/libgnat/a-strmap.adb index 8ad9f1265973..c87f4e52d744 100644 --- a/gcc/ada/libgnat/a-strmap.adb +++ b/gcc/ada/libgnat/a-strmap.adb @@ -35,7 +35,17 @@ -- is bit-by-bit or character-by-character and therefore rather slow. -- Generally for character sets we favor the full 32-byte representation. -package body Ada.Strings.Maps is +-- Assertions, ghost code and loop invariants 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. + +pragma Assertion_Policy (Assert => Ignore, + Ghost => Ignore, + Loop_Invariant => Ignore); + +package body Ada.Strings.Maps + with SPARK_Mode +is --------- -- "-" -- @@ -102,9 +112,7 @@ package body Ada.Strings.Maps is (Element : Character; Set : Character_Set) return Boolean is - begin - return Set (Element); - end Is_In; + (Set (Element)); --------------- -- Is_Subset -- @@ -122,18 +130,37 @@ package body Ada.Strings.Maps is -- To_Domain -- --------------- - function To_Domain (Map : Character_Mapping) return Character_Sequence - is - Result : String (1 .. Map'Length); + function To_Domain (Map : Character_Mapping) return Character_Sequence is + Result : String (1 .. Map'Length) with Relaxed_Initialization; J : Natural; + type Character_Index is array (Character) of Natural with Ghost; + Indexes : Character_Index := (others => 0) with Ghost; + begin J := 0; for C in Map'Range loop if Map (C) /= C then J := J + 1; Result (J) := C; + Indexes (C) := J; end if; + + pragma Loop_Invariant (if Map = Identity then J = 0); + pragma Loop_Invariant (J <= Character'Pos (C) + 1); + pragma Loop_Invariant (Result (1 .. J)'Initialized); + pragma Loop_Invariant (for all K in 1 .. J => Result (K) <= C); + pragma Loop_Invariant + (SPARK_Proof_Sorted_Character_Sequence (Result (1 .. J))); + pragma Loop_Invariant + (for all D in Map'First .. C => + (if Map (D) = D then + Indexes (D) = 0 + else + Indexes (D) in 1 .. J + and then Result (Indexes (D)) = D)); + pragma Loop_Invariant + (for all Char of Result (1 .. J) => Map (Char) /= Char); end loop; return Result (1 .. J); @@ -146,7 +173,7 @@ package body Ada.Strings.Maps is function To_Mapping (From, To : Character_Sequence) return Character_Mapping is - Result : Character_Mapping; + Result : Character_Mapping with Relaxed_Initialization; Inserted : Character_Set := Null_Set; From_Len : constant Natural := From'Length; To_Len : constant Natural := To'Length; @@ -158,6 +185,9 @@ package body Ada.Strings.Maps is for Char in Character loop Result (Char) := Char; + pragma Loop_Invariant (Result (Result'First .. Char)'Initialized); + pragma Loop_Invariant + (for all C in Result'First .. Char => Result (C) = C); end loop; for J in From'Range loop @@ -167,6 +197,23 @@ package body Ada.Strings.Maps is Result (From (J)) := To (J - From'First + To'First); Inserted (From (J)) := True; + + pragma Loop_Invariant (Result'Initialized); + pragma Loop_Invariant + (for all K in From'First .. J => + Result (From (K)) = To (K - From'First + To'First) + and then Inserted (From (K))); + pragma Loop_Invariant + (for all Char in Character => + (Inserted (Char) = + (for some K in From'First .. J => Char = From (K)))); + pragma Loop_Invariant + (for all Char in Character => + (if not Inserted (Char) then Result (Char) = Char)); + pragma Loop_Invariant + (if (for all K in From'First .. J => + From (K) = To (J - From'First + To'First)) + then Result = Identity); end loop; return Result; @@ -176,19 +223,195 @@ package body Ada.Strings.Maps is -- To_Range -- -------------- - function To_Range (Map : Character_Mapping) return Character_Sequence - is - Result : String (1 .. Map'Length); + function To_Range (Map : Character_Mapping) return Character_Sequence is + + -- Extract from the postcondition of To_Domain the essential properties + -- that define Seq as the domain of Map. + function Is_Domain + (Map : Character_Mapping; + Seq : Character_Sequence) + return Boolean + is + (Seq'First = 1 + and then + SPARK_Proof_Sorted_Character_Sequence (Seq) + and then + (for all Char in Character => + (if (for all X of Seq => X /= Char) + then Map (Char) = Char)) + and then + (for all Char of Seq => Map (Char) /= Char)) + with + Ghost; + + -- Given Map, there is a unique sequence Seq for which + -- Is_Domain(Map,Seq) holds. + procedure Lemma_Domain_Unicity + (Map : Character_Mapping; + Seq1, Seq2 : Character_Sequence) + with + Ghost, + Pre => Is_Domain (Map, Seq1) + and then Is_Domain (Map, Seq2), + Post => Seq1 = Seq2; + + -- Isolate the proof that To_Domain(Map) returns a sequence for which + -- Is_Domain holds. + procedure Lemma_Is_Domain (Map : Character_Mapping) + with + Ghost, + Post => Is_Domain (Map, To_Domain (Map)); + + -- Deduce the alternative expression of sortedness from the one in + -- SPARK_Proof_Sorted_Character_Sequence which compares consecutive + -- elements. + procedure Lemma_Is_Sorted (Seq : Character_Sequence) + with + Ghost, + Pre => SPARK_Proof_Sorted_Character_Sequence (Seq), + Post => (for all J in Seq'Range => + (for all K in Seq'Range => + (if J < K then Seq (J) < Seq (K)))); + + -------------------------- + -- Lemma_Domain_Unicity -- + -------------------------- + + procedure Lemma_Domain_Unicity + (Map : Character_Mapping; + Seq1, Seq2 : Character_Sequence) + is + J : Positive := 1; + + begin + while J <= Seq1'Last + and then J <= Seq2'Last + and then Seq1 (J) = Seq2 (J) + loop + pragma Loop_Invariant + (Seq1 (Seq1'First .. J) = Seq2 (Seq2'First .. J)); + + if J = Positive'Last then + return; + end if; + + J := J + 1; + end loop; + + Lemma_Is_Sorted (Seq1); + Lemma_Is_Sorted (Seq2); + + if J <= Seq1'Last + and then J <= Seq2'Last + then + if Seq1 (J) < Seq2 (J) then + pragma Assert (for all X of Seq2 => X /= Seq1 (J)); + pragma Assert (Map (Seq1 (J)) = Seq1 (J)); + pragma Assert (False); + else + pragma Assert (for all X of Seq1 => X /= Seq2 (J)); + pragma Assert (Map (Seq2 (J)) = Seq2 (J)); + pragma Assert (False); + end if; + + elsif J <= Seq1'Last then + pragma Assert (for all X of Seq2 => X /= Seq1 (J)); + pragma Assert (Map (Seq1 (J)) = Seq1 (J)); + pragma Assert (False); + + elsif J <= Seq2'Last then + pragma Assert (for all X of Seq1 => X /= Seq2 (J)); + pragma Assert (Map (Seq2 (J)) = Seq2 (J)); + pragma Assert (False); + end if; + end Lemma_Domain_Unicity; + + --------------------- + -- Lemma_Is_Domain -- + --------------------- + + procedure Lemma_Is_Domain (Map : Character_Mapping) is + Ignore : constant Character_Sequence := To_Domain (Map); + begin + null; + end Lemma_Is_Domain; + + --------------------- + -- Lemma_Is_Sorted -- + --------------------- + + procedure Lemma_Is_Sorted (Seq : Character_Sequence) is + begin + for A in Seq'Range loop + exit when A = Positive'Last; + + for B in A + 1 .. Seq'Last loop + pragma Loop_Invariant + (for all K in A + 1 .. B => Seq (A) < Seq (K)); + end loop; + + pragma Loop_Invariant + (for all J in Seq'First .. A => + (for all K in Seq'Range => + (if J < K then Seq (J) < Seq (K)))); + end loop; + end Lemma_Is_Sorted; + + -- Local variables + + Result : String (1 .. Map'Length) with Relaxed_Initialization; J : Natural; + + -- Repeat the computation from To_Domain in ghost code, in order to + -- prove the relationship between Result and To_Domain(Map). + + Domain : String (1 .. Map'Length) with Ghost, Relaxed_Initialization; + type Character_Index is array (Character) of Natural with Ghost; + Indexes : Character_Index := (others => 0) with Ghost; + + -- Start of processing for To_Range + begin J := 0; for C in Map'Range loop if Map (C) /= C then J := J + 1; Result (J) := Map (C); + Domain (J) := C; + Indexes (C) := J; end if; + + -- Repeat the loop invariants from To_Domain regarding Domain and + -- Indexes. Add similar loop invariants for Result and Indexes. + + pragma Loop_Invariant (J <= Character'Pos (C) + 1); + pragma Loop_Invariant (Result (1 .. J)'Initialized); + pragma Loop_Invariant (Domain (1 .. J)'Initialized); + pragma Loop_Invariant (for all K in 1 .. J => Domain (K) <= C); + pragma Loop_Invariant + (SPARK_Proof_Sorted_Character_Sequence (Domain (1 .. J))); + pragma Loop_Invariant + (for all D in Map'First .. C => + (if Map (D) = D then + Indexes (D) = 0 + else + Indexes (D) in 1 .. J + and then Domain (Indexes (D)) = D + and then Result (Indexes (D)) = Map (D))); + pragma Loop_Invariant + (for all Char of Domain (1 .. J) => Map (Char) /= Char); + pragma Loop_Invariant + (for all K in 1 .. J => Result (K) = Map (Domain (K))); end loop; + -- Show the equality of Domain and To_Domain(Map) + + Lemma_Is_Domain (Map); + Lemma_Domain_Unicity (Map, Domain (1 .. J), To_Domain (Map)); + pragma Assert + (for all K in 1 .. J => Domain (K) = To_Domain (Map) (K)); + pragma Assert (To_Domain (Map)'Length = J); + return Result (1 .. J); end To_Range; @@ -197,18 +420,26 @@ package body Ada.Strings.Maps is --------------- function To_Ranges (Set : Character_Set) return Character_Ranges is - Max_Ranges : Character_Ranges (1 .. Set'Length / 2 + 1); + Max_Ranges : Character_Ranges (1 .. Set'Length / 2 + 1) + with Relaxed_Initialization; Range_Num : Natural; C : Character; + C_Iter : Character with Ghost; begin C := Character'First; Range_Num := 0; loop + C_Iter := C; + -- Skip gap between subsets while not Set (C) loop + pragma Loop_Invariant + (Character'Pos (C) >= Character'Pos (C'Loop_Entry)); + pragma Loop_Invariant + (for all Char in C'Loop_Entry .. C => not Set (Char)); exit when C = Character'Last; C := Character'Succ (C); end loop; @@ -221,16 +452,45 @@ package body Ada.Strings.Maps is -- Span a subset loop + pragma Loop_Invariant + (Character'Pos (C) >= Character'Pos (C'Loop_Entry)); + pragma Loop_Invariant + (for all Char in C'Loop_Entry .. C => + (if Char /= C then Set (Char))); exit when not Set (C) or else C = Character'Last; C := Character'Succ (C); end loop; if Set (C) then - Max_Ranges (Range_Num). High := C; + Max_Ranges (Range_Num).High := C; exit; else - Max_Ranges (Range_Num). High := Character'Pred (C); + Max_Ranges (Range_Num).High := Character'Pred (C); end if; + + pragma Assert + (for all Char in C_Iter .. C => + (Set (Char) = + (Char in Max_Ranges (Range_Num).Low .. + Max_Ranges (Range_Num).High))); + pragma Assert + (for all Char in Character'First .. C_Iter => + (if Char /= C_Iter then + (Set (Char) = + (for some Span of Max_Ranges (1 .. Range_Num - 1) => + Char in Span.Low .. Span.High)))); + + pragma Loop_Invariant (2 * Range_Num <= Character'Pos (C) + 1); + pragma Loop_Invariant (Max_Ranges (1 .. Range_Num)'Initialized); + pragma Loop_Invariant (not Set (C)); + pragma Loop_Invariant + (for all Char in Character'First .. C => + (Set (Char) = + (for some Span of Max_Ranges (1 .. Range_Num) => + Char in Span.Low .. Span.High))); + pragma Loop_Invariant + (for all Span of Max_Ranges (1 .. Range_Num) => + (for all Char in Span.Low .. Span.High => Set (Char))); end loop; return Max_Ranges (1 .. Range_Num); @@ -241,7 +501,8 @@ package body Ada.Strings.Maps is ----------------- function To_Sequence (Set : Character_Set) return Character_Sequence is - Result : String (1 .. Character'Pos (Character'Last) + 1); + Result : String (1 .. Character'Pos (Character'Last) + 1) + with Relaxed_Initialization; Count : Natural := 0; begin for Char in Set'Range loop @@ -249,6 +510,17 @@ package body Ada.Strings.Maps is Count := Count + 1; Result (Count) := Char; end if; + + pragma Loop_Invariant (Count <= Character'Pos (Char) + 1); + pragma Loop_Invariant (Result (1 .. Count)'Initialized); + pragma Loop_Invariant (for all K in 1 .. Count => Result (K) <= Char); + pragma Loop_Invariant + (SPARK_Proof_Sorted_Character_Sequence (Result (1 .. Count))); + pragma Loop_Invariant + (for all C in Set'First .. Char => + (Set (C) = (for some X of Result (1 .. Count) => C = X))); + pragma Loop_Invariant + (for all Char of Result (1 .. Count) => Is_In (Char, Set)); end loop; return Result (1 .. Count); @@ -259,30 +531,37 @@ package body Ada.Strings.Maps is ------------ function To_Set (Ranges : Character_Ranges) return Character_Set is - Result : Character_Set; + Result : Character_Set := Null_Set; begin - for C in Result'Range loop - Result (C) := False; - end loop; - for R in Ranges'Range loop for C in Ranges (R).Low .. Ranges (R).High loop Result (C) := True; + pragma Loop_Invariant + (for all Char in Character => + Result (Char) = + ((for some Prev in Ranges'First .. R - 1 => + Char in Ranges (Prev).Low .. Ranges (Prev).High) + or else (Char in Ranges (R).Low .. C))); end loop; + + pragma Loop_Invariant + (for all Char in Character => + Result (Char) = + (for some Prev in Ranges'First .. R => + Char in Ranges (Prev).Low .. Ranges (Prev).High)); end loop; return Result; end To_Set; function To_Set (Span : Character_Range) return Character_Set is - Result : Character_Set; + Result : Character_Set := Null_Set; begin - for C in Result'Range loop - Result (C) := False; - end loop; - for C in Span.Low .. Span.High loop Result (C) := True; + pragma Loop_Invariant + (for all Char in Character => + Result (Char) = (Char in Span.Low .. C)); end loop; return Result; @@ -293,6 +572,10 @@ package body Ada.Strings.Maps is begin for J in Sequence'Range loop Result (Sequence (J)) := True; + pragma Loop_Invariant + (for all Char in Character => + Result (Char) = + (for some K in Sequence'First .. J => Char = Sequence (K))); end loop; return Result; @@ -313,8 +596,6 @@ package body Ada.Strings.Maps is (Map : Character_Mapping; Element : Character) return Character is - begin - return Map (Element); - end Value; + (Map (Element)); end Ada.Strings.Maps; diff --git a/gcc/ada/libgnat/a-strmap.ads b/gcc/ada/libgnat/a-strmap.ads index ffc69a92136b..1a15d5dc2d6e 100644 --- a/gcc/ada/libgnat/a-strmap.ads +++ b/gcc/ada/libgnat/a-strmap.ads @@ -33,6 +33,9 @@ -- -- ------------------------------------------------------------------------------ +-- The package Strings.Maps defines the types, operations, and other entities +-- needed for character sets and character-to-character mappings. + -- 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 @@ -45,7 +48,9 @@ pragma Assertion_Policy (Pre => Ignore, with Ada.Characters.Latin_1; -package Ada.Strings.Maps is +package Ada.Strings.Maps + with SPARK_Mode +is pragma Pure; -- In accordance with Ada 2005 AI-362 @@ -55,9 +60,10 @@ package Ada.Strings.Maps is type Character_Set is private; pragma Preelaborable_Initialization (Character_Set); - -- Representation for a set of character values: + -- An object of type Character_Set represents a set of characters. Null_Set : constant Character_Set; + -- Null_Set represents the set containing no characters. --------------------------- -- Constructors for Sets -- @@ -67,9 +73,12 @@ package Ada.Strings.Maps is Low : Character; High : Character; end record; - -- Represents Character range Low .. High + -- An object Obj of type Character_Range represents the set of characters + -- in the range Obj.Low .. Obj.High. type Character_Ranges is array (Positive range <>) of Character_Range; + -- An object Obj of type Character_Ranges represents the union of the sets + -- corresponding to Obj(I) for I in Obj'Range. function To_Set (Ranges : Character_Ranges) return Character_Set with Post => @@ -82,6 +91,8 @@ package Ada.Strings.Maps is (for all Span of Ranges => (for all Char in Span.Low .. Span.High => Is_In (Char, To_Set'Result))); + -- If Ranges'Length=0 then Null_Set is returned; otherwise, the returned + -- value represents the set corresponding to Ranges. function To_Set (Span : Character_Range) return Character_Set with Post => @@ -91,6 +102,7 @@ package Ada.Strings.Maps is (if Is_In (Char, To_Set'Result) then Char in Span.Low .. Span.High)) and then (for all Char in Span.Low .. Span.High => Is_In (Char, To_Set'Result)); + -- The returned value represents the set containing each character in Span. function To_Ranges (Set : Character_Set) return Character_Ranges with Post => @@ -104,6 +116,12 @@ package Ada.Strings.Maps is and then (for all Span of To_Ranges'Result => (for all Char in Span.Low .. Span.High => Is_In (Char, Set))); + -- If Set = Null_Set, then an empty Character_Ranges array is returned; + -- otherwise, the shortest array of contiguous ranges of Character values + -- in Set, in increasing order of Low, is returned. + -- + -- The postcondition above does not express that the result is the shortest + -- array and that it is sorted. ---------------------------------- -- Operations on Character Sets -- @@ -115,6 +133,13 @@ package Ada.Strings.Maps is = (for all Char in Character => (Is_In (Char, Left) = Is_In (Char, Right))); + -- The function "=" returns True if Left and Right represent identical + -- sets, and False otherwise. + + -- Each of the logical operators "not", "and", "or", and "xor" returns a + -- Character_Set value that represents the set obtained by applying the + -- corresponding operation to the set(s) represented by the parameter(s) + -- of the operator. function "not" (Right : Character_Set) return Character_Set with Post => @@ -150,10 +175,12 @@ package Ada.Strings.Maps is (Is_In (Char, "-"'Result) = (Is_In (Char, Left) and not Is_In (Char, Right)))); + -- "-"(Left, Right) is equivalent to "and"(Left, "not"(Right)). function Is_In (Element : Character; Set : Character_Set) return Boolean; + -- Is_In returns True if Element is in Set, and False otherwise. function Is_Subset (Elements : Character_Set; @@ -164,6 +191,8 @@ package Ada.Strings.Maps is = (for all Char in Character => (if Is_In (Char, Elements) then Is_In (Char, Set))); + -- Is_Subset returns True if Elements is a subset of Set, and False + -- otherwise. function "<=" (Left : Character_Set; @@ -171,7 +200,23 @@ package Ada.Strings.Maps is renames Is_Subset; subtype Character_Sequence is String; - -- Alternative representation for a set of character values + -- The Character_Sequence subtype is used to portray a set of character + -- values and also to identify the domain and range of a character mapping. + + function SPARK_Proof_Sorted_Character_Sequence + (Seq : Character_Sequence) return Boolean + is + (for all J in Seq'Range => + (if J /= Seq'Last then Seq (J) < Seq (J + 1))) + with + Ghost; + -- Check whether the Character_Sequence is sorted in stricly increasing + -- order, as expected from the result of To_Sequence and To_Domain. + + -- Sequence portrays the set of character values that it explicitly + -- contains (ignoring duplicates). Singleton portrays the set comprising a + -- single Character. Each of the To_Set functions returns a Character_Set + -- value that represents the set portrayed by Sequence or Singleton. function To_Set (Sequence : Character_Sequence) return Character_Set with Post => @@ -201,10 +246,10 @@ package Ada.Strings.Maps is and then (for all Char of To_Sequence'Result => Is_In (Char, Set)) and then - (for all J in To_Sequence'Result'Range => - (for all K in To_Sequence'Result'Range => - (if J /= K - then To_Sequence'Result (J) /= To_Sequence'Result (K)))); + SPARK_Proof_Sorted_Character_Sequence (To_Sequence'Result); + -- The function To_Sequence returns a Character_Sequence value containing + -- each of the characters in the set represented by Set, in ascending order + -- with no duplicates. ------------------------------------ -- Character Mapping Declarations -- @@ -212,7 +257,8 @@ package Ada.Strings.Maps is type Character_Mapping is private; pragma Preelaborable_Initialization (Character_Mapping); - -- Representation for a character to character mapping: + -- An object of type Character_Mapping represents a Character-to-Character + -- mapping. type SPARK_Proof_Character_Mapping_Model is array (Character) of Character @@ -233,7 +279,17 @@ package Ada.Strings.Maps is -- The function Value returns the Character value to which Element maps -- with respect to the mapping represented by Map. + -- A character C matches a pattern character P with respect to a given + -- Character_Mapping value Map if Value(Map, C) = P. A string S matches + -- a pattern string P with respect to a given Character_Mapping if + -- their lengths are the same and if each character in S matches its + -- corresponding character in the pattern string P. + + -- String handling subprograms that deal with character mappings have + -- parameters whose type is Character_Mapping. + Identity : constant Character_Mapping; + -- Identity maps each Character to itself. ---------------------------- -- Operations on Mappings -- @@ -259,6 +315,10 @@ package Ada.Strings.Maps is and then (if (for all X of From => Char /= X) then Value (To_Mapping'Result, Char) = Char))); + -- To_Mapping produces a Character_Mapping such that each element of From + -- maps to the corresponding element of To, and each other character maps + -- to itself. If From'Length /= To'Length, or if some character is repeated + -- in From, then Translation_Error is propagated. function To_Domain (Map : Character_Mapping) return Character_Sequence with @@ -267,24 +327,40 @@ package Ada.Strings.Maps is and then To_Domain'Result'First = 1 and then + SPARK_Proof_Sorted_Character_Sequence (To_Domain'Result) + and then (for all Char in Character => (if (for all X of To_Domain'Result => X /= Char) then Value (Map, Char) = Char)) and then (for all Char of To_Domain'Result => Value (Map, Char) /= Char); + -- To_Domain returns the shortest Character_Sequence value D such that each + -- character not in D maps to itself, and such that the characters in D are + -- in ascending order. The lower bound of D is 1. function To_Range (Map : Character_Mapping) return Character_Sequence with Post => To_Range'Result'First = 1 and then - To_Range'Result'Last = To_Domain (Map)'Last + To_Range'Result'Length = To_Domain (Map)'Length and then (for all J in To_Range'Result'Range => To_Range'Result (J) = Value (Map, To_Domain (Map) (J))); + -- To_Range returns the Character_Sequence value R, such that if D = + -- To_Domain(Map), then R has the same bounds as D, and D(I) maps to + -- R(I) for each I in D'Range. + -- + -- A direct encoding of the Ada RM would be the postcondition + -- To_Range'Result'Last = To_Domain (Map)'Last + -- which is not provable unless the postcondition of To_Domain is also + -- strengthened to state the value of the high bound for an empty result. type Character_Mapping_Function is access function (From : Character) return Character; + -- An object F of type Character_Mapping_Function maps a Character value C + -- to the Character value F.all(C), which is said to match C with respect + -- to mapping function F. private pragma Inline (Is_In);