| ------------------------------------------------------------------------------ |
| -- -- |
| -- GNAT LIBRARY COMPONENTS -- |
| -- -- |
| -- ADA.CONTAINERS.FUNCTIONAL_SETS -- |
| -- -- |
| -- S p e c -- |
| -- -- |
| -- Copyright (C) 2016-2021, 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/>. -- |
| ------------------------------------------------------------------------------ |
| |
| pragma Ada_2012; |
| private with Ada.Containers.Functional_Base; |
| |
| generic |
| type Element_Type (<>) is private; |
| |
| with function Equivalent_Elements |
| (Left : Element_Type; |
| Right : Element_Type) return Boolean is "="; |
| |
| 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 |
| |
| type Set is private with |
| Default_Initial_Condition => Is_Empty (Set), |
| Iterable => (First => Iter_First, |
| Next => Iter_Next, |
| Has_Element => Iter_Has_Element, |
| Element => Iter_Element); |
| -- 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 (the range of quantification comprises all the elements that |
| -- are equivalent to any element of the set). |
| |
| ----------------------- |
| -- Basic operations -- |
| ----------------------- |
| |
| -- Sets are axiomatized using Contains, which encodes whether an element is |
| -- contained in a set. The length of a set is also added to protect Add |
| -- against overflows but it is not actually modeled. |
| |
| function Contains (Container : Set; Item : Element_Type) return Boolean with |
| -- 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 |
| |
| ------------------------ |
| -- Property Functions -- |
| ------------------------ |
| |
| function "<=" (Left : Set; Right : Set) return Boolean with |
| -- Set inclusion |
| |
| Global => null, |
| Post => "<="'Result = (for all Item of Left => Contains (Right, Item)); |
| |
| function "=" (Left : Set; Right : Set) return Boolean with |
| -- Extensional equality over sets |
| |
| Global => null, |
| Post => "="'Result = (Left <= Right and Right <= Left); |
| |
| pragma Warnings (Off, "unused variable ""Item"""); |
| function Is_Empty (Container : Set) return Boolean with |
| -- A set is empty if it contains no element |
| |
| Global => null, |
| Post => |
| Is_Empty'Result = (for all Item of Container => False) |
| and Is_Empty'Result = (Length (Container) = 0); |
| pragma Warnings (On, "unused variable ""Item"""); |
| |
| function Included_Except |
| (Left : Set; |
| Right : Set; |
| Item : Element_Type) return Boolean |
| -- Return True if Left contains only elements of Right except possibly |
| -- Item. |
| |
| with |
| Global => null, |
| Post => |
| Included_Except'Result = |
| (for all E of Left => |
| Contains (Right, E) or Equivalent_Elements (E, Item)); |
| |
| function Includes_Intersection |
| (Container : Set; |
| Left : Set; |
| Right : Set) return Boolean |
| with |
| -- Return True if every element of the intersection of Left and Right is |
| -- in Container. |
| |
| Global => null, |
| Post => |
| Includes_Intersection'Result = |
| (for all Item of Left => |
| (if Contains (Right, Item) then Contains (Container, Item))); |
| |
| function Included_In_Union |
| (Container : Set; |
| Left : Set; |
| Right : Set) return Boolean |
| with |
| -- Return True if every element of Container is the union of Left and Right |
| |
| Global => null, |
| Post => |
| Included_In_Union'Result = |
| (for all Item of Container => |
| Contains (Left, Item) or Contains (Right, Item)); |
| |
| function Is_Singleton |
| (Container : Set; |
| New_Item : Element_Type) return Boolean |
| with |
| -- Return True Container only contains New_Item |
| |
| Global => null, |
| Post => |
| Is_Singleton'Result = |
| (for all Item of Container => Equivalent_Elements (Item, New_Item)); |
| |
| function Not_In_Both |
| (Container : Set; |
| Left : Set; |
| Right : Set) return Boolean |
| -- Return True if there are no elements in Container that are in Left and |
| -- Right. |
| |
| with |
| Global => null, |
| Post => |
| Not_In_Both'Result = |
| (for all Item of Container => |
| not Contains (Left, Item) or not Contains (Right, Item)); |
| |
| function No_Overlap (Left : Set; Right : Set) return Boolean with |
| -- Return True if there are no equivalent elements in Left and Right |
| |
| Global => null, |
| Post => |
| No_Overlap'Result = |
| (for all Item of Left => not Contains (Right, Item)); |
| |
| function Num_Overlaps (Left : Set; Right : Set) return Count_Type with |
| -- Number of elements that are both in Left and Right |
| |
| Global => null, |
| Post => |
| Num_Overlaps'Result = Length (Intersection (Left, Right)) |
| and (if Left <= Right then Num_Overlaps'Result = Length (Left) |
| else Num_Overlaps'Result < Length (Left)) |
| and (if Right <= Left then Num_Overlaps'Result = Length (Right) |
| else Num_Overlaps'Result < Length (Right)) |
| and (Num_Overlaps'Result = 0) = No_Overlap (Left, Right); |
| |
| ---------------------------- |
| -- Construction Functions -- |
| ---------------------------- |
| |
| -- For better efficiency of both proofs and execution, avoid using |
| -- construction functions in annotations and rather use property functions. |
| |
| function Add (Container : Set; Item : Element_Type) return Set with |
| -- Return a new set containing all the elements of Container plus E |
| |
| Global => null, |
| Pre => |
| not Contains (Container, Item) |
| and Length (Container) < Count_Type'Last, |
| Post => |
| Length (Add'Result) = Length (Container) + 1 |
| and Contains (Add'Result, Item) |
| and Container <= Add'Result |
| and Included_Except (Add'Result, Container, Item); |
| |
| function Remove (Container : Set; Item : Element_Type) return Set with |
| -- Return a new set containing all the elements of Container except E |
| |
| Global => null, |
| Pre => Contains (Container, Item), |
| Post => |
| Length (Remove'Result) = Length (Container) - 1 |
| and not Contains (Remove'Result, Item) |
| and Remove'Result <= Container |
| and Included_Except (Container, Remove'Result, Item); |
| |
| function Intersection (Left : Set; Right : Set) return Set with |
| -- Returns the intersection of Left and Right |
| |
| Global => null, |
| Post => |
| Intersection'Result <= Left |
| and Intersection'Result <= Right |
| and Includes_Intersection (Intersection'Result, Left, Right); |
| |
| function Union (Left : Set; Right : Set) return Set with |
| -- Returns the union of Left and Right |
| |
| Global => null, |
| Pre => |
| Length (Left) - Num_Overlaps (Left, Right) <= |
| Count_Type'Last - Length (Right), |
| Post => |
| Length (Union'Result) = |
| Length (Left) - Num_Overlaps (Left, Right) + Length (Right) |
| and Left <= Union'Result |
| and Right <= Union'Result |
| and Included_In_Union (Union'Result, Left, Right); |
| |
| function Copy_Element (Item : Element_Type) return Element_Type is (Item); |
| -- Elements of containers are copied by numerous primitives in this |
| -- package. This function causes GNATprove to verify that such a copy is |
| -- valid (in particular, it does not break the ownership policy of SPARK, |
| -- i.e. it does not contain pointers that could be used to alias mutable |
| -- data). |
| |
| --------------------------- |
| -- Iteration Primitives -- |
| --------------------------- |
| |
| type Private_Key is private; |
| |
| function Iter_First (Container : Set) return Private_Key with |
| Global => null; |
| |
| function Iter_Has_Element |
| (Container : Set; |
| Key : Private_Key) return Boolean |
| with |
| Global => null; |
| |
| function Iter_Next |
| (Container : Set; |
| Key : Private_Key) return Private_Key |
| with |
| Global => null, |
| Pre => Iter_Has_Element (Container, Key); |
| |
| function Iter_Element |
| (Container : Set; |
| Key : Private_Key) return Element_Type |
| with |
| Global => null, |
| Pre => Iter_Has_Element (Container, Key); |
| pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Contains); |
| |
| private |
| |
| pragma SPARK_Mode (Off); |
| |
| subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; |
| |
| function "=" |
| (Left : Element_Type; |
| Right : Element_Type) return Boolean renames Equivalent_Elements; |
| |
| package Containers is new Ada.Containers.Functional_Base |
| (Element_Type => Element_Type, |
| Index_Type => Positive_Count_Type); |
| |
| type Set is record |
| Content : Containers.Container; |
| end record; |
| |
| type Private_Key is new Count_Type; |
| |
| function Iter_First (Container : Set) return Private_Key is (1); |
| |
| function Iter_Has_Element |
| (Container : Set; |
| Key : Private_Key) return Boolean |
| is |
| (Count_Type (Key) in 1 .. Containers.Length (Container.Content)); |
| |
| function Iter_Next |
| (Container : Set; |
| Key : Private_Key) return Private_Key |
| is |
| (if Key = Private_Key'Last then 0 else Key + 1); |
| |
| function Iter_Element |
| (Container : Set; |
| Key : Private_Key) return Element_Type |
| is |
| (Containers.Get (Container.Content, Count_Type (Key))); |
| |
| end Ada.Containers.Functional_Sets; |
