-- 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
---------
-- "-" --
(Element : Character;
Set : Character_Set) return Boolean
is
- begin
- return Set (Element);
- end Is_In;
+ (Set (Element));
---------------
-- Is_Subset --
-- 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);
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;
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
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;
-- 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;
---------------
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;
-- 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);
-----------------
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
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);
------------
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;
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;
(Map : Character_Mapping;
Element : Character) return Character
is
- begin
- return Map (Element);
- end Value;
+ (Map (Element));
end Ada.Strings.Maps;
-- --
------------------------------------------------------------------------------
+-- 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
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
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 --
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 =>
(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 =>
(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 =>
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 --
=
(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 =>
(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;
=
(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;
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 =>
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 --
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
-- 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 --
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
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);
projects / thirdparty / gcc.git / commitdiff
