Mercurial > hg > CbC > CbC_gcc
diff gcc/ada/libgnat/a-cforse.ads @ 111:04ced10e8804
gcc 7
| author | kono |
|---|---|
| date | Fri, 27 Oct 2017 22:46:09 +0900 |
| parents | |
| children | 84e7813d76e9 |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/gcc/ada/libgnat/a-cforse.ads Fri Oct 27 22:46:09 2017 +0900 @@ -0,0 +1,1784 @@ +------------------------------------------------------------------------------ +-- -- +-- GNAT LIBRARY COMPONENTS -- +-- -- +-- A D A . C O N T A I N E R S . F O R M A L _ O R D E R E D _ S E T S -- +-- -- +-- S p e c -- +-- -- +-- 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 -- +-- apply solely to the contents of the part following the private keyword. -- +-- -- +-- 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/>. -- +------------------------------------------------------------------------------ + +-- This spec is derived from package Ada.Containers.Bounded_Ordered_Sets in +-- the Ada 2012 RM. The modifications are meant to facilitate formal proofs by +-- making it easier to express properties, and by making the specification of +-- this unit compatible with SPARK 2014. Note that the API of this unit may be +-- subject to incompatible changes as SPARK 2014 evolves. + +-- The modifications are: + +-- A parameter for the container is added to every function reading the +-- content of a container: Key, Element, Next, Query_Element, Previous, +-- Has_Element, Iterate, Reverse_Iterate. This change is motivated by the +-- need to have cursors which are valid on different containers (typically +-- a container C and its previous version C'Old) for expressing properties, +-- which is not possible if cursors encapsulate an access to the underlying +-- container. The operators "<" and ">" that could not be modified that way +-- have been removed. + +with Ada.Containers.Functional_Maps; +with Ada.Containers.Functional_Sets; +with Ada.Containers.Functional_Vectors; +private with Ada.Containers.Red_Black_Trees; + +generic + type Element_Type is private; + + with function "<" (Left, Right : Element_Type) return Boolean is <>; + +package Ada.Containers.Formal_Ordered_Sets with + SPARK_Mode +is + pragma Annotate (CodePeer, Skip_Analysis); + + function Equivalent_Elements (Left, Right : Element_Type) return Boolean + with + Global => null, + Post => + Equivalent_Elements'Result = + (not (Left < Right) and not (Right < Left)); + pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Elements); + + type Set (Capacity : Count_Type) is private with + Iterable => (First => First, + Next => Next, + Has_Element => Has_Element, + Element => Element), + Default_Initial_Condition => Is_Empty (Set); + pragma Preelaborable_Initialization (Set); + + type Cursor is record + Node : Count_Type; + end record; + + No_Element : constant Cursor := (Node => 0); + + function Length (Container : Set) 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_Sets + (Element_Type => Element_Type, + Equivalent_Elements => Equivalent_Elements); + + function "=" + (Left : M.Set; + Right : M.Set) return Boolean renames M."="; + + function "<=" + (Left : M.Set; + Right : M.Set) return Boolean renames M."<="; + + package E is new Ada.Containers.Functional_Vectors + (Element_Type => Element_Type, + Index_Type => Positive_Count_Type); + + function "=" + (Left : E.Sequence; + Right : E.Sequence) return Boolean renames E."="; + + function "<" + (Left : E.Sequence; + Right : E.Sequence) return Boolean renames E."<"; + + function "<=" + (Left : E.Sequence; + Right : E.Sequence) return Boolean renames E."<="; + + function E_Bigger_Than_Range + (Container : E.Sequence; + Fst : Positive_Count_Type; + Lst : Count_Type; + Item : Element_Type) return Boolean + with + Global => null, + Pre => Lst <= E.Length (Container), + Post => + E_Bigger_Than_Range'Result = + (for all I in Fst .. Lst => E.Get (Container, I) < Item); + pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range); + + function E_Smaller_Than_Range + (Container : E.Sequence; + Fst : Positive_Count_Type; + Lst : Count_Type; + Item : Element_Type) return Boolean + with + Global => null, + Pre => Lst <= E.Length (Container), + Post => + E_Smaller_Than_Range'Result = + (for all I in Fst .. Lst => Item < E.Get (Container, I)); + pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range); + + function E_Is_Find + (Container : E.Sequence; + Item : Element_Type; + Position : Count_Type) return Boolean + with + Global => null, + Pre => Position - 1 <= E.Length (Container), + Post => + E_Is_Find'Result = + + ((if Position > 0 then + E_Bigger_Than_Range (Container, 1, Position - 1, Item)) + + and (if Position < E.Length (Container) then + E_Smaller_Than_Range + (Container, + Position + 1, + E.Length (Container), + Item))); + pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find); + + function Find + (Container : E.Sequence; + Item : Element_Type) return Count_Type + -- Search for Item in Container + + with + Global => null, + Post => + (if Find'Result > 0 then + Find'Result <= E.Length (Container) + and Equivalent_Elements (Item, E.Get (Container, Find'Result))); + + function E_Elements_Included + (Left : E.Sequence; + Right : E.Sequence) return Boolean + -- The elements of Left are contained in Right + + with + Global => null, + Post => + E_Elements_Included'Result = + (for all I in 1 .. E.Length (Left) => + Find (Right, E.Get (Left, I)) > 0 + and then E.Get (Right, Find (Right, E.Get (Left, I))) = + E.Get (Left, I)); + pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); + + function E_Elements_Included + (Left : E.Sequence; + Model : M.Set; + Right : E.Sequence) return Boolean + -- The elements of Container contained in Model are in Right + + with + Global => null, + Post => + E_Elements_Included'Result = + (for all I in 1 .. E.Length (Left) => + (if M.Contains (Model, E.Get (Left, I)) then + Find (Right, E.Get (Left, I)) > 0 + and then E.Get (Right, Find (Right, E.Get (Left, I))) = + E.Get (Left, I))); + pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); + + function E_Elements_Included + (Container : E.Sequence; + Model : M.Set; + Left : E.Sequence; + Right : E.Sequence) return Boolean + -- The elements of Container contained in Model are in Left and others + -- are in Right. + + with + Global => null, + Post => + E_Elements_Included'Result = + (for all I in 1 .. E.Length (Container) => + (if M.Contains (Model, E.Get (Container, I)) then + Find (Left, E.Get (Container, I)) > 0 + and then E.Get (Left, Find (Left, E.Get (Container, I))) = + E.Get (Container, I) + else + Find (Right, E.Get (Container, I)) > 0 + and then E.Get (Right, Find (Right, E.Get (Container, I))) = + E.Get (Container, I))); + pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included); + + 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 Mapping_Preserved + (E_Left : E.Sequence; + E_Right : E.Sequence; + P_Left : P.Map; + P_Right : P.Map) return Boolean + with + Ghost, + Global => null, + Post => + (if Mapping_Preserved'Result then + + -- Right contains all the cursors of Left + + P.Keys_Included (P_Left, P_Right) + + -- Right contains all the elements of Left + + and E_Elements_Included (E_Left, E_Right) + + -- Mappings from cursors to elements induced by E_Left, P_Left + -- and E_Right, P_Right are the same. + + and (for all C of P_Left => + E.Get (E_Left, P.Get (P_Left, C)) = + E.Get (E_Right, P.Get (P_Right, C)))); + + function Mapping_Preserved_Except + (E_Left : E.Sequence; + E_Right : E.Sequence; + P_Left : P.Map; + P_Right : P.Map; + Position : Cursor) return Boolean + with + Ghost, + Global => null, + Post => + (if Mapping_Preserved_Except'Result then + + -- Right contains all the cursors of Left + + P.Keys_Included (P_Left, P_Right) + + -- Mappings from cursors to elements induced by E_Left, P_Left + -- and E_Right, P_Right are the same except for Position. + + and (for all C of P_Left => + (if C /= Position then + E.Get (E_Left, P.Get (P_Left, C)) = + E.Get (E_Right, P.Get (P_Right, C))))); + + function Model (Container : Set) return M.Set with + -- The high-level model of a set is a set of elements. Neither cursors + -- nor order of elements are represented in this model. Elements are + -- modeled up to equivalence. + + Ghost, + Global => null, + Post => M.Length (Model'Result) = Length (Container); + + function Elements (Container : Set) return E.Sequence with + -- The Elements sequence represents the underlying list structure of + -- sets that is used for iteration. It stores the actual values of + -- elements in the set. It does not model cursors. + + Ghost, + Global => null, + Post => + E.Length (Elements'Result) = Length (Container) + + -- It only contains keys contained in Model + + and (for all Item of Elements'Result => + M.Contains (Model (Container), Item)) + + -- It contains all the elements contained in Model + + and (for all Item of Model (Container) => + (Find (Elements'Result, Item) > 0 + and then Equivalent_Elements + (E.Get (Elements'Result, Find (Elements'Result, Item)), + Item))) + + -- It is sorted in increasing order + + and (for all I in 1 .. Length (Container) => + Find (Elements'Result, E.Get (Elements'Result, I)) = I + and + E_Is_Find + (Elements'Result, E.Get (Elements'Result, I), I)); + pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Elements); + + function Positions (Container : Set) 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 : Set) 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 Item of Elements (Container) => + (for some I of Positions (Container) => + E.Get (Elements (Container), P.Get (Positions (Container), I)) = + Item)); + + function Contains + (C : M.Set; + K : Element_Type) return Boolean renames M.Contains; + -- To improve readability of contracts, we rename the function used to + -- search for an element in the model to Contains. + + end Formal_Model; + use Formal_Model; + + Empty_Set : constant Set; + + function "=" (Left, Right : Set) return Boolean with + Global => null, + Post => + + -- If two sets are equal, they contain the same elements in the same + -- order. + + (if "="'Result then Elements (Left) = Elements (Right) + + -- If they are different, then they do not contain the same elements + + else + not E_Elements_Included (Elements (Left), Elements (Right)) + or not E_Elements_Included (Elements (Right), Elements (Left))); + + function Equivalent_Sets (Left, Right : Set) return Boolean with + Global => null, + Post => Equivalent_Sets'Result = (Model (Left) = Model (Right)); + + function To_Set (New_Item : Element_Type) return Set with + Global => null, + Post => + M.Is_Singleton (Model (To_Set'Result), New_Item) + and Length (To_Set'Result) = 1 + and E.Get (Elements (To_Set'Result), 1) = New_Item; + + function Is_Empty (Container : Set) return Boolean with + Global => null, + Post => Is_Empty'Result = (Length (Container) = 0); + + procedure Clear (Container : in out Set) with + Global => null, + Post => Length (Container) = 0 and M.Is_Empty (Model (Container)); + + procedure Assign (Target : in out Set; Source : Set) with + Global => null, + Pre => Target.Capacity >= Length (Source), + Post => + Model (Target) = Model (Source) + and Elements (Target) = Elements (Source) + and Length (Target) = Length (Source); + + function Copy (Source : Set; Capacity : Count_Type := 0) return Set with + Global => null, + Pre => Capacity = 0 or else Capacity >= Source.Capacity, + Post => + Model (Copy'Result) = Model (Source) + and Elements (Copy'Result) = Elements (Source) + and Positions (Copy'Result) = Positions (Source) + and (if Capacity = 0 then + Copy'Result.Capacity = Source.Capacity + else + Copy'Result.Capacity = Capacity); + + function Element + (Container : Set; + Position : Cursor) return Element_Type + with + Global => null, + Pre => Has_Element (Container, Position), + Post => + Element'Result = + E.Get (Elements (Container), P.Get (Positions (Container), Position)); + pragma Annotate (GNATprove, Inline_For_Proof, Element); + + procedure Replace_Element + (Container : in out Set; + Position : Cursor; + New_Item : Element_Type) + with + Global => null, + Pre => Has_Element (Container, Position), + Post => + Length (Container) = Length (Container)'Old + + -- Position now maps to New_Item + + and Element (Container, Position) = New_Item + + -- New_Item is contained in Container + + and Contains (Model (Container), New_Item) + + -- Other elements are preserved + + and M.Included_Except + (Model (Container)'Old, + Model (Container), + Element (Container, Position)'Old) + and M.Included_Except + (Model (Container), + Model (Container)'Old, + New_Item) + + -- Mapping from cursors to elements is preserved + + and Mapping_Preserved_Except + (E_Left => Elements (Container)'Old, + E_Right => Elements (Container), + P_Left => Positions (Container)'Old, + P_Right => Positions (Container), + Position => Position) + and Positions (Container) = Positions (Container)'Old; + + procedure Move (Target : in out Set; Source : in out Set) with + Global => null, + Pre => Target.Capacity >= Length (Source), + Post => + Model (Target) = Model (Source)'Old + and Elements (Target) = Elements (Source)'Old + and Length (Source)'Old = Length (Target) + and Length (Source) = 0; + + procedure Insert + (Container : in out Set; + New_Item : Element_Type; + Position : out Cursor; + Inserted : out Boolean) + with + Global => null, + Pre => + Length (Container) < Container.Capacity + or Contains (Container, New_Item), + Post => + Contains (Container, New_Item) + and Has_Element (Container, Position) + and Equivalent_Elements (Element (Container, Position), New_Item) + and E_Is_Find + (Elements (Container), + New_Item, + P.Get (Positions (Container), Position)), + Contract_Cases => + + -- If New_Item is already in Container, it is not modified and Inserted + -- is set to False. + + (Contains (Container, New_Item) => + not Inserted + and Model (Container) = Model (Container)'Old + and Elements (Container) = Elements (Container)'Old + and Positions (Container) = Positions (Container)'Old, + + -- Otherwise, New_Item is inserted in Container and Inserted is set to + -- True + + others => + Inserted + and Length (Container) = Length (Container)'Old + 1 + + -- Position now maps to New_Item + + and Element (Container, Position) = New_Item + + -- Other elements are preserved + + and Model (Container)'Old <= Model (Container) + and M.Included_Except + (Model (Container), + Model (Container)'Old, + New_Item) + + -- The elements of Container located before Position are preserved + + and E.Range_Equal + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => 1, + Lst => P.Get (Positions (Container), Position) - 1) + + -- Other elements are shifted by 1 + + and E.Range_Shifted + (Left => Elements (Container)'Old, + Right => Elements (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 Set; + New_Item : Element_Type) + with + Global => null, + Pre => + Length (Container) < Container.Capacity + and then (not Contains (Container, New_Item)), + Post => + Length (Container) = Length (Container)'Old + 1 + and Contains (Container, New_Item) + + -- New_Item is inserted in the set + + and E.Get (Elements (Container), + Find (Elements (Container), New_Item)) = New_Item + + -- Other mappings are preserved + + and Model (Container)'Old <= Model (Container) + and M.Included_Except + (Model (Container), + Model (Container)'Old, + New_Item) + + -- The elements of Container located before New_Item are preserved + + and E.Range_Equal + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => 1, + Lst => Find (Elements (Container), New_Item) - 1) + + -- Other elements are shifted by 1 + + and E.Range_Shifted + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => Find (Elements (Container), New_Item), + Lst => Length (Container)'Old, + Offset => 1) + + -- A new cursor has been inserted in Container + + and P_Positions_Shifted + (Positions (Container)'Old, + Positions (Container), + Cut => Find (Elements (Container), New_Item)); + + procedure Include + (Container : in out Set; + New_Item : Element_Type) + with + Global => null, + Pre => + Length (Container) < Container.Capacity + or Contains (Container, New_Item), + Post => Contains (Container, New_Item), + Contract_Cases => + + -- If New_Item is already in Container + + (Contains (Container, New_Item) => + + -- Elements are preserved + + Model (Container)'Old = Model (Container) + + -- Cursors are preserved + + and Positions (Container) = Positions (Container)'Old + + -- The element equivalent to New_Item in Container is replaced by + -- New_Item. + + and E.Get (Elements (Container), + Find (Elements (Container), New_Item)) = New_Item + + and E.Equal_Except + (Elements (Container)'Old, + Elements (Container), + Find (Elements (Container), New_Item)), + + -- Otherwise, New_Item is inserted in Container + + others => + Length (Container) = Length (Container)'Old + 1 + + -- Other elements are preserved + + and Model (Container)'Old <= Model (Container) + and M.Included_Except + (Model (Container), + Model (Container)'Old, + New_Item) + + -- New_Item is inserted in Container + + and E.Get (Elements (Container), + Find (Elements (Container), New_Item)) = New_Item + + -- The Elements of Container located before New_Item are preserved + + and E.Range_Equal + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => 1, + Lst => Find (Elements (Container), New_Item) - 1) + + -- Other Elements are shifted by 1 + + and E.Range_Shifted + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => Find (Elements (Container), New_Item), + Lst => Length (Container)'Old, + Offset => 1) + + -- A new cursor has been inserted in Container + + and P_Positions_Shifted + (Positions (Container)'Old, + Positions (Container), + Cut => Find (Elements (Container), New_Item))); + + procedure Replace + (Container : in out Set; + New_Item : Element_Type) + with + Global => null, + Pre => Contains (Container, New_Item), + Post => + + -- Elements are preserved + + Model (Container)'Old = Model (Container) + + -- Cursors are preserved + + and Positions (Container) = Positions (Container)'Old + + -- The element equivalent to New_Item in Container is replaced by + -- New_Item. + + and E.Get (Elements (Container), + Find (Elements (Container), New_Item)) = New_Item + and E.Equal_Except + (Elements (Container)'Old, + Elements (Container), + Find (Elements (Container), New_Item)); + + procedure Exclude + (Container : in out Set; + Item : Element_Type) + with + Global => null, + Post => not Contains (Container, Item), + Contract_Cases => + + -- If Item is not in Container, nothing is changed + + (not Contains (Container, Item) => + Model (Container) = Model (Container)'Old + and Elements (Container) = Elements (Container)'Old + and Positions (Container) = Positions (Container)'Old, + + -- Otherwise, Item is removed from Container + + others => + Length (Container) = Length (Container)'Old - 1 + + -- Other elements are preserved + + and Model (Container) <= Model (Container)'Old + and M.Included_Except + (Model (Container)'Old, + Model (Container), + Item) + + -- The elements of Container located before Item are preserved + + and E.Range_Equal + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => 1, + Lst => Find (Elements (Container), Item)'Old - 1) + + -- The elements located after Item are shifted by 1 + + and E.Range_Shifted + (Left => Elements (Container), + Right => Elements (Container)'Old, + Fst => Find (Elements (Container), Item)'Old, + Lst => Length (Container), + Offset => 1) + + -- A cursor has been removed from Container + + and P_Positions_Shifted + (Positions (Container), + Positions (Container)'Old, + Cut => Find (Elements (Container), Item)'Old)); + + procedure Delete + (Container : in out Set; + Item : Element_Type) + with + Global => null, + Pre => Contains (Container, Item), + Post => + Length (Container) = Length (Container)'Old - 1 + + -- Item is no longer in Container + + and not Contains (Container, Item) + + -- Other elements are preserved + + and Model (Container) <= Model (Container)'Old + and M.Included_Except + (Model (Container)'Old, + Model (Container), + Item) + + -- The elements of Container located before Item are preserved + + and E.Range_Equal + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => 1, + Lst => Find (Elements (Container), Item)'Old - 1) + + -- The elements located after Item are shifted by 1 + + and E.Range_Shifted + (Left => Elements (Container), + Right => Elements (Container)'Old, + Fst => Find (Elements (Container), Item)'Old, + Lst => Length (Container), + Offset => 1) + + -- A cursor has been removed from Container + + and P_Positions_Shifted + (Positions (Container), + Positions (Container)'Old, + Cut => Find (Elements (Container), Item)'Old); + + procedure Delete + (Container : in out Set; + Position : in out Cursor) + with + Global => null, + Pre => Has_Element (Container, Position), + Post => + Position = No_Element + and Length (Container) = Length (Container)'Old - 1 + + -- The element at position Position is no longer in Container + + and not Contains (Container, Element (Container, Position)'Old) + and not P.Has_Key (Positions (Container), Position'Old) + + -- Other elements are preserved + + and Model (Container) <= Model (Container)'Old + and M.Included_Except + (Model (Container)'Old, + Model (Container), + Element (Container, Position)'Old) + + -- The elements of Container located before Position are preserved. + + and E.Range_Equal + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => 1, + Lst => P.Get (Positions (Container)'Old, Position'Old) - 1) + + -- The elements located after Position are shifted by 1 + + and E.Range_Shifted + (Left => Elements (Container), + Right => Elements (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 Set) with + Global => null, + Contract_Cases => + (Length (Container) = 0 => Length (Container) = 0, + others => + Length (Container) = Length (Container)'Old - 1 + + -- The first element has been removed from Container + + and not Contains (Container, First_Element (Container)'Old) + + -- Other elements are preserved + + and Model (Container) <= Model (Container)'Old + and M.Included_Except + (Model (Container)'Old, + Model (Container), + First_Element (Container)'Old) + + -- Other elements are shifted by 1 + + and E.Range_Shifted + (Left => Elements (Container), + Right => Elements (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 Set) with + Global => null, + Contract_Cases => + (Length (Container) = 0 => Length (Container) = 0, + others => + Length (Container) = Length (Container)'Old - 1 + + -- The last element has been removed from Container + + and not Contains (Container, Last_Element (Container)'Old) + + -- Other elements are preserved + + and Model (Container) <= Model (Container)'Old + and M.Included_Except + (Model (Container)'Old, + Model (Container), + Last_Element (Container)'Old) + + -- Others elements of Container are preserved + + and E.Range_Equal + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => 1, + Lst => Length (Container)) + + -- Last cursor has been removed from Container + + and Positions (Container) <= Positions (Container)'Old); + + procedure Union (Target : in out Set; Source : Set) with + Global => null, + Pre => + Length (Source) - Length (Target and Source) <= + Target.Capacity - Length (Target), + Post => + Length (Target) = Length (Target)'Old + - M.Num_Overlaps (Model (Target)'Old, Model (Source)) + + Length (Source) + + -- Elements already in Target are still in Target + + and Model (Target)'Old <= Model (Target) + + -- Elements of Source are included in Target + + and Model (Source) <= Model (Target) + + -- Elements of Target come from either Source or Target + + and + M.Included_In_Union + (Model (Target), Model (Source), Model (Target)'Old) + + -- Actual value of elements come from either Left or Right + + and + E_Elements_Included + (Elements (Target), + Model (Target)'Old, + Elements (Target)'Old, + Elements (Source)) + and + E_Elements_Included + (Elements (Target)'Old, Model (Target)'Old, Elements (Target)) + and + E_Elements_Included + (Elements (Source), + Model (Target)'Old, + Elements (Source), + Elements (Target)) + + -- Mapping from cursors of Target to elements is preserved + + and Mapping_Preserved + (E_Left => Elements (Target)'Old, + E_Right => Elements (Target), + P_Left => Positions (Target)'Old, + P_Right => Positions (Target)); + + function Union (Left, Right : Set) return Set with + Global => null, + Pre => Length (Left) <= Count_Type'Last - Length (Right), + Post => + Length (Union'Result) = Length (Left) + - M.Num_Overlaps (Model (Left), Model (Right)) + + Length (Right) + + -- Elements of Left and Right are in the result of Union + + and Model (Left) <= Model (Union'Result) + and Model (Right) <= Model (Union'Result) + + -- Elements of the result of union come from either Left or Right + + and + M.Included_In_Union + (Model (Union'Result), Model (Left), Model (Right)) + + -- Actual value of elements come from either Left or Right + + and + E_Elements_Included + (Elements (Union'Result), + Model (Left), + Elements (Left), + Elements (Right)) + and + E_Elements_Included + (Elements (Left), Model (Left), Elements (Union'Result)) + and + E_Elements_Included + (Elements (Right), + Model (Left), + Elements (Right), + Elements (Union'Result)); + + function "or" (Left, Right : Set) return Set renames Union; + + procedure Intersection (Target : in out Set; Source : Set) with + Global => null, + Post => + Length (Target) = + M.Num_Overlaps (Model (Target)'Old, Model (Source)) + + -- Elements of Target were already in Target + + and Model (Target) <= Model (Target)'Old + + -- Elements of Target are in Source + + and Model (Target) <= Model (Source) + + -- Elements both in Source and Target are in the intersection + + and + M.Includes_Intersection + (Model (Target), Model (Source), Model (Target)'Old) + + -- Actual value of elements of Target is preserved + + and E_Elements_Included (Elements (Target), Elements (Target)'Old) + and + E_Elements_Included + (Elements (Target)'Old, Model (Source), Elements (Target)) + + -- Mapping from cursors of Target to elements is preserved + + and Mapping_Preserved + (E_Left => Elements (Target), + E_Right => Elements (Target)'Old, + P_Left => Positions (Target), + P_Right => Positions (Target)'Old); + + function Intersection (Left, Right : Set) return Set with + Global => null, + Post => + Length (Intersection'Result) = + M.Num_Overlaps (Model (Left), Model (Right)) + + -- Elements in the result of Intersection are in Left and Right + + and Model (Intersection'Result) <= Model (Left) + and Model (Intersection'Result) <= Model (Right) + + -- Elements both in Left and Right are in the result of Intersection + + and + M.Includes_Intersection + (Model (Intersection'Result), Model (Left), Model (Right)) + + -- Actual value of elements come from Left + + and + E_Elements_Included + (Elements (Intersection'Result), Elements (Left)) + and + E_Elements_Included + (Elements (Left), Model (Right), Elements (Intersection'Result)); + + function "and" (Left, Right : Set) return Set renames Intersection; + + procedure Difference (Target : in out Set; Source : Set) with + Global => null, + Post => + Length (Target) = Length (Target)'Old - + M.Num_Overlaps (Model (Target)'Old, Model (Source)) + + -- Elements of Target were already in Target + + and Model (Target) <= Model (Target)'Old + + -- Elements of Target are not in Source + + and M.No_Overlap (Model (Target), Model (Source)) + + -- Elements in Target but not in Source are in the difference + + and + M.Included_In_Union + (Model (Target)'Old, Model (Target), Model (Source)) + + -- Actual value of elements of Target is preserved + + and E_Elements_Included (Elements (Target), Elements (Target)'Old) + and + E_Elements_Included + (Elements (Target)'Old, Model (Target), Elements (Target)) + + -- Mapping from cursors of Target to elements is preserved + + and Mapping_Preserved + (E_Left => Elements (Target), + E_Right => Elements (Target)'Old, + P_Left => Positions (Target), + P_Right => Positions (Target)'Old); + + function Difference (Left, Right : Set) return Set with + Global => null, + Post => + Length (Difference'Result) = Length (Left) - + M.Num_Overlaps (Model (Left), Model (Right)) + + -- Elements of the result of Difference are in Left + + and Model (Difference'Result) <= Model (Left) + + -- Elements of the result of Difference are in Right + + and M.No_Overlap (Model (Difference'Result), Model (Right)) + + -- Elements in Left but not in Right are in the difference + + and + M.Included_In_Union + (Model (Left), Model (Difference'Result), Model (Right)) + + -- Actual value of elements come from Left + + and + E_Elements_Included (Elements (Difference'Result), Elements (Left)) + and + E_Elements_Included + (Elements (Left), + Model (Difference'Result), + Elements (Difference'Result)); + + function "-" (Left, Right : Set) return Set renames Difference; + + procedure Symmetric_Difference (Target : in out Set; Source : Set) with + Global => null, + Pre => + Length (Source) - Length (Target and Source) <= + Target.Capacity - Length (Target) + Length (Target and Source), + Post => + Length (Target) = Length (Target)'Old - + 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) + + Length (Source) + + -- Elements of the difference were not both in Source and in Target + + and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source)) + + -- Elements in Target but not in Source are in the difference + + and + M.Included_In_Union + (Model (Target)'Old, Model (Target), Model (Source)) + + -- Elements in Source but not in Target are in the difference + + and + M.Included_In_Union + (Model (Source), Model (Target), Model (Target)'Old) + + -- Actual value of elements come from either Left or Right + + and + E_Elements_Included + (Elements (Target), + Model (Target)'Old, + Elements (Target)'Old, + Elements (Source)) + and + E_Elements_Included + (Elements (Target)'Old, Model (Target), Elements (Target)) + and + E_Elements_Included + (Elements (Source), Model (Target), Elements (Target)); + + function Symmetric_Difference (Left, Right : Set) return Set with + Global => null, + Pre => Length (Left) <= Count_Type'Last - Length (Right), + Post => + Length (Symmetric_Difference'Result) = Length (Left) - + 2 * M.Num_Overlaps (Model (Left), Model (Right)) + + Length (Right) + + -- Elements of the difference were not both in Left and Right + + and + M.Not_In_Both + (Model (Symmetric_Difference'Result), Model (Left), Model (Right)) + + -- Elements in Left but not in Right are in the difference + + and + M.Included_In_Union + (Model (Left), Model (Symmetric_Difference'Result), Model (Right)) + + -- Elements in Right but not in Left are in the difference + + and + M.Included_In_Union + (Model (Right), Model (Symmetric_Difference'Result), Model (Left)) + + -- Actual value of elements come from either Left or Right + + and + E_Elements_Included + (Elements (Symmetric_Difference'Result), + Model (Left), + Elements (Left), + Elements (Right)) + and + E_Elements_Included + (Elements (Left), + Model (Symmetric_Difference'Result), + Elements (Symmetric_Difference'Result)) + and + E_Elements_Included + (Elements (Right), + Model (Symmetric_Difference'Result), + Elements (Symmetric_Difference'Result)); + + function "xor" (Left, Right : Set) return Set + renames Symmetric_Difference; + + function Overlap (Left, Right : Set) return Boolean with + Global => null, + Post => + Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right))); + + function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with + Global => null, + Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set)); + + function First (Container : Set) return Cursor with + 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 : Set) return Element_Type with + Global => null, + Pre => not Is_Empty (Container), + Post => + First_Element'Result = E.Get (Elements (Container), 1) + and E_Smaller_Than_Range + (Elements (Container), + 2, + Length (Container), + First_Element'Result); + + function Last (Container : Set) return Cursor with + 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 : Set) return Element_Type with + Global => null, + Pre => not Is_Empty (Container), + Post => + Last_Element'Result = E.Get (Elements (Container), Length (Container)) + and E_Bigger_Than_Range + (Elements (Container), + 1, + Length (Container) - 1, + Last_Element'Result); + + function Next (Container : Set; Position : Cursor) return Cursor with + 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 : Set; Position : in out Cursor) with + 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 : Set; Position : Cursor) return Cursor with + 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 : Set; Position : in out Cursor) with + 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 : Set; Item : Element_Type) return Cursor with + Global => null, + Contract_Cases => + + -- If Item is not contained in Container, Find returns No_Element + + (not Contains (Model (Container), Item) => + not P.Has_Key (Positions (Container), Find'Result) + and Find'Result = No_Element, + + -- Otherwise, Find returns a valid cursor in Container + + others => + P.Has_Key (Positions (Container), Find'Result) + and P.Get (Positions (Container), Find'Result) = + Find (Elements (Container), Item) + + -- The element designated by the result of Find is Item + + and Equivalent_Elements + (Element (Container, Find'Result), Item)); + + function Floor (Container : Set; Item : Element_Type) return Cursor with + Global => null, + Contract_Cases => + (Length (Container) = 0 or else Item < First_Element (Container) => + Floor'Result = No_Element, + others => + Has_Element (Container, Floor'Result) + and + not (Item < E.Get (Elements (Container), + P.Get (Positions (Container), Floor'Result))) + and E_Is_Find + (Elements (Container), + Item, + P.Get (Positions (Container), Floor'Result))); + + function Ceiling (Container : Set; Item : Element_Type) return Cursor with + Global => null, + Contract_Cases => + (Length (Container) = 0 or else Last_Element (Container) < Item => + Ceiling'Result = No_Element, + others => + Has_Element (Container, Ceiling'Result) + and + not (E.Get (Elements (Container), + P.Get (Positions (Container), Ceiling'Result)) < + Item) + and E_Is_Find + (Elements (Container), + Item, + P.Get (Positions (Container), Ceiling'Result))); + + function Contains (Container : Set; Item : Element_Type) return Boolean with + Global => null, + Post => Contains'Result = Contains (Model (Container), Item); + pragma Annotate (GNATprove, Inline_For_Proof, Contains); + + function Has_Element (Container : Set; Position : Cursor) return Boolean + with + Global => null, + Post => + Has_Element'Result = P.Has_Key (Positions (Container), Position); + pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); + + generic + type Key_Type (<>) is private; + + with function Key (Element : Element_Type) return Key_Type; + + with function "<" (Left, Right : Key_Type) return Boolean is <>; + + package Generic_Keys with SPARK_Mode is + + function Equivalent_Keys (Left, Right : Key_Type) return Boolean with + Global => null, + Post => + Equivalent_Keys'Result = (not (Left < Right) and not (Right < Left)); + pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Keys); + + package Formal_Model with Ghost is + function E_Bigger_Than_Range + (Container : E.Sequence; + Fst : Positive_Count_Type; + Lst : Count_Type; + Key : Key_Type) return Boolean + with + Global => null, + Pre => Lst <= E.Length (Container), + Post => + E_Bigger_Than_Range'Result = + (for all I in Fst .. Lst => + Generic_Keys.Key (E.Get (Container, I)) < Key); + pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range); + + function E_Smaller_Than_Range + (Container : E.Sequence; + Fst : Positive_Count_Type; + Lst : Count_Type; + Key : Key_Type) return Boolean + with + Global => null, + Pre => Lst <= E.Length (Container), + Post => + E_Smaller_Than_Range'Result = + (for all I in Fst .. Lst => + Key < Generic_Keys.Key (E.Get (Container, I))); + pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range); + + function E_Is_Find + (Container : E.Sequence; + Key : Key_Type; + Position : Count_Type) return Boolean + with + Global => null, + Pre => Position - 1 <= E.Length (Container), + Post => + E_Is_Find'Result = + + ((if Position > 0 then + E_Bigger_Than_Range (Container, 1, Position - 1, Key)) + + and (if Position < E.Length (Container) then + E_Smaller_Than_Range + (Container, + Position + 1, + E.Length (Container), + Key))); + pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find); + + function Find + (Container : E.Sequence; + Key : Key_Type) return Count_Type + -- Search for Key in Container + + with + Global => null, + Post => + (if Find'Result > 0 then + Find'Result <= E.Length (Container) + and Equivalent_Keys + (Key, Generic_Keys.Key (E.Get (Container, Find'Result))) + and E_Is_Find (Container, Key, Find'Result)); + + function M_Included_Except + (Left : M.Set; + Right : M.Set; + Key : Key_Type) return Boolean + with + Global => null, + Post => + M_Included_Except'Result = + (for all E of Left => + Contains (Right, E) + or Equivalent_Keys (Generic_Keys.Key (E), Key)); + end Formal_Model; + use Formal_Model; + + function Key (Container : Set; Position : Cursor) return Key_Type with + Global => null, + Post => Key'Result = Key (Element (Container, Position)); + pragma Annotate (GNATprove, Inline_For_Proof, Key); + + function Element (Container : Set; Key : Key_Type) return Element_Type + with + Global => null, + Pre => Contains (Container, Key), + Post => + Element'Result = Element (Container, Find (Container, Key)); + pragma Annotate (GNATprove, Inline_For_Proof, Element); + + procedure Replace + (Container : in out Set; + Key : Key_Type; + New_Item : Element_Type) + with + Global => null, + Pre => Contains (Container, Key), + Post => + Length (Container) = Length (Container)'Old + + -- Key now maps to New_Item + + and Element (Container, Key) = New_Item + + -- New_Item is contained in Container + + and Contains (Model (Container), New_Item) + + -- Other elements are preserved + + and M_Included_Except + (Model (Container)'Old, + Model (Container), + Key) + and M.Included_Except + (Model (Container), + Model (Container)'Old, + New_Item) + + -- Mapping from cursors to elements is preserved + + and Mapping_Preserved_Except + (E_Left => Elements (Container)'Old, + E_Right => Elements (Container), + P_Left => Positions (Container)'Old, + P_Right => Positions (Container), + Position => Find (Container, Key)) + and Positions (Container) = Positions (Container)'Old; + + procedure Exclude (Container : in out Set; Key : Key_Type) with + 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 Elements (Container) = Elements (Container)'Old + and Positions (Container) = Positions (Container)'Old, + + -- Otherwise, Key is removed from Container + + others => + Length (Container) = Length (Container)'Old - 1 + + -- Other elements are preserved + + and Model (Container) <= Model (Container)'Old + and M_Included_Except + (Model (Container)'Old, + Model (Container), + Key) + + -- The elements of Container located before Key are preserved + + and E.Range_Equal + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => 1, + Lst => Find (Elements (Container), Key)'Old - 1) + + -- The elements located after Key are shifted by 1 + + and E.Range_Shifted + (Left => Elements (Container), + Right => Elements (Container)'Old, + Fst => Find (Elements (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 => Find (Elements (Container), Key)'Old)); + + procedure Delete (Container : in out Set; Key : Key_Type) with + Global => null, + Pre => Contains (Container, Key), + Post => + Length (Container) = Length (Container)'Old - 1 + + -- Key is no longer in Container + + and not Contains (Container, Key) + + -- Other elements are preserved + + and Model (Container) <= Model (Container)'Old + and M_Included_Except + (Model (Container)'Old, + Model (Container), + Key) + + -- The elements of Container located before Key are preserved + + and E.Range_Equal + (Left => Elements (Container)'Old, + Right => Elements (Container), + Fst => 1, + Lst => Find (Elements (Container), Key)'Old - 1) + + -- The elements located after Key are shifted by 1 + + and E.Range_Shifted + (Left => Elements (Container), + Right => Elements (Container)'Old, + Fst => Find (Elements (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 => Find (Elements (Container), Key)'Old); + + function Find (Container : Set; Key : Key_Type) return Cursor with + Global => null, + Contract_Cases => + + -- If Key is not contained in Container, Find returns No_Element + + ((for all E of Model (Container) => + not Equivalent_Keys (Key, Generic_Keys.Key (E))) => + not P.Has_Key (Positions (Container), Find'Result) + and Find'Result = No_Element, + + -- Otherwise, Find returns a valid cursor in Container + + others => + P.Has_Key (Positions (Container), Find'Result) + and P.Get (Positions (Container), Find'Result) = + Find (Elements (Container), Key) + + -- The element designated by the result of Find is Key + + and Equivalent_Keys + (Generic_Keys.Key (Element (Container, Find'Result)), Key)); + + function Floor (Container : Set; Key : Key_Type) return Cursor with + Global => null, + Contract_Cases => + (Length (Container) = 0 + or else Key < Generic_Keys.Key (First_Element (Container)) => + Floor'Result = No_Element, + others => + Has_Element (Container, Floor'Result) + and + not (Key < + Generic_Keys.Key + (E.Get (Elements (Container), + P.Get (Positions (Container), Floor'Result)))) + and E_Is_Find + (Elements (Container), + Key, + P.Get (Positions (Container), Floor'Result))); + + function Ceiling (Container : Set; Key : Key_Type) return Cursor with + Global => null, + Contract_Cases => + (Length (Container) = 0 + or else Generic_Keys.Key (Last_Element (Container)) < Key => + Ceiling'Result = No_Element, + others => + Has_Element (Container, Ceiling'Result) + and + not (Generic_Keys.Key + (E.Get (Elements (Container), + P.Get (Positions (Container), Ceiling'Result))) + < Key) + and E_Is_Find + (Elements (Container), + Key, + P.Get (Positions (Container), Ceiling'Result))); + + function Contains (Container : Set; Key : Key_Type) return Boolean with + Global => null, + Post => + Contains'Result = + (for some E of Model (Container) => + Equivalent_Keys (Key, Generic_Keys.Key (E))); + + end Generic_Keys; + +private + pragma SPARK_Mode (Off); + + pragma Inline (Next); + pragma Inline (Previous); + + type Node_Type is record + Has_Element : Boolean := False; + Parent : Count_Type := 0; + Left : Count_Type := 0; + Right : Count_Type := 0; + Color : Red_Black_Trees.Color_Type; + Element : Element_Type; + end record; + + package Tree_Types is + new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type); + + type Set (Capacity : Count_Type) is + new Tree_Types.Tree_Type (Capacity) with null record; + + use Red_Black_Trees; + + Empty_Set : constant Set := (Capacity => 0, others => <>); + +end Ada.Containers.Formal_Ordered_Sets;