From f2acfbce60d8225bff9f469a68606ebd2fe54736 Mon Sep 17 00:00:00 2001 From: Claire Dross Date: Thu, 27 Apr 2017 12:55:29 +0000 Subject: [PATCH] a-cforma.adb, [...] (=): Generic parameter removed to allow the use of regular equality over elements in... 2017-04-27 Claire Dross * a-cforma.adb, a-cforma.ads (=): Generic parameter removed to allow the use of regular equality over elements in contracts. (Formal_Model): Ghost package containing model functions that are used in subprogram contracts. (Current_To_Last): Removed, model functions should be used instead. (First_To_Previous): Removed, model functions should be used instead. (Strict_Equal): Removed, model functions should be used instead. (No_Overlap): Removed, model functions should be used instead. * a-cofuma.adb, a-cofuma.ads (Enable_Handling_Of_Equivalence) Boolean generic parameter to disable contracts for equivalence between keys. (Witness): Create a witness of a key that is used for handling of equivalence between keys. (Has_Witness): Check whether a witness is contained in a map. (W_Get): Get the element associated to a witness. (Lift_Equivalent_Keys): Removed, equivalence between keys is handled directly. * a-cofuse.adb, a-cofuse.ads (Enable_Handling_Of_Equivalence) Boolean generic parameter to disable contracts for equivalence between keys. * a-cfhama.adb, a-cfhama.ads (Formal_Model.P) Disable handling of equivalence on functional maps. * a-cfdlli.adb, a-cfdlli.ads (Formal_Model.P) Disable handling of equivalence on functional maps. From-SVN: r247328 --- gcc/ada/ChangeLog | 27 ++ gcc/ada/a-cfdlli.ads | 7 +- gcc/ada/a-cfhama.ads | 17 +- gcc/ada/a-cforma.adb | 323 +++++++++++------- gcc/ada/a-cforma.ads | 947 +++++++++++++++++++++++++++++++++++++++++++++------ gcc/ada/a-cofuma.adb | 32 +- gcc/ada/a-cofuma.ads | 83 +++-- gcc/ada/a-cofuse.ads | 17 +- 8 files changed, 1181 insertions(+), 272 deletions(-) diff --git a/gcc/ada/ChangeLog b/gcc/ada/ChangeLog index 44c6ed5..83b6596 100644 --- a/gcc/ada/ChangeLog +++ b/gcc/ada/ChangeLog @@ -1,3 +1,30 @@ +2017-04-27 Claire Dross + + * a-cforma.adb, a-cforma.ads (=): Generic parameter removed to + allow the use of regular equality over elements in contracts. + (Formal_Model): Ghost package containing model functions that + are used in subprogram contracts. + (Current_To_Last): Removed, model functions should be used instead. + (First_To_Previous): Removed, model functions should be used instead. + (Strict_Equal): Removed, model functions should be used instead. + (No_Overlap): Removed, model functions should be used instead. + * a-cofuma.adb, a-cofuma.ads (Enable_Handling_Of_Equivalence) + Boolean generic parameter to disable contracts for equivalence + between keys. + (Witness): Create a witness of a key that is used for handling of + equivalence between keys. + (Has_Witness): Check whether a witness is contained in a map. + (W_Get): Get the element associated to a witness. + (Lift_Equivalent_Keys): Removed, equivalence between keys is handled + directly. + * a-cofuse.adb, a-cofuse.ads (Enable_Handling_Of_Equivalence) + Boolean generic parameter to disable contracts for equivalence + between keys. + * a-cfhama.adb, a-cfhama.ads (Formal_Model.P) Disable handling + of equivalence on functional maps. + * a-cfdlli.adb, a-cfdlli.ads (Formal_Model.P) Disable handling + of equivalence on functional maps. + 2017-04-27 Hristian Kirtchev * exp_ch9.adb (Expand_Entry_Barrier): Code diff --git a/gcc/ada/a-cfdlli.ads b/gcc/ada/a-cfdlli.ads index 596af5e..0bd57bf 100644 --- a/gcc/ada/a-cfdlli.ads +++ b/gcc/ada/a-cfdlli.ads @@ -151,9 +151,10 @@ is pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped); package P is new Ada.Containers.Functional_Maps - (Key_Type => Cursor, - Element_Type => Positive_Count_Type, - Equivalent_Keys => "="); + (Key_Type => Cursor, + Element_Type => Positive_Count_Type, + Equivalent_Keys => "=", + Enable_Handling_Of_Equivalence => False); function "=" (Left : P.Map; diff --git a/gcc/ada/a-cfhama.ads b/gcc/ada/a-cfhama.ads index 452e5ee..533a3bf 100644 --- a/gcc/ada/a-cfhama.ads +++ b/gcc/ada/a-cfhama.ads @@ -68,7 +68,7 @@ is Next => Next, Has_Element => Has_Element, Element => Key), - Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0; + Default_Initial_Condition => Is_Empty (Map); pragma Preelaborable_Initialization (Map); Empty_Map : constant Map; @@ -118,9 +118,10 @@ is Right : K.Sequence) return Boolean renames K."<="; package P is new Ada.Containers.Functional_Maps - (Key_Type => Cursor, - Element_Type => Positive_Count_Type, - Equivalent_Keys => "="); + (Key_Type => Cursor, + Element_Type => Positive_Count_Type, + Equivalent_Keys => "=", + Enable_Handling_Of_Equivalence => False); function "=" (Left : P.Map; @@ -262,7 +263,7 @@ is function Is_Empty (Container : Map) return Boolean with Global => null, - Post => Is_Empty'Result = M.Is_Empty (Model (Container)); + Post => Is_Empty'Result = (Length (Container) = 0); procedure Clear (Container : in out Map) with Global => null, @@ -503,6 +504,12 @@ is Model (Container)'Old, Key) + -- Key is inserted in Container + + and K.Get (Keys (Container), + P.Get (Positions (Container), Find (Container, Key))) = + Key + -- Mapping from cursors to keys is preserved and Mapping_Preserved diff --git a/gcc/ada/a-cforma.adb b/gcc/ada/a-cforma.adb index 4bf302d..c54515b 100644 --- a/gcc/ada/a-cforma.adb +++ b/gcc/ada/a-cforma.adb @@ -6,7 +6,7 @@ -- -- -- B o d y -- -- -- --- Copyright (C) 2010-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 2010-2017, 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- -- @@ -324,34 +324,6 @@ is end return; end Copy; - --------------------- - -- Current_To_Last -- - --------------------- - - function Current_To_Last (Container : Map; Current : Cursor) return Map is - Curs : Cursor := First (Container); - C : Map (Container.Capacity) := Copy (Container, Container.Capacity); - Node : Count_Type; - - begin - if Curs = No_Element then - Clear (C); - return C; - - elsif Current /= No_Element and not Has_Element (Container, Current) then - raise Constraint_Error; - - else - while Curs.Node /= Current.Node loop - Node := Curs.Node; - Delete (C, Curs); - Curs := Next (Container, (Node => Node)); - end loop; - - return C; - end if; - end Current_To_Last; - ------------ -- Delete -- ------------ @@ -369,6 +341,7 @@ is Tree_Operations.Delete_Node_Sans_Free (Container, Position.Node); Formal_Ordered_Maps.Free (Container, Position.Node); + Position := No_Element; end Delete; procedure Delete (Container : in out Map; Key : Key_Type) is @@ -520,36 +493,6 @@ is return Container.Nodes (First (Container).Node).Key; end First_Key; - ----------------------- - -- First_To_Previous -- - ----------------------- - - function First_To_Previous - (Container : Map; - Current : Cursor) return Map - is - Curs : Cursor := Current; - C : Map (Container.Capacity) := Copy (Container, Container.Capacity); - Node : Count_Type; - - begin - if Curs = No_Element then - return C; - - elsif not Has_Element (Container, Curs) then - raise Constraint_Error; - - else - while Curs.Node /= 0 loop - Node := Curs.Node; - Delete (C, Curs); - Curs := Next (Container, (Node => Node)); - end loop; - - return C; - end if; - end First_To_Previous; - ----------- -- Floor -- ----------- @@ -565,6 +508,196 @@ is return (Node => Node); end Floor; + ------------------ + -- Formal_Model -- + ------------------ + + package body Formal_Model is + + ------------------------- + -- K_Bigger_Than_Range -- + ------------------------- + + function K_Bigger_Than_Range + (Container : K.Sequence; + Fst : Positive_Count_Type; + Lst : Count_Type; + Key : Key_Type) return Boolean + is + begin + for I in Fst .. Lst loop + if not (K.Get (Container, I) < Key) then + return False; + end if; + end loop; + return True; + end K_Bigger_Than_Range; + + --------------- + -- K_Is_Find -- + --------------- + + function K_Is_Find + (Container : K.Sequence; + Key : Key_Type; + Position : Count_Type) return Boolean + is + begin + for I in 1 .. Position - 1 loop + if Key < K.Get (Container, I) then + return False; + end if; + end loop; + + if Position < K.Length (Container) then + for I in Position + 1 .. K.Length (Container) loop + if K.Get (Container, I) < Key then + return False; + end if; + end loop; + end if; + return True; + end K_Is_Find; + + -------------------------- + -- K_Smaller_Than_Range -- + -------------------------- + + function K_Smaller_Than_Range + (Container : K.Sequence; + Fst : Positive_Count_Type; + Lst : Count_Type; + Key : Key_Type) return Boolean + is + begin + for I in Fst .. Lst loop + if not (Key < K.Get (Container, I)) then + return False; + end if; + end loop; + return True; + end K_Smaller_Than_Range; + + ---------- + -- Keys -- + ---------- + + function Keys (Container : Map) return K.Sequence is + Position : Count_Type := Container.First; + R : K.Sequence; + + begin + -- Can't use First, Next or Element here, since they depend on models + -- for their postconditions. + + while Position /= 0 loop + R := K.Add (R, Container.Nodes (Position).Key); + Position := Tree_Operations.Next (Container, Position); + end loop; + + return R; + end Keys; + + ---------------------------- + -- Lift_Abstraction_Level -- + ---------------------------- + + procedure Lift_Abstraction_Level (Container : Map) is null; + + ----------- + -- Model -- + ----------- + + function Model (Container : Map) return M.Map is + Position : Count_Type := Container.First; + R : M.Map; + + begin + -- Can't use First, Next or Element here, since they depend on models + -- for their postconditions. + + while Position /= 0 loop + R := M.Add (Container => R, + New_Key => Container.Nodes (Position).Key, + New_Item => Container.Nodes (Position).Element); + Position := Tree_Operations.Next (Container, Position); + end loop; + + return R; + end Model; + + ------------------------- + -- P_Positions_Shifted -- + ------------------------- + + function P_Positions_Shifted + (Small : P.Map; + Big : P.Map; + Cut : Positive_Count_Type; + Count : Count_Type := 1) return Boolean + is + begin + for Cu of Small loop + if not P.Has_Key (Big, Cu) then + return False; + end if; + end loop; + + for Cu of Big loop + declare + Pos : constant Positive_Count_Type := P.Get (Big, Cu); + + begin + if Pos < Cut then + if not P.Has_Key (Small, Cu) + or else Pos /= P.Get (Small, Cu) + then + return False; + end if; + + elsif Pos >= Cut + Count then + if not P.Has_Key (Small, Cu) + or else Pos /= P.Get (Small, Cu) + Count + then + return False; + end if; + + else + if P.Has_Key (Small, Cu) then + return False; + end if; + end if; + end; + end loop; + + return True; + end P_Positions_Shifted; + + --------------- + -- Positions -- + --------------- + + function Positions (Container : Map) return P.Map is + I : Count_Type := 1; + Position : Count_Type := Container.First; + R : P.Map; + + begin + -- Can't use First, Next or Element here, since they depend on models + -- for their postconditions. + + while Position /= 0 loop + R := P.Add (R, (Node => Position), I); + pragma Assert (P.Length (R) = I); + Position := Tree_Operations.Next (Container, Position); + I := I + 1; + end loop; + + return R; + end Positions; + + end Formal_Model; + ---------- -- Free -- ---------- @@ -864,47 +997,6 @@ is return (Node => Tree_Operations.Next (Container, Position.Node)); end Next; - ------------- - -- Overlap -- - ------------- - - function Overlap (Left, Right : Map) return Boolean is - begin - if Length (Left) = 0 or Length (Right) = 0 then - return False; - end if; - - declare - L_Node : Count_Type := First (Left).Node; - R_Node : Count_Type := First (Right).Node; - L_Last : constant Count_Type := Next (Left, Last (Left).Node); - R_Last : constant Count_Type := Next (Right, Last (Right).Node); - - begin - if Left'Address = Right'Address then - return True; - end if; - - loop - if L_Node = L_Last - or else R_Node = R_Last - then - return False; - end if; - - if Left.Nodes (L_Node).Key < Right.Nodes (R_Node).Key then - L_Node := Next (Left, L_Node); - - elsif Right.Nodes (R_Node).Key < Left.Nodes (L_Node).Key then - R_Node := Next (Right, R_Node); - - else - return True; - end if; - end loop; - end; - end Overlap; - ------------ -- Parent -- ------------ @@ -1042,35 +1134,4 @@ is Node.Right := Right; end Set_Right; - ------------------ - -- Strict_Equal -- - ------------------ - - function Strict_Equal (Left, Right : Map) return Boolean is - LNode : Count_Type := First (Left).Node; - RNode : Count_Type := First (Right).Node; - - begin - if Length (Left) /= Length (Right) then - return False; - end if; - - while LNode = RNode loop - if LNode = 0 then - return True; - end if; - - if Left.Nodes (LNode).Element /= Right.Nodes (RNode).Element - or else Left.Nodes (LNode).Key /= Right.Nodes (RNode).Key - then - exit; - end if; - - LNode := Next (Left, LNode); - RNode := Next (Right, RNode); - end loop; - - return False; - end Strict_Equal; - end Ada.Containers.Formal_Ordered_Maps; diff --git a/gcc/ada/a-cforma.ads b/gcc/ada/a-cforma.ads index 018a21b..7999e2e 100644 --- a/gcc/ada/a-cforma.ads +++ b/gcc/ada/a-cforma.ads @@ -6,7 +6,7 @@ -- -- -- S p e c -- -- -- --- Copyright (C) 2004-2015, Free Software Foundation, Inc. -- +-- Copyright (C) 2004-2017, Free Software Foundation, Inc. -- -- -- -- This specification is derived from the Ada Reference Manual for use with -- -- GNAT. The copyright notice above, and the license provisions that follow -- @@ -46,17 +46,11 @@ -- container. The operators "<" and ">" that could not be modified that way -- have been removed. --- There are four new functions: - --- function Strict_Equal (Left, Right : Map) return Boolean; --- function Overlap (Left, Right : Map) return Boolean; --- function First_To_Previous (Container : Map; Current : Cursor) --- return Map; --- function Current_To_Last (Container : Map; Current : Cursor) --- return Map; - --- See detailed specifications for these subprograms +-- Iteration over maps is done using the Iterable aspect, which is SPARK +-- compatible. "For of" iteration ranges over keys instead of elements. +with Ada.Containers.Functional_Vectors; +with Ada.Containers.Functional_Maps; private with Ada.Containers.Red_Black_Trees; generic @@ -64,63 +58,304 @@ generic type Element_Type is private; with function "<" (Left, Right : Key_Type) return Boolean is <>; - with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Formal_Ordered_Maps with - Pure, SPARK_Mode is - pragma Annotate (GNATprove, External_Axiomatization); pragma Annotate (CodePeer, Skip_Analysis); function Equivalent_Keys (Left, Right : Key_Type) return Boolean with - Global => null; + Global => null, + Post => + Equivalent_Keys'Result = (not (Left < Right) and not (Right < Left)); + pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Keys); type Map (Capacity : Count_Type) is private with Iterable => (First => First, Next => Next, Has_Element => Has_Element, - Element => Element), + Element => Key), Default_Initial_Condition => Is_Empty (Map); pragma Preelaborable_Initialization (Map); - type Cursor is private; - pragma Preelaborable_Initialization (Cursor); + type Cursor is record + Node : Count_Type; + end record; + + No_Element : constant Cursor := (Node => 0); Empty_Map : constant Map; - No_Element : constant Cursor; + function Length (Container : Map) return Count_Type with + Global => null, + Post => Length'Result <= Container.Capacity; + + pragma Unevaluated_Use_Of_Old (Allow); + + package Formal_Model with Ghost is + subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; + + package M is new Ada.Containers.Functional_Maps + (Element_Type => Element_Type, + Key_Type => Key_Type, + Equivalent_Keys => Equivalent_Keys); + + function "=" + (Left : M.Map; + Right : M.Map) return Boolean renames M."="; + + function "<=" + (Left : M.Map; + Right : M.Map) return Boolean renames M."<="; + + package K is new Ada.Containers.Functional_Vectors + (Element_Type => Key_Type, + Index_Type => Positive_Count_Type); + + function "=" + (Left : K.Sequence; + Right : K.Sequence) return Boolean renames K."="; + + function "<" + (Left : K.Sequence; + Right : K.Sequence) return Boolean renames K."<"; + + function "<=" + (Left : K.Sequence; + Right : K.Sequence) return Boolean renames K."<="; + + function K_Bigger_Than_Range + (Container : K.Sequence; + Fst : Positive_Count_Type; + Lst : Count_Type; + Key : Key_Type) return Boolean + with + Global => null, + Pre => Lst <= K.Length (Container), + Post => + K_Bigger_Than_Range'Result = + (for all I in Fst .. Lst => K.Get (Container, I) < Key); + pragma Annotate (GNATprove, Inline_For_Proof, K_Bigger_Than_Range); + + function K_Smaller_Than_Range + (Container : K.Sequence; + Fst : Positive_Count_Type; + Lst : Count_Type; + Key : Key_Type) return Boolean + with + Global => null, + Pre => Lst <= K.Length (Container), + Post => + K_Smaller_Than_Range'Result = + (for all I in Fst .. Lst => Key < K.Get (Container, I)); + pragma Annotate (GNATprove, Inline_For_Proof, K_Smaller_Than_Range); + + function K_Is_Find + (Container : K.Sequence; + Key : Key_Type; + Position : Count_Type) return Boolean + with + Global => null, + Pre => Position - 1 <= K.Length (Container), + Post => + K_Is_Find'Result = + + ((if Position > 0 then + K_Bigger_Than_Range (Container, 1, Position - 1, Key)) + + and (if Position < K.Length (Container) then + K_Smaller_Than_Range + (Container, + Position + 1, + K.Length (Container), + Key))); + pragma Annotate (GNATprove, Inline_For_Proof, K_Is_Find); + + package P is new Ada.Containers.Functional_Maps + (Key_Type => Cursor, + Element_Type => Positive_Count_Type, + Equivalent_Keys => "=", + Enable_Handling_Of_Equivalence => False); + + function "=" + (Left : P.Map; + Right : P.Map) return Boolean renames P."="; + + function "<=" + (Left : P.Map; + Right : P.Map) return Boolean renames P."<="; + + function P_Positions_Shifted + (Small : P.Map; + Big : P.Map; + Cut : Positive_Count_Type; + Count : Count_Type := 1) return Boolean + with + Global => null, + Post => + P_Positions_Shifted'Result = + + -- Big contains all cursors of Small + + (P.Keys_Included (Small, Big) + + -- Cursors located before Cut are not moved, cursors located + -- after are shifted by Count. + + and (for all I of Small => + (if P.Get (Small, I) < Cut then + P.Get (Big, I) = P.Get (Small, I) + else + P.Get (Big, I) - Count = P.Get (Small, I))) + + -- New cursors of Big (if any) are between Cut and Cut - 1 + + -- Count. + + and (for all I of Big => + P.Has_Key (Small, I) + or P.Get (Big, I) - Count in Cut - Count .. Cut - 1)); + + function Model (Container : Map) return M.Map with + -- The high-level model of a map is a map from keys to elements. Neither + -- cursors nor order of elements are represented in this model. Keys are + -- modeled up to equivalence. + + Ghost, + Global => null; + + function Keys (Container : Map) return K.Sequence with + -- The Keys sequence represents the underlying list structure of maps + -- that is used for iteration. It stores the actual values of keys in + -- the map. It does not model cursors nor elements. + + Ghost, + Global => null, + Post => + K.Length (Keys'Result) = Length (Container) + + -- It only contains keys contained in Model + + and (for all Key of Keys'Result => + M.Has_Key (Model (Container), Key)) + + -- It contains all the keys contained in Model + + and + (for all Key of Model (Container) => + (for some L of Keys'Result => Equivalent_Keys (L, Key))) + + -- It is sorted in increasing order + + and + (for all I in 1 .. Length (Container) => + (for all J in 1 .. Length (Container) => + (K.Get (Keys'Result, I) < K.Get (Keys'Result, J)) = + (I < J))); + pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Keys); + + function Positions (Container : Map) return P.Map with + -- The Positions map is used to model cursors. It only contains valid + -- cursors and maps them to their position in the container. + + Ghost, + Global => null, + Post => + not P.Has_Key (Positions'Result, No_Element) + + -- Positions of cursors are smaller than the container's length. + + and then + (for all I of Positions'Result => + P.Get (Positions'Result, I) in 1 .. Length (Container) + + -- No two cursors have the same position. Note that we do not + -- state that there is a cursor in the map for each position, as + -- it is rarely needed. + + and then + (for all J of Positions'Result => + (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J) + then I = J))); + + procedure Lift_Abstraction_Level (Container : Map) with + -- Lift_Abstraction_Level is a ghost procedure that does nothing but + -- assume that we can access the same elements by iterating over + -- positions or cursors. + -- This information is not generally useful except when switching from + -- a low-level, cursor-aware view of a container, to a high-level, + -- position-based view. + + Ghost, + Global => null, + Post => + (for all Key of Keys (Container) => + (for some I of Positions (Container) => + K.Get (Keys (Container), P.Get (Positions (Container), I)) = + Key)); + + function Contains + (C : M.Map; + K : Key_Type) return Boolean renames M.Has_Key; + -- To improve readability of contracts, we rename the function used to + -- search for a key in the model to Contains. + + function Element + (C : M.Map; + K : Key_Type) return Element_Type renames M.Get; + -- To improve readability of contracts, we rename the function used to + -- access an element in the model to Element. + end Formal_Model; + use Formal_Model; function "=" (Left, Right : Map) return Boolean with - Global => null; - - function Length (Container : Map) return Count_Type with - Global => null; + Global => null, + Post => "="'Result = (Model (Left) = Model (Right)); function Is_Empty (Container : Map) return Boolean with - Global => null; + Global => null, + Post => Is_Empty'Result = (Length (Container) = 0); procedure Clear (Container : in out Map) with - Global => null; + Global => null, + Post => Length (Container) = 0 and M.Is_Empty (Model (Container)); procedure Assign (Target : in out Map; Source : Map) with Global => null, - Pre => Target.Capacity >= Length (Source); + Pre => Target.Capacity >= Length (Source), + Post => + Model (Target) = Model (Source) + and Keys (Target) = Keys (Source) + and Length (Source) = Length (Target); function Copy (Source : Map; Capacity : Count_Type := 0) return Map with Global => null, - Pre => Capacity = 0 or else Capacity >= Source.Capacity; + Pre => Capacity = 0 or else Capacity >= Source.Capacity, + Post => + Model (Copy'Result) = Model (Source) + and Keys (Copy'Result) = Keys (Source) + and Positions (Copy'Result) = Positions (Source) + and (if Capacity = 0 then + Copy'Result.Capacity = Source.Capacity + else + Copy'Result.Capacity = Capacity); function Key (Container : Map; Position : Cursor) return Key_Type with Global => null, - Pre => Has_Element (Container, Position); + Pre => Has_Element (Container, Position), + Post => + Key'Result = + K.Get (Keys (Container), P.Get (Positions (Container), Position)); + pragma Annotate (GNATprove, Inline_For_Proof, Key); function Element (Container : Map; Position : Cursor) return Element_Type with Global => null, - Pre => Has_Element (Container, Position); + Pre => Has_Element (Container, Position), + Post => + Element'Result = Element (Model (Container), Key (Container, Position)); + pragma Annotate (GNATprove, Inline_For_Proof, Element); procedure Replace_Element (Container : in out Map; @@ -128,11 +363,35 @@ is New_Item : Element_Type) with Global => null, - Pre => Has_Element (Container, Position); + Pre => Has_Element (Container, Position), + Post => + + -- Order of keys and cursors is preserved + + Keys (Container) = Keys (Container)'Old + and Positions (Container) = Positions (Container)'Old + + -- New_Item is now associated with the key at position Position in + -- Container. + + and Element (Container, Position) = New_Item + + -- Elements associated with other keys are preserved + + and M.Same_Keys (Model (Container), Model (Container)'Old) + and M.Elements_Equal_Except + (Model (Container), + Model (Container)'Old, + Key (Container, Position)); procedure Move (Target : in out Map; Source : in out Map) with Global => null, - Pre => Target.Capacity >= Length (Source); + Pre => Target.Capacity >= Length (Source), + Post => + Model (Target) = Model (Source)'Old + and Keys (Target) = Keys (Source)'Old + and Length (Source)'Old = Length (Target) + and Length (Source) = 0; procedure Insert (Container : in out Map; @@ -141,8 +400,72 @@ is Position : out Cursor; Inserted : out Boolean) with - Global => null, - Pre => Length (Container) < Container.Capacity; + Global => null, + Pre => + Length (Container) < Container.Capacity or Contains (Container, Key), + Post => + Contains (Container, Key) + and Has_Element (Container, Position) + and Equivalent_Keys + (Formal_Ordered_Maps.Key (Container, Position), Key) + and K_Is_Find + (Keys (Container), + Key, + P.Get (Positions (Container), Position)), + Contract_Cases => + + -- If Key is already in Container, it is not modified and Inserted is + -- set to False. + + (Contains (Container, Key) => + not Inserted + and Model (Container) = Model (Container)'Old + and Keys (Container) = Keys (Container)'Old + and Positions (Container) = Positions (Container)'Old, + + -- Otherwise, Key is inserted in Container and Inserted is set to True + + others => + Inserted + and Length (Container) = Length (Container)'Old + 1 + + -- Key now maps to New_Item + + and Formal_Ordered_Maps.Key (Container, Position) = Key + and Element (Model (Container), Key) = New_Item + + -- Other mappings are preserved + + and Model (Container)'Old <= Model (Container) + and M.Keys_Included_Except + (Model (Container), + Model (Container)'Old, + Key) + + -- The keys of Container located before Position are preserved + + and K.Range_Equal + (Left => Keys (Container)'Old, + Right => Keys (Container), + Fst => 1, + Lst => P.Get (Positions (Container), Position) - 1) + + -- Other keys are shifted by 1 + + and K.Range_Shifted + (Left => Keys (Container)'Old, + Right => Keys (Container), + Fst => P.Get (Positions (Container), Position), + Lst => Length (Container)'Old, + Offset => 1) + + -- A new cursor has been inserted at position Position in + -- Container. + + and P_Positions_Shifted + (Positions (Container)'Old, + Positions (Container), + Cut => P.Get (Positions (Container), Position))); procedure Insert (Container : in out Map; @@ -150,16 +473,135 @@ is New_Item : Element_Type) with Global => null, - Pre => Length (Container) < Container.Capacity - and then (not Contains (Container, Key)); + Pre => + Length (Container) < Container.Capacity + and then (not Contains (Container, Key)), + Post => + Length (Container) = Length (Container)'Old + 1 + and Contains (Container, Key) + + -- Key now maps to New_Item + + and Formal_Ordered_Maps.Key (Container, Find (Container, Key)) = Key + and Element (Model (Container), Key) = New_Item + + -- Other mappings are preserved + + and Model (Container)'Old <= Model (Container) + and M.Keys_Included_Except + (Model (Container), + Model (Container)'Old, + Key) + + -- The keys of Container located before Key are preserved + + and K.Range_Equal + (Left => Keys (Container)'Old, + Right => Keys (Container), + Fst => 1, + Lst => + P.Get (Positions (Container), Find (Container, Key)) - 1) + + -- Other keys are shifted by 1 + + and K.Range_Shifted + (Left => Keys (Container)'Old, + Right => Keys (Container), + Fst => P.Get (Positions (Container), Find (Container, Key)), + Lst => Length (Container)'Old, + Offset => 1) + + -- A new cursor has been inserted in Container + + and P_Positions_Shifted + (Positions (Container)'Old, + Positions (Container), + Cut => P.Get (Positions (Container), Find (Container, Key))); procedure Include (Container : in out Map; Key : Key_Type; New_Item : Element_Type) with - Global => null, - Pre => Length (Container) < Container.Capacity; + Global => null, + Pre => + Length (Container) < Container.Capacity or Contains (Container, Key), + Post => + Contains (Container, Key) and Element (Container, Key) = New_Item, + Contract_Cases => + + -- If Key is already in Container, Key is mapped to New_Item + + (Contains (Container, Key) => + + -- Cursors are preserved + + Positions (Container) = Positions (Container)'Old + + -- The key equivalent to Key in Container is replaced by Key + + and K.Get + (Keys (Container), + P.Get (Positions (Container), Find (Container, Key))) = Key + + and K.Equal_Except + (Keys (Container)'Old, + Keys (Container), + P.Get (Positions (Container), Find (Container, Key))) + + -- Elements associated with other keys are preserved + + and M.Same_Keys (Model (Container), Model (Container)'Old) + and M.Elements_Equal_Except + (Model (Container), + Model (Container)'Old, + Key), + + -- Otherwise, Key is inserted in Container + + others => + Length (Container) = Length (Container)'Old + 1 + + -- Other mappings are preserved + + and Model (Container)'Old <= Model (Container) + and M.Keys_Included_Except + (Model (Container), + Model (Container)'Old, + Key) + + -- Key is inserted in Container + + and K.Get + (Keys (Container), + P.Get (Positions (Container), Find (Container, Key))) = Key + + -- The keys of Container located before Key are preserved + + and K.Range_Equal + (Left => Keys (Container)'Old, + Right => Keys (Container), + Fst => 1, + Lst => + P.Get (Positions (Container), Find (Container, Key)) - 1) + + -- Other keys are shifted by 1 + + and K.Range_Shifted + (Left => Keys (Container)'Old, + Right => Keys (Container), + Fst => + P.Get (Positions (Container), Find (Container, Key)), + Lst => Length (Container)'Old, + Offset => 1) + + -- A new cursor has been inserted in Container + + and P_Positions_Shifted + (Positions (Container)'Old, + Positions (Container), + Cut => + P.Get (Positions (Container), Find (Container, Key)))); procedure Replace (Container : in out Map; @@ -167,112 +609,427 @@ is New_Item : Element_Type) with Global => null, - Pre => Contains (Container, Key); + Pre => Contains (Container, Key), + Post => + + -- Cursors are preserved + + Positions (Container) = Positions (Container)'Old + + -- The key equivalent to Key in Container is replaced by Key + + and K.Get (Keys (Container), + P.Get (Positions (Container), Find (Container, Key))) = Key + and K.Equal_Except + (Keys (Container)'Old, + Keys (Container), + P.Get (Positions (Container), Find (Container, Key))) + + -- New_Item is now associated with the Key in Container + + and Element (Model (Container), Key) = New_Item + + -- Elements associated with other keys are preserved + + and M.Same_Keys (Model (Container), Model (Container)'Old) + and M.Elements_Equal_Except + (Model (Container), + Model (Container)'Old, + Key); procedure Exclude (Container : in out Map; Key : Key_Type) with - Global => null; + Global => null, + Post => not Contains (Container, Key), + Contract_Cases => + + -- If Key is not in Container, nothing is changed + + (not Contains (Container, Key) => + Model (Container) = Model (Container)'Old + and Keys (Container) = Keys (Container)'Old + and Positions (Container) = Positions (Container)'Old, + + -- Otherwise, Key is removed from Container + + others => + Length (Container) = Length (Container)'Old - 1 + + -- Other mappings are preserved + + and Model (Container) <= Model (Container)'Old + and M.Keys_Included_Except + (Model (Container)'Old, + Model (Container), + Key) + + -- The keys of Container located before Key are preserved + + and K.Range_Equal + (Left => Keys (Container)'Old, + Right => Keys (Container), + Fst => 1, + Lst => + P.Get (Positions (Container), Find (Container, Key))'Old + - 1) + + -- The keys located after Key are shifted by 1 + + and K.Range_Shifted + (Left => Keys (Container), + Right => Keys (Container)'Old, + Fst => + P.Get (Positions (Container), Find (Container, Key))'Old, + Lst => Length (Container), + Offset => 1) + + -- A cursor has been removed from Container + + and P_Positions_Shifted + (Positions (Container), + Positions (Container)'Old, + Cut => + P.Get + (Positions (Container), Find (Container, Key))'Old)); procedure Delete (Container : in out Map; Key : Key_Type) with Global => null, - Pre => Contains (Container, Key); + Pre => Contains (Container, Key), + Post => + Length (Container) = Length (Container)'Old - 1 + + -- Key is no longer in Container + + and not Contains (Container, Key) + + -- Other mappings are preserved + + and Model (Container) <= Model (Container)'Old + and M.Keys_Included_Except + (Model (Container)'Old, + Model (Container), + Key) + + -- The keys of Container located before Key are preserved + + and K.Range_Equal + (Left => Keys (Container)'Old, + Right => Keys (Container), + Fst => 1, + Lst => + P.Get (Positions (Container), Find (Container, Key))'Old - 1) + + -- The keys located after Key are shifted by 1 + + and K.Range_Shifted + (Left => Keys (Container), + Right => Keys (Container)'Old, + Fst => + P.Get (Positions (Container), Find (Container, Key))'Old, + Lst => Length (Container), + Offset => 1) + + -- A cursor has been removed from Container + + and P_Positions_Shifted + (Positions (Container), + Positions (Container)'Old, + Cut => + P.Get (Positions (Container), Find (Container, Key))'Old); procedure Delete (Container : in out Map; Position : in out Cursor) with Global => null, - Pre => Has_Element (Container, Position); + Pre => Has_Element (Container, Position), + Post => + Position = No_Element + and Length (Container) = Length (Container)'Old - 1 + + -- The key at position Position is no longer in Container + + and not Contains (Container, Key (Container, Position)'Old) + and not P.Has_Key (Positions (Container), Position'Old) + + -- Other mappings are preserved + + and Model (Container) <= Model (Container)'Old + and M.Keys_Included_Except + (Model (Container)'Old, + Model (Container), + Key (Container, Position)'Old) + + -- The keys of Container located before Position are preserved. + + and K.Range_Equal + (Left => Keys (Container)'Old, + Right => Keys (Container), + Fst => 1, + Lst => P.Get (Positions (Container)'Old, Position'Old) - 1) + + -- The keys located after Position are shifted by 1 + + and K.Range_Shifted + (Left => Keys (Container), + Right => Keys (Container)'Old, + Fst => P.Get (Positions (Container)'Old, Position'Old), + Lst => Length (Container), + Offset => 1) + + -- Position has been removed from Container + + and P_Positions_Shifted + (Positions (Container), + Positions (Container)'Old, + Cut => P.Get (Positions (Container)'Old, Position'Old)); procedure Delete_First (Container : in out Map) with - Global => null; + Global => null, + Contract_Cases => + (Length (Container) = 0 => Length (Container) = 0, + others => + Length (Container) = Length (Container)'Old - 1 + + -- The first key has been removed from Container + + and not Contains (Container, First_Key (Container)'Old) + + -- Other mappings are preserved + + and Model (Container) <= Model (Container)'Old + and M.Keys_Included_Except + (Model (Container)'Old, + Model (Container), + First_Key (Container)'Old) + + -- Other keys are shifted by 1 + + and K.Range_Shifted + (Left => Keys (Container), + Right => Keys (Container)'Old, + Fst => 1, + Lst => Length (Container), + Offset => 1) + + -- First has been removed from Container + + and P_Positions_Shifted + (Positions (Container), + Positions (Container)'Old, + Cut => 1)); procedure Delete_Last (Container : in out Map) with - Global => null; + Global => null, + Contract_Cases => + (Length (Container) = 0 => Length (Container) = 0, + others => + Length (Container) = Length (Container)'Old - 1 + + -- The last key has been removed from Container + + and not Contains (Container, Last_Key (Container)'Old) + + -- Other mappings are preserved + + and Model (Container) <= Model (Container)'Old + and M.Keys_Included_Except + (Model (Container)'Old, + Model (Container), + Last_Key (Container)'Old) + + -- Others keys of Container are preserved + + and K.Range_Equal + (Left => Keys (Container)'Old, + Right => Keys (Container), + Fst => 1, + Lst => Length (Container)) + + -- Last cursor has been removed from Container + + and Positions (Container) <= Positions (Container)'Old); function First (Container : Map) return Cursor with - Global => null; + Global => null, + Contract_Cases => + (Length (Container) = 0 => + First'Result = No_Element, + + others => + Has_Element (Container, First'Result) + and P.Get (Positions (Container), First'Result) = 1); function First_Element (Container : Map) return Element_Type with Global => null, - Pre => not Is_Empty (Container); + Pre => not Is_Empty (Container), + Post => + First_Element'Result = + Element (Model (Container), First_Key (Container)); function First_Key (Container : Map) return Key_Type with Global => null, - Pre => not Is_Empty (Container); + Pre => not Is_Empty (Container), + Post => + First_Key'Result = K.Get (Keys (Container), 1) + and K_Smaller_Than_Range + (Keys (Container), 2, Length (Container), First_Key'Result); function Last (Container : Map) return Cursor with - Global => null; + Global => null, + Contract_Cases => + (Length (Container) = 0 => + Last'Result = No_Element, + + others => + Has_Element (Container, Last'Result) + and P.Get (Positions (Container), Last'Result) = + Length (Container)); function Last_Element (Container : Map) return Element_Type with Global => null, - Pre => not Is_Empty (Container); + Pre => not Is_Empty (Container), + Post => + Last_Element'Result = Element (Model (Container), Last_Key (Container)); function Last_Key (Container : Map) return Key_Type with Global => null, - Pre => not Is_Empty (Container); + Pre => not Is_Empty (Container), + Post => + Last_Key'Result = K.Get (Keys (Container), Length (Container)) + and K_Bigger_Than_Range + (Keys (Container), 1, Length (Container) - 1, Last_Key'Result); function Next (Container : Map; Position : Cursor) return Cursor with - Global => null, - Pre => Has_Element (Container, Position) or else Position = No_Element; + Global => null, + Pre => + Has_Element (Container, Position) or else Position = No_Element, + Contract_Cases => + (Position = No_Element + or else P.Get (Positions (Container), Position) = Length (Container) + => + Next'Result = No_Element, + + others => + Has_Element (Container, Next'Result) + and then P.Get (Positions (Container), Next'Result) = + P.Get (Positions (Container), Position) + 1); procedure Next (Container : Map; Position : in out Cursor) with - Global => null, - Pre => Has_Element (Container, Position) or else Position = No_Element; + Global => null, + Pre => + Has_Element (Container, Position) or else Position = No_Element, + Contract_Cases => + (Position = No_Element + or else P.Get (Positions (Container), Position) = Length (Container) + => + Position = No_Element, + + others => + Has_Element (Container, Position) + and then P.Get (Positions (Container), Position) = + P.Get (Positions (Container), Position'Old) + 1); function Previous (Container : Map; Position : Cursor) return Cursor with - Global => null, - Pre => Has_Element (Container, Position) or else Position = No_Element; + Global => null, + Pre => + Has_Element (Container, Position) or else Position = No_Element, + Contract_Cases => + (Position = No_Element + or else P.Get (Positions (Container), Position) = 1 + => + Previous'Result = No_Element, + + others => + Has_Element (Container, Previous'Result) + and then P.Get (Positions (Container), Previous'Result) = + P.Get (Positions (Container), Position) - 1); procedure Previous (Container : Map; Position : in out Cursor) with - Global => null, - Pre => Has_Element (Container, Position) or else Position = No_Element; + Global => null, + Pre => + Has_Element (Container, Position) or else Position = No_Element, + Contract_Cases => + (Position = No_Element + or else P.Get (Positions (Container), Position) = 1 + => + Position = No_Element, + + others => + Has_Element (Container, Position) + and then P.Get (Positions (Container), Position) = + P.Get (Positions (Container), Position'Old) - 1); function Find (Container : Map; Key : Key_Type) return Cursor with - Global => null; + Global => null, + Contract_Cases => + + -- If Key is not is not contained in Container, Find returns No_Element + + (not Contains (Model (Container), Key) => + not P.Has_Key (Positions (Container), Find'Result) + and Find'Result = No_Element, + + -- Otherwise, Find returns a valid cusror in Container + + others => + P.Has_Key (Positions (Container), Find'Result) + + -- The key designated by the result of Find is Key + + and Equivalent_Keys + (Formal_Ordered_Maps.Key (Container, Find'Result), Key) + + -- Keys of Container are ordered + + and K_Is_Find + (Keys (Container), + Key, + P.Get (Positions (Container), + Find'Result))); function Element (Container : Map; Key : Key_Type) return Element_Type with Global => null, - Pre => Contains (Container, Key); + Pre => Contains (Container, Key), + Post => Element'Result = Element (Model (Container), Key); + pragma Annotate (GNATprove, Inline_For_Proof, Element); function Floor (Container : Map; Key : Key_Type) return Cursor with - Global => null; + Global => null, + Contract_Cases => + (Length (Container) = 0 or else Key < First_Key (Container) => + Floor'Result = No_Element, + others => + Has_Element (Container, Floor'Result) + and not (Key < K.Get (Keys (Container), + P.Get (Positions (Container), Floor'Result))) + and K_Is_Find + (Keys (Container), + Key, + P.Get (Positions (Container), Floor'Result))); function Ceiling (Container : Map; Key : Key_Type) return Cursor with - Global => null; + Global => null, + Contract_Cases => + (Length (Container) = 0 or else Last_Key (Container) < Key => + Ceiling'Result = No_Element, + others => + Has_Element (Container, Ceiling'Result) + and + not (K.Get (Keys (Container), + P.Get (Positions (Container), Ceiling'Result)) < Key) + and K_Is_Find + (Keys (Container), + Key, + P.Get (Positions (Container), Ceiling'Result))); function Contains (Container : Map; Key : Key_Type) return Boolean with - Global => null; - - function Has_Element (Container : Map; Position : Cursor) return Boolean - with - Global => null; - - function Strict_Equal (Left, Right : Map) return Boolean with - Ghost, - Global => null; - -- Strict_Equal returns True if the containers are physically equal, i.e. - -- they are structurally equal (function "=" returns True) and that they - -- have the same set of cursors. - - function First_To_Previous (Container : Map; Current : Cursor) return Map - with - Ghost, Global => null, - Pre => Has_Element (Container, Current) or else Current = No_Element; + Post => Contains'Result = Contains (Model (Container), Key); + pragma Annotate (GNATprove, Inline_For_Proof, Contains); - function Current_To_Last (Container : Map; Current : Cursor) return Map + function Has_Element (Container : Map; Position : Cursor) return Boolean with - Ghost, Global => null, - Pre => Has_Element (Container, Current) or else Current = No_Element; - -- First_To_Previous returns a container containing all elements preceding - -- Current (excluded) in Container. Current_To_Last returns a container - -- containing all elements following Current (included) in Container. - -- These two new functions can be used to express invariant properties in - -- loops which iterate over containers. First_To_Previous returns the part - -- of the container already scanned and Current_To_Last the part not - -- scanned yet. - - function Overlap (Left, Right : Map) return Boolean with - Global => null; - -- Overlap returns True if the containers have common keys + Post => + Has_Element'Result = P.Has_Key (Positions (Container), Position); + pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); private pragma SPARK_Mode (Off); @@ -300,12 +1057,6 @@ private type Map (Capacity : Count_Type) is new Tree_Types.Tree_Type (Capacity) with null record; - type Cursor is record - Node : Node_Access; - end record; - Empty_Map : constant Map := (Capacity => 0, others => <>); - No_Element : constant Cursor := (Node => 0); - end Ada.Containers.Formal_Ordered_Maps; diff --git a/gcc/ada/a-cofuma.adb b/gcc/ada/a-cofuma.adb index 2e30089..487aff4 100644 --- a/gcc/ada/a-cofuma.adb +++ b/gcc/ada/a-cofuma.adb @@ -148,6 +148,13 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is return Find (Container.Keys, Key) > 0; end Has_Key; + ----------------- + -- Has_Witness -- + ----------------- + + function Has_Witness (Container : Map; Witness : Count_Type) return Boolean + is (Witness in 1 .. Length (Container.Keys)); + -------------- -- Is_Empty -- -------------- @@ -233,16 +240,6 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is return Length (Container.Elements); end Length; - -------------------------- - -- Lift_Equivalent_Keys -- - -------------------------- - - procedure Lift_Equivalent_Keys - (Container : Map; - Left : Key_Type; - Right : Key_Type) - is null; - --------------- -- Same_Keys -- --------------- @@ -264,4 +261,19 @@ package body Ada.Containers.Functional_Maps with SPARK_Mode => Off is Elements => Set (Container.Elements, Find (Container.Keys, Key), New_Item)); + ----------- + -- W_Get -- + ----------- + + function W_Get (Container : Map; Witness : Count_Type) return Element_Type + is + (Get (Container.Elements, Witness)); + + ------------- + -- Witness -- + ------------- + + function Witness (Container : Map; Key : Key_Type) return Count_Type is + (Find (Container.Keys, Key)); + end Ada.Containers.Functional_Maps; diff --git a/gcc/ada/a-cofuma.ads b/gcc/ada/a-cofuma.ads index 2d8a204..2b167b2 100644 --- a/gcc/ada/a-cofuma.ads +++ b/gcc/ada/a-cofuma.ads @@ -36,6 +36,10 @@ generic type Key_Type (<>) is private; type Element_Type (<>) is private; with function Equivalent_Keys (Left, Right : Key_Type) return Boolean; + Enable_Handling_Of_Equivalence : Boolean := True; + -- This constant should only be set to False when no particular handling + -- of equivalence over keys is needed, that is, Equivalent_Keys defines a + -- key uniquely. package Ada.Containers.Functional_Maps with SPARK_Mode is @@ -57,38 +61,40 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is ----------------------- -- Maps are axiomatized using Has_Key and Get, encoding respectively the - -- presence of a key in a map and an accessor to elements associated to its - -- keys. The length of a map is also added to protect Add against overflows - -- but it is not actually modeled. + -- presence of a key in a map and an accessor to elements associated with + -- its keys. The length of a map is also added to protect Add against + -- overflows but it is not actually modeled. function Has_Key (Container : Map; Key : Key_Type) return Boolean with - Global => null; -- Return True if Key is present in Container - function Get (Container : Map; Key : Key_Type) return Element_Type with Global => null, - Pre => Has_Key (Container, Key); - -- Return the element associated to Key is present in Container + Post => + (if Enable_Handling_Of_Equivalence then - function Length (Container : Map) return Count_Type with - Global => null; - -- Return the number of mappings in Container + -- Has_Key returns the same result on all equivalent keys - procedure Lift_Equivalent_Keys - (Container : Map; - Left : Key_Type; - Right : Key_Type) - -- Lemma function which can be called manually to allow GNATprove to deduce - -- that Has_Key and Get always return the same result on equivalent keys. + (if (for some K of Container => Equivalent_Keys (K, Key)) then + Has_Key'Result)); + + function Get (Container : Map; Key : Key_Type) return Element_Type with + -- Return the element associated with Key in Container - with - Ghost, Global => null, - Pre => Equivalent_Keys (Left, Right), + Pre => Has_Key (Container, Key), Post => - Has_Key (Container, Left) = Has_Key (Container, Right) - and (if Has_Key (Container, Left) then - Get (Container, Left) = Get (Container, Right)); + (if Enable_Handling_Of_Equivalence then + + -- Get returns the same result on all equivalent keys + + Get'Result = W_Get (Container, Witness (Container, Key)) + and (for all K of Container => + (if Equivalent_Keys (K, Key) then + Witness (Container, Key) = Witness (Container, K)))); + + function Length (Container : Map) return Count_Type with + Global => null; + -- Return the number of mappings in Container ------------------------ -- Property Functions -- @@ -236,8 +242,8 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is (Container : Map; Key : Key_Type; New_Item : Element_Type) return Map - -- Returns Container, where the element associated to Key has been replaced - -- by New_Item. + -- Returns Container, where the element associated with Key has been + -- replaced by New_Item. with Global => null, @@ -248,6 +254,35 @@ package Ada.Containers.Functional_Maps with SPARK_Mode is and Same_Keys (Container, Set'Result) and Elements_Equal_Except (Container, Set'Result, Key); + ------------------------------ + -- Handling of Equivalence -- + ------------------------------ + + -- These functions are used to specify that Get returns the same value on + -- equivalent keys. They should not be used directly in user code. + + function Has_Witness (Container : Map; Witness : Count_Type) return Boolean + with + Ghost, + Global => null; + -- Returns True if there is a key with witness Witness in Container + + function Witness (Container : Map; Key : Key_Type) return Count_Type with + -- Returns the witness of Key in Container + + Ghost, + Global => null, + Pre => Has_Key (Container, Key), + Post => Has_Witness (Container, Witness'Result); + + function W_Get (Container : Map; Witness : Count_Type) return Element_Type + with + -- Returns the element associated with a witness in Container + + Ghost, + Global => null, + Pre => Has_Witness (Container, Witness); + --------------------------- -- Iteration Primitives -- --------------------------- diff --git a/gcc/ada/a-cofuse.ads b/gcc/ada/a-cofuse.ads index 16a4a4d..0a998f3 100644 --- a/gcc/ada/a-cofuse.ads +++ b/gcc/ada/a-cofuse.ads @@ -37,6 +37,10 @@ generic with function Equivalent_Elements (Left : Element_Type; Right : Element_Type) return Boolean; + Enable_Handling_Of_Equivalence : Boolean := True; + -- This constant should only be set to False when no particular handling + -- of equivalence over elements is needed, that is, Equivalent_Elements + -- defines an element uniquely. package Ada.Containers.Functional_Sets with SPARK_Mode is @@ -49,6 +53,9 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is -- Sets are empty when default initialized. -- "For in" quantification over sets should not be used. -- "For of" quantification over sets iterates over elements. + -- Note that, for proof, "for of" quantification is understood modulo + -- equivalence (quantification includes elements equivalent to elements of + -- the map). ----------------------- -- Basic operations -- @@ -59,9 +66,17 @@ package Ada.Containers.Functional_Sets with SPARK_Mode is -- against overflows but it is not actually modeled. function Contains (Container : Set; Item : Element_Type) return Boolean with - Global => null; -- Return True if Item is contained in Container + Global => null, + Post => + (if Enable_Handling_Of_Equivalence then + + -- Contains returns the same result on all equivalent elements + + (if (for some E of Container => Equivalent_Elements (E, Item)) then + Contains'Result)); + function Length (Container : Set) return Count_Type with Global => null; -- Return the number of elements in Container -- 2.7.4