| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT RUN-TIME COMPONENTS -- |
| -- -- |
| -- A D A . S T R I N G S . M A P S -- |
| -- -- |
| -- B o d y -- |
| -- -- |
| -- Copyright (C) 1992-2022, Free Software Foundation, Inc. -- |
| -- -- |
| -- GNAT is free software; you can redistribute it and/or modify it under -- |
| -- terms of the GNU General Public License as published by the Free Soft- -- |
| -- ware Foundation; either version 3, or (at your option) any later ver- -- |
| -- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- |
| -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- |
| -- or FITNESS FOR A PARTICULAR PURPOSE. -- |
| -- -- |
| -- As a special exception under Section 7 of GPL version 3, you are granted -- |
| -- additional permissions described in the GCC Runtime Library Exception, -- |
| -- version 3.1, as published by the Free Software Foundation. -- |
| -- -- |
| -- You should have received a copy of the GNU General Public License and -- |
| -- a copy of the GCC Runtime Library Exception along with this program; -- |
| -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- |
| -- <http://www.gnu.org/licenses/>. -- |
| -- -- |
| -- GNAT was originally developed by the GNAT team at New York University. -- |
| -- Extensive contributions were provided by Ada Core Technologies Inc. -- |
| -- -- |
| ------------------------------------------------------------------------------ |
| |
| -- Note: parts of this code are derived from the ADAR.CSH public domain |
| -- Ada 83 versions of the Appendix C string handling packages. The main |
| -- differences are that we avoid the use of the minimize function which |
| -- is bit-by-bit or character-by-character and therefore rather slow. |
| -- Generally for character sets we favor the full 32-byte representation. |
| |
| -- 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 |
| |
| --------- |
| -- "-" -- |
| --------- |
| |
| function "-" (Left, Right : Character_Set) return Character_Set is |
| begin |
| return Left and not Right; |
| end "-"; |
| |
| --------- |
| -- "=" -- |
| --------- |
| |
| function "=" (Left, Right : Character_Set) return Boolean is |
| begin |
| return Character_Set_Internal (Left) = Character_Set_Internal (Right); |
| end "="; |
| |
| ----------- |
| -- "and" -- |
| ----------- |
| |
| function "and" (Left, Right : Character_Set) return Character_Set is |
| begin |
| return Character_Set |
| (Character_Set_Internal (Left) and Character_Set_Internal (Right)); |
| end "and"; |
| |
| ----------- |
| -- "not" -- |
| ----------- |
| |
| function "not" (Right : Character_Set) return Character_Set is |
| begin |
| return Character_Set (not Character_Set_Internal (Right)); |
| end "not"; |
| |
| ---------- |
| -- "or" -- |
| ---------- |
| |
| function "or" (Left, Right : Character_Set) return Character_Set is |
| begin |
| return Character_Set |
| (Character_Set_Internal (Left) or Character_Set_Internal (Right)); |
| end "or"; |
| |
| ----------- |
| -- "xor" -- |
| ----------- |
| |
| function "xor" (Left, Right : Character_Set) return Character_Set is |
| begin |
| return Character_Set |
| (Character_Set_Internal (Left) xor Character_Set_Internal (Right)); |
| end "xor"; |
| |
| ----------- |
| -- Is_In -- |
| ----------- |
| |
| function Is_In |
| (Element : Character; |
| Set : Character_Set) return Boolean |
| is |
| (Set (Element)); |
| |
| --------------- |
| -- Is_Subset -- |
| --------------- |
| |
| function Is_Subset |
| (Elements : Character_Set; |
| Set : Character_Set) return Boolean |
| is |
| begin |
| return (Elements and Set) = Elements; |
| end Is_Subset; |
| |
| --------------- |
| -- To_Domain -- |
| --------------- |
| |
| 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); |
| end To_Domain; |
| |
| ---------------- |
| -- To_Mapping -- |
| ---------------- |
| |
| function To_Mapping |
| (From, To : Character_Sequence) return Character_Mapping |
| is |
| Result : Character_Mapping with Relaxed_Initialization; |
| Inserted : Character_Set := Null_Set; |
| From_Len : constant Natural := From'Length; |
| To_Len : constant Natural := To'Length; |
| |
| begin |
| if From_Len /= To_Len then |
| raise Strings.Translation_Error; |
| end if; |
| |
| 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 |
| if Inserted (From (J)) then |
| raise Strings.Translation_Error; |
| end if; |
| |
| 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; |
| end To_Mapping; |
| |
| -------------- |
| -- To_Range -- |
| -------------- |
| |
| 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; |
| |
| --------------- |
| -- To_Ranges -- |
| --------------- |
| |
| function To_Ranges (Set : Character_Set) return Character_Ranges is |
| 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; |
| |
| exit when not Set (C); |
| |
| Range_Num := Range_Num + 1; |
| Max_Ranges (Range_Num).Low := C; |
| |
| -- 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; |
| exit; |
| else |
| 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); |
| end To_Ranges; |
| |
| ----------------- |
| -- To_Sequence -- |
| ----------------- |
| |
| function To_Sequence (Set : Character_Set) return Character_Sequence is |
| Result : String (1 .. Character'Pos (Character'Last) + 1) |
| with Relaxed_Initialization; |
| Count : Natural := 0; |
| begin |
| for Char in Set'Range loop |
| if Set (Char) then |
| 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); |
| end To_Sequence; |
| |
| ------------ |
| -- To_Set -- |
| ------------ |
| |
| function To_Set (Ranges : Character_Ranges) return Character_Set is |
| Result : Character_Set := Null_Set; |
| begin |
| 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 := Null_Set; |
| begin |
| 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; |
| end To_Set; |
| |
| function To_Set (Sequence : Character_Sequence) return Character_Set is |
| Result : Character_Set := Null_Set; |
| 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; |
| end To_Set; |
| |
| function To_Set (Singleton : Character) return Character_Set is |
| Result : Character_Set := Null_Set; |
| begin |
| Result (Singleton) := True; |
| return Result; |
| end To_Set; |
| |
| ----------- |
| -- Value -- |
| ----------- |
| |
| function Value |
| (Map : Character_Mapping; |
| Element : Character) return Character |
| is |
| (Map (Element)); |
| |
| end Ada.Strings.Maps; |
