1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- 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 -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2004-2011, 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 32-- This spec is derived from package Ada.Containers.Bounded_Ordered_Sets in 33-- the Ada 2012 RM. The modifications are to facilitate formal proofs by 34-- making it easier to express properties. 35 36-- The modifications are: 37 38-- A parameter for the container is added to every function reading the 39-- content of a container: Key, Element, Next, Query_Element, Previous, 40-- Has_Element, Iterate, Reverse_Iterate. This change is motivated by the 41-- need to have cursors which are valid on different containers (typically 42-- a container C and its previous version C'Old) for expressing properties, 43-- which is not possible if cursors encapsulate an access to the underlying 44-- container. The operators "<" and ">" that could not be modified that way 45-- have been removed. 46 47-- There are three new functions: 48 49-- function Strict_Equal (Left, Right : Set) return Boolean; 50-- function Left (Container : Set; Position : Cursor) return Set; 51-- function Right (Container : Set; Position : Cursor) return Set; 52 53-- See detailed specifications for these subprograms 54 55private with Ada.Containers.Red_Black_Trees; 56private with Ada.Streams; 57 58generic 59 type Element_Type is private; 60 61 with function "<" (Left, Right : Element_Type) return Boolean is <>; 62 with function "=" (Left, Right : Element_Type) return Boolean is <>; 63 64package Ada.Containers.Formal_Ordered_Sets is 65 pragma Pure; 66 67 function Equivalent_Elements (Left, Right : Element_Type) return Boolean; 68 69 type Set (Capacity : Count_Type) is tagged private; 70 -- why is this commented out ??? 71 -- pragma Preelaborable_Initialization (Set); 72 73 type Cursor is private; 74 pragma Preelaborable_Initialization (Cursor); 75 76 Empty_Set : constant Set; 77 78 No_Element : constant Cursor; 79 80 function "=" (Left, Right : Set) return Boolean; 81 82 function Equivalent_Sets (Left, Right : Set) return Boolean; 83 84 function To_Set (New_Item : Element_Type) return Set; 85 86 function Length (Container : Set) return Count_Type; 87 88 function Is_Empty (Container : Set) return Boolean; 89 90 procedure Clear (Container : in out Set); 91 92 procedure Assign (Target : in out Set; Source : Set); 93 94 function Copy (Source : Set; Capacity : Count_Type := 0) return Set; 95 96 function Element (Container : Set; Position : Cursor) return Element_Type; 97 98 procedure Replace_Element 99 (Container : in out Set; 100 Position : Cursor; 101 New_Item : Element_Type); 102 103 procedure Query_Element 104 (Container : in out Set; 105 Position : Cursor; 106 Process : not null access procedure (Element : Element_Type)); 107 108 procedure Move (Target : in out Set; Source : in out Set); 109 110 procedure Insert 111 (Container : in out Set; 112 New_Item : Element_Type; 113 Position : out Cursor; 114 Inserted : out Boolean); 115 116 procedure Insert 117 (Container : in out Set; 118 New_Item : Element_Type); 119 120 procedure Include 121 (Container : in out Set; 122 New_Item : Element_Type); 123 124 procedure Replace 125 (Container : in out Set; 126 New_Item : Element_Type); 127 128 procedure Exclude 129 (Container : in out Set; 130 Item : Element_Type); 131 132 procedure Delete 133 (Container : in out Set; 134 Item : Element_Type); 135 136 procedure Delete 137 (Container : in out Set; 138 Position : in out Cursor); 139 140 procedure Delete_First (Container : in out Set); 141 142 procedure Delete_Last (Container : in out Set); 143 144 procedure Union (Target : in out Set; Source : Set); 145 146 function Union (Left, Right : Set) return Set; 147 148 function "or" (Left, Right : Set) return Set renames Union; 149 150 procedure Intersection (Target : in out Set; Source : Set); 151 152 function Intersection (Left, Right : Set) return Set; 153 154 function "and" (Left, Right : Set) return Set renames Intersection; 155 156 procedure Difference (Target : in out Set; Source : Set); 157 158 function Difference (Left, Right : Set) return Set; 159 160 function "-" (Left, Right : Set) return Set renames Difference; 161 162 procedure Symmetric_Difference (Target : in out Set; Source : Set); 163 164 function Symmetric_Difference (Left, Right : Set) return Set; 165 166 function "xor" (Left, Right : Set) return Set renames Symmetric_Difference; 167 168 function Overlap (Left, Right : Set) return Boolean; 169 170 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean; 171 172 function First (Container : Set) return Cursor; 173 174 function First_Element (Container : Set) return Element_Type; 175 176 function Last (Container : Set) return Cursor; 177 178 function Last_Element (Container : Set) return Element_Type; 179 180 function Next (Container : Set; Position : Cursor) return Cursor; 181 182 procedure Next (Container : Set; Position : in out Cursor); 183 184 function Previous (Container : Set; Position : Cursor) return Cursor; 185 186 procedure Previous (Container : Set; Position : in out Cursor); 187 188 function Find (Container : Set; Item : Element_Type) return Cursor; 189 190 function Floor (Container : Set; Item : Element_Type) return Cursor; 191 192 function Ceiling (Container : Set; Item : Element_Type) return Cursor; 193 194 function Contains (Container : Set; Item : Element_Type) return Boolean; 195 196 function Has_Element (Container : Set; Position : Cursor) return Boolean; 197 198 procedure Iterate 199 (Container : Set; 200 Process : 201 not null access procedure (Container : Set; Position : Cursor)); 202 203 procedure Reverse_Iterate 204 (Container : Set; 205 Process : not null access 206 procedure (Container : Set; Position : Cursor)); 207 208 generic 209 type Key_Type (<>) is private; 210 211 with function Key (Element : Element_Type) return Key_Type; 212 213 with function "<" (Left, Right : Key_Type) return Boolean is <>; 214 215 package Generic_Keys is 216 217 function Equivalent_Keys (Left, Right : Key_Type) return Boolean; 218 219 function Key (Container : Set; Position : Cursor) return Key_Type; 220 221 function Element (Container : Set; Key : Key_Type) return Element_Type; 222 223 procedure Replace 224 (Container : in out Set; 225 Key : Key_Type; 226 New_Item : Element_Type); 227 228 procedure Exclude (Container : in out Set; Key : Key_Type); 229 230 procedure Delete (Container : in out Set; Key : Key_Type); 231 232 function Find (Container : Set; Key : Key_Type) return Cursor; 233 234 function Floor (Container : Set; Key : Key_Type) return Cursor; 235 236 function Ceiling (Container : Set; Key : Key_Type) return Cursor; 237 238 function Contains (Container : Set; Key : Key_Type) return Boolean; 239 240 procedure Update_Element_Preserving_Key 241 (Container : in out Set; 242 Position : Cursor; 243 Process : not null access 244 procedure (Element : in out Element_Type)); 245 246 end Generic_Keys; 247 248 function Strict_Equal (Left, Right : Set) return Boolean; 249 -- Strict_Equal returns True if the containers are physically equal, i.e. 250 -- they are structurally equal (function "=" returns True) and that they 251 -- have the same set of cursors. 252 253 function Left (Container : Set; Position : Cursor) return Set; 254 function Right (Container : Set; Position : Cursor) return Set; 255 -- Left returns a container containing all elements preceding Position 256 -- (excluded) in Container. Right returns a container containing all 257 -- elements following Position (included) in Container. These two new 258 -- functions can be used to express invariant properties in loops which 259 -- iterate over containers. Left returns the part of the container already 260 -- scanned and Right the part not scanned yet. 261 262private 263 264 pragma Inline (Next); 265 pragma Inline (Previous); 266 267 type Node_Type is record 268 Has_Element : Boolean := False; 269 Parent : Count_Type := 0; 270 Left : Count_Type := 0; 271 Right : Count_Type := 0; 272 Color : Red_Black_Trees.Color_Type; 273 Element : Element_Type; 274 end record; 275 276 package Tree_Types is 277 new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type); 278 279 type Set (Capacity : Count_Type) is 280 new Tree_Types.Tree_Type (Capacity) with null record; 281 282 use Red_Black_Trees; 283 use Ada.Streams; 284 285 type Set_Access is access all Set; 286 for Set_Access'Storage_Size use 0; 287 288 type Cursor is record 289 Node : Count_Type; 290 end record; 291 292 procedure Write 293 (Stream : not null access Root_Stream_Type'Class; 294 Item : Cursor); 295 296 for Cursor'Write use Write; 297 298 procedure Read 299 (Stream : not null access Root_Stream_Type'Class; 300 Item : out Cursor); 301 302 for Cursor'Read use Read; 303 304 No_Element : constant Cursor := (Node => 0); 305 306 procedure Write 307 (Stream : not null access Root_Stream_Type'Class; 308 Container : Set); 309 310 for Set'Write use Write; 311 312 procedure Read 313 (Stream : not null access Root_Stream_Type'Class; 314 Container : out Set); 315 316 for Set'Read use Read; 317 318 Empty_Set : constant Set := (Capacity => 0, others => <>); 319 320end Ada.Containers.Formal_Ordered_Sets; 321