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 _ V E C T O R S -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2004-2015, 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_Vectors in the Ada 33-- 2012 RM. The modifications are meant to facilitate formal proofs by making 34-- it easier to express properties, and by making the specification of this 35-- unit compatible with SPARK 2014. Note that the API of this unit may be 36-- subject to incompatible changes as SPARK 2014 evolves. 37 38generic 39 type Index_Type is range <>; 40 type Element_Type is private; 41 42 with function "=" (Left, Right : Element_Type) return Boolean is <>; 43 44 Bounded : Boolean := True; 45 -- If True, the containers are bounded; the initial capacity is the maximum 46 -- size, and heap allocation will be avoided. If False, the containers can 47 -- grow via heap allocation. 48 49package Ada.Containers.Formal_Vectors with 50 SPARK_Mode 51is 52 pragma Annotate (GNATprove, External_Axiomatization); 53 pragma Annotate (CodePeer, Skip_Analysis); 54 55 subtype Extended_Index is Index_Type'Base 56 range Index_Type'First - 1 .. 57 Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; 58 59 No_Index : constant Extended_Index := Extended_Index'First; 60 61 subtype Capacity_Range is 62 Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1); 63 64 type Vector (Capacity : Capacity_Range) is limited private with 65 Default_Initial_Condition => Is_Empty (Vector); 66 -- In the bounded case, Capacity is the capacity of the container, which 67 -- never changes. In the unbounded case, Capacity is the initial capacity 68 -- of the container, and operations such as Reserve_Capacity and Append can 69 -- increase the capacity. The capacity never shrinks, except in the case of 70 -- Clear. 71 -- 72 -- Note that all objects of type Vector are constrained, including in the 73 -- unbounded case; you can't assign from one object to another if the 74 -- Capacity is different. 75 76 function Empty_Vector return Vector; 77 78 function "=" (Left, Right : Vector) return Boolean with 79 Global => null; 80 81 function To_Vector 82 (New_Item : Element_Type; 83 Length : Capacity_Range) return Vector 84 with 85 Global => null; 86 87 function Capacity (Container : Vector) return Capacity_Range with 88 Global => null, 89 Post => Capacity'Result >= Container.Capacity; 90 91 procedure Reserve_Capacity 92 (Container : in out Vector; 93 Capacity : Capacity_Range) 94 with 95 Global => null, 96 Pre => (if Bounded then Capacity <= Container.Capacity); 97 98 function Length (Container : Vector) return Capacity_Range with 99 Global => null; 100 101 function Is_Empty (Container : Vector) return Boolean with 102 Global => null; 103 104 procedure Clear (Container : in out Vector) with 105 Global => null; 106 -- Note that this reclaims storage in the unbounded case. You need to call 107 -- this before a container goes out of scope in order to avoid storage 108 -- leaks. In addition, "X := ..." can leak unless you Clear(X) first. 109 110 procedure Assign (Target : in out Vector; Source : Vector) with 111 Global => null, 112 Pre => (if Bounded then Length (Source) <= Target.Capacity); 113 114 function Copy 115 (Source : Vector; 116 Capacity : Capacity_Range := 0) return Vector 117 with 118 Global => null, 119 Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)); 120 121 function Element 122 (Container : Vector; 123 Index : Index_Type) return Element_Type 124 with 125 Global => null, 126 Pre => Index in First_Index (Container) .. Last_Index (Container); 127 128 procedure Replace_Element 129 (Container : in out Vector; 130 Index : Index_Type; 131 New_Item : Element_Type) 132 with 133 Global => null, 134 Pre => Index in First_Index (Container) .. Last_Index (Container); 135 136 procedure Append 137 (Container : in out Vector; 138 New_Item : Vector) 139 with 140 Global => null, 141 Pre => (if Bounded then 142 Length (Container) + Length (New_Item) <= Container.Capacity); 143 144 procedure Append 145 (Container : in out Vector; 146 New_Item : Element_Type) 147 with 148 Global => null, 149 Pre => (if Bounded then 150 Length (Container) < Container.Capacity); 151 152 procedure Delete_Last 153 (Container : in out Vector) 154 with 155 Global => null; 156 157 procedure Reverse_Elements (Container : in out Vector) with 158 Global => null; 159 160 procedure Swap (Container : in out Vector; I, J : Index_Type) with 161 Global => null, 162 Pre => I in First_Index (Container) .. Last_Index (Container) 163 and then J in First_Index (Container) .. Last_Index (Container); 164 165 function First_Index (Container : Vector) return Index_Type with 166 Global => null; 167 168 function First_Element (Container : Vector) return Element_Type with 169 Global => null, 170 Pre => not Is_Empty (Container); 171 172 function Last_Index (Container : Vector) return Extended_Index with 173 Global => null; 174 175 function Last_Element (Container : Vector) return Element_Type with 176 Global => null, 177 Pre => not Is_Empty (Container); 178 179 function Find_Index 180 (Container : Vector; 181 Item : Element_Type; 182 Index : Index_Type := Index_Type'First) return Extended_Index 183 with 184 Global => null; 185 186 function Reverse_Find_Index 187 (Container : Vector; 188 Item : Element_Type; 189 Index : Index_Type := Index_Type'Last) return Extended_Index 190 with 191 Global => null; 192 193 function Contains 194 (Container : Vector; 195 Item : Element_Type) return Boolean 196 with 197 Global => null; 198 199 function Has_Element 200 (Container : Vector; 201 Position : Extended_Index) return Boolean 202 with 203 Global => null; 204 205 generic 206 with function "<" (Left, Right : Element_Type) return Boolean is <>; 207 package Generic_Sorting with SPARK_Mode is 208 209 function Is_Sorted (Container : Vector) return Boolean with 210 Global => null; 211 212 procedure Sort (Container : in out Vector) with 213 Global => null; 214 215 end Generic_Sorting; 216 217 function First_To_Previous 218 (Container : Vector; 219 Current : Index_Type) return Vector 220 with 221 Ghost, 222 Global => null, 223 Pre => Current in First_Index (Container) .. Last_Index (Container); 224 225 function Current_To_Last 226 (Container : Vector; 227 Current : Index_Type) return Vector 228 with 229 Ghost, 230 Global => null, 231 Pre => Current in First_Index (Container) .. Last_Index (Container); 232 -- First_To_Previous returns a container containing all elements preceding 233 -- Current (excluded) in Container. Current_To_Last returns a container 234 -- containing all elements following Current (included) in Container. 235 -- These two new functions can be used to express invariant properties in 236 -- loops which iterate over containers. First_To_Previous returns the part 237 -- of the container already scanned and Current_To_Last the part not 238 -- scanned yet. 239 240private 241 pragma SPARK_Mode (Off); 242 243 pragma Inline (First_Index); 244 pragma Inline (Last_Index); 245 pragma Inline (Element); 246 pragma Inline (First_Element); 247 pragma Inline (Last_Element); 248 pragma Inline (Replace_Element); 249 pragma Inline (Contains); 250 251 subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last; 252 type Elements_Array is array (Array_Index range <>) of Element_Type; 253 function "=" (L, R : Elements_Array) return Boolean is abstract; 254 255 type Elements_Array_Ptr is access all Elements_Array; 256 257 type Vector (Capacity : Capacity_Range) is limited record 258 -- In the bounded case, the elements are stored in Elements. In the 259 -- unbounded case, the elements are initially stored in Elements, until 260 -- we run out of room, then we switch to Elements_Ptr. 261 Last : Extended_Index := No_Index; 262 Elements_Ptr : Elements_Array_Ptr := null; 263 Elements : aliased Elements_Array (1 .. Capacity); 264 end record; 265 266 -- The primary reason Vector is limited is that in the unbounded case, once 267 -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will 268 -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr, 269 -- so for example "Append (X, ...);" will modify BOTH X and Y. That would 270 -- allow SPARK to "prove" things that are false. We could fix that by 271 -- making Vector a controlled type, and override Adjust to make a deep 272 -- copy, but finalization is not allowed in SPARK. 273 -- 274 -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not 275 -- allowed on Vectors. 276 277 function Empty_Vector return Vector is 278 ((Capacity => 0, others => <>)); 279 280end Ada.Containers.Formal_Vectors; 281