------------------------------------------------------------------------------ | |

-- -- | |

-- 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; |