1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- ADA.CONTAINERS.FUNCTIONAL_SETS -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2016-2019, Free Software Foundation, Inc. -- 10-- -- 11-- This specification is derived from the Ada Reference Manual for use with -- 12-- GNAT. The copyright notice above, and the license provisions that follow -- 13-- apply solely to the contents of the part following the private keyword. -- 14-- -- 15-- GNAT is free software; you can redistribute it and/or modify it under -- 16-- terms of the GNU General Public License as published by the Free Soft- -- 17-- ware Foundation; either version 3, or (at your option) any later ver- -- 18-- sion. GNAT is distributed in the hope that it will be useful, but WITH- -- 19-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -- 20-- or FITNESS FOR A PARTICULAR PURPOSE. -- 21-- -- 22-- As a special exception under Section 7 of GPL version 3, you are granted -- 23-- additional permissions described in the GCC Runtime Library Exception, -- 24-- version 3.1, as published by the Free Software Foundation. -- 25-- -- 26-- You should have received a copy of the GNU General Public License and -- 27-- a copy of the GCC Runtime Library Exception along with this program; -- 28-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see -- 29-- <http://www.gnu.org/licenses/>. -- 30------------------------------------------------------------------------------ 31 32pragma Ada_2012; 33private with Ada.Containers.Functional_Base; 34 35generic 36 type Element_Type (<>) is private; 37 38 with function Equivalent_Elements 39 (Left : Element_Type; 40 Right : Element_Type) return Boolean is "="; 41 42 Enable_Handling_Of_Equivalence : Boolean := True; 43 -- This constant should only be set to False when no particular handling 44 -- of equivalence over elements is needed, that is, Equivalent_Elements 45 -- defines an element uniquely. 46 47package Ada.Containers.Functional_Sets with SPARK_Mode is 48 49 type Set is private with 50 Default_Initial_Condition => Is_Empty (Set), 51 Iterable => (First => Iter_First, 52 Next => Iter_Next, 53 Has_Element => Iter_Has_Element, 54 Element => Iter_Element); 55 -- Sets are empty when default initialized. 56 -- "For in" quantification over sets should not be used. 57 -- "For of" quantification over sets iterates over elements. 58 -- Note that, for proof, "for of" quantification is understood modulo 59 -- equivalence (the range of quantification comprises all the elements that 60 -- are equivalent to any element of the set). 61 62 ----------------------- 63 -- Basic operations -- 64 ----------------------- 65 66 -- Sets are axiomatized using Contains, which encodes whether an element is 67 -- contained in a set. The length of a set is also added to protect Add 68 -- against overflows but it is not actually modeled. 69 70 function Contains (Container : Set; Item : Element_Type) return Boolean with 71 -- Return True if Item is contained in Container 72 73 Global => null, 74 Post => 75 (if Enable_Handling_Of_Equivalence then 76 77 -- Contains returns the same result on all equivalent elements 78 79 (if (for some E of Container => Equivalent_Elements (E, Item)) then 80 Contains'Result)); 81 82 function Length (Container : Set) return Count_Type with 83 Global => null; 84 -- Return the number of elements in Container 85 86 ------------------------ 87 -- Property Functions -- 88 ------------------------ 89 90 function "<=" (Left : Set; Right : Set) return Boolean with 91 -- Set inclusion 92 93 Global => null, 94 Post => "<="'Result = (for all Item of Left => Contains (Right, Item)); 95 96 function "=" (Left : Set; Right : Set) return Boolean with 97 -- Extensional equality over sets 98 99 Global => null, 100 Post => "="'Result = (Left <= Right and Right <= Left); 101 102 pragma Warnings (Off, "unused variable ""Item"""); 103 function Is_Empty (Container : Set) return Boolean with 104 -- A set is empty if it contains no element 105 106 Global => null, 107 Post => 108 Is_Empty'Result = (for all Item of Container => False) 109 and Is_Empty'Result = (Length (Container) = 0); 110 pragma Warnings (On, "unused variable ""Item"""); 111 112 function Included_Except 113 (Left : Set; 114 Right : Set; 115 Item : Element_Type) return Boolean 116 -- Return True if Left contains only elements of Right except possibly 117 -- Item. 118 119 with 120 Global => null, 121 Post => 122 Included_Except'Result = 123 (for all E of Left => 124 Contains (Right, E) or Equivalent_Elements (E, Item)); 125 126 function Includes_Intersection 127 (Container : Set; 128 Left : Set; 129 Right : Set) return Boolean 130 with 131 -- Return True if every element of the intersection of Left and Right is 132 -- in Container. 133 134 Global => null, 135 Post => 136 Includes_Intersection'Result = 137 (for all Item of Left => 138 (if Contains (Right, Item) then Contains (Container, Item))); 139 140 function Included_In_Union 141 (Container : Set; 142 Left : Set; 143 Right : Set) return Boolean 144 with 145 -- Return True if every element of Container is the union of Left and Right 146 147 Global => null, 148 Post => 149 Included_In_Union'Result = 150 (for all Item of Container => 151 Contains (Left, Item) or Contains (Right, Item)); 152 153 function Is_Singleton 154 (Container : Set; 155 New_Item : Element_Type) return Boolean 156 with 157 -- Return True Container only contains New_Item 158 159 Global => null, 160 Post => 161 Is_Singleton'Result = 162 (for all Item of Container => Equivalent_Elements (Item, New_Item)); 163 164 function Not_In_Both 165 (Container : Set; 166 Left : Set; 167 Right : Set) return Boolean 168 -- Return True if there are no elements in Container that are in Left and 169 -- Right. 170 171 with 172 Global => null, 173 Post => 174 Not_In_Both'Result = 175 (for all Item of Container => 176 not Contains (Left, Item) or not Contains (Right, Item)); 177 178 function No_Overlap (Left : Set; Right : Set) return Boolean with 179 -- Return True if there are no equivalent elements in Left and Right 180 181 Global => null, 182 Post => 183 No_Overlap'Result = 184 (for all Item of Left => not Contains (Right, Item)); 185 186 function Num_Overlaps (Left : Set; Right : Set) return Count_Type with 187 -- Number of elements that are both in Left and Right 188 189 Global => null, 190 Post => 191 Num_Overlaps'Result = Length (Intersection (Left, Right)) 192 and (if Left <= Right then Num_Overlaps'Result = Length (Left) 193 else Num_Overlaps'Result < Length (Left)) 194 and (if Right <= Left then Num_Overlaps'Result = Length (Right) 195 else Num_Overlaps'Result < Length (Right)) 196 and (Num_Overlaps'Result = 0) = No_Overlap (Left, Right); 197 198 ---------------------------- 199 -- Construction Functions -- 200 ---------------------------- 201 202 -- For better efficiency of both proofs and execution, avoid using 203 -- construction functions in annotations and rather use property functions. 204 205 function Add (Container : Set; Item : Element_Type) return Set with 206 -- Return a new set containing all the elements of Container plus E 207 208 Global => null, 209 Pre => 210 not Contains (Container, Item) 211 and Length (Container) < Count_Type'Last, 212 Post => 213 Length (Add'Result) = Length (Container) + 1 214 and Contains (Add'Result, Item) 215 and Container <= Add'Result 216 and Included_Except (Add'Result, Container, Item); 217 218 function Remove (Container : Set; Item : Element_Type) return Set with 219 -- Return a new set containing all the elements of Container except E 220 221 Global => null, 222 Pre => Contains (Container, Item), 223 Post => 224 Length (Remove'Result) = Length (Container) - 1 225 and not Contains (Remove'Result, Item) 226 and Remove'Result <= Container 227 and Included_Except (Container, Remove'Result, Item); 228 229 function Intersection (Left : Set; Right : Set) return Set with 230 -- Returns the intersection of Left and Right 231 232 Global => null, 233 Post => 234 Intersection'Result <= Left 235 and Intersection'Result <= Right 236 and Includes_Intersection (Intersection'Result, Left, Right); 237 238 function Union (Left : Set; Right : Set) return Set with 239 -- Returns the union of Left and Right 240 241 Global => null, 242 Pre => 243 Length (Left) - Num_Overlaps (Left, Right) <= 244 Count_Type'Last - Length (Right), 245 Post => 246 Length (Union'Result) = 247 Length (Left) - Num_Overlaps (Left, Right) + Length (Right) 248 and Left <= Union'Result 249 and Right <= Union'Result 250 and Included_In_Union (Union'Result, Left, Right); 251 252 --------------------------- 253 -- Iteration Primitives -- 254 --------------------------- 255 256 type Private_Key is private; 257 258 function Iter_First (Container : Set) return Private_Key with 259 Global => null; 260 261 function Iter_Has_Element 262 (Container : Set; 263 Key : Private_Key) return Boolean 264 with 265 Global => null; 266 267 function Iter_Next 268 (Container : Set; 269 Key : Private_Key) return Private_Key 270 with 271 Global => null, 272 Pre => Iter_Has_Element (Container, Key); 273 274 function Iter_Element 275 (Container : Set; 276 Key : Private_Key) return Element_Type 277 with 278 Global => null, 279 Pre => Iter_Has_Element (Container, Key); 280 pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Contains); 281 282private 283 284 pragma SPARK_Mode (Off); 285 286 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; 287 288 function "=" 289 (Left : Element_Type; 290 Right : Element_Type) return Boolean renames Equivalent_Elements; 291 292 package Containers is new Ada.Containers.Functional_Base 293 (Element_Type => Element_Type, 294 Index_Type => Positive_Count_Type); 295 296 type Set is record 297 Content : Containers.Container; 298 end record; 299 300 type Private_Key is new Count_Type; 301 302 function Iter_First (Container : Set) return Private_Key is (1); 303 304 function Iter_Has_Element 305 (Container : Set; 306 Key : Private_Key) return Boolean 307 is 308 (Count_Type (Key) in 1 .. Containers.Length (Container.Content)); 309 310 function Iter_Next 311 (Container : Set; 312 Key : Private_Key) return Private_Key 313 is 314 (if Key = Private_Key'Last then 0 else Key + 1); 315 316 function Iter_Element 317 (Container : Set; 318 Key : Private_Key) return Element_Type 319 is 320 (Containers.Get (Container.Content, Count_Type (Key))); 321 322end Ada.Containers.Functional_Sets; 323