1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- ADA.CONTAINERS.FUNCTIONAL_VECTORS -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2016-2020, 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 Index_Type is (<>); 37 -- To avoid Constraint_Error being raised at run time, Index_Type'Base 38 -- should have at least one more element at the low end than Index_Type. 39 40 type Element_Type (<>) is private; 41 with function "=" (Left, Right : Element_Type) return Boolean is <>; 42 43package Ada.Containers.Functional_Vectors with SPARK_Mode is 44 45 subtype Extended_Index is Index_Type'Base range 46 Index_Type'Pred (Index_Type'First) .. Index_Type'Last; 47 -- Index_Type with one more element at the low end of the range. 48 -- This type is never used but it forces GNATprove to check that there is 49 -- room for one more element at the low end of Index_Type. 50 51 type Sequence is private 52 with Default_Initial_Condition => Length (Sequence) = 0, 53 Iterable => (First => Iter_First, 54 Has_Element => Iter_Has_Element, 55 Next => Iter_Next, 56 Element => Get); 57 -- Sequences are empty when default initialized. 58 -- Quantification over sequences can be done using the regular 59 -- quantification over its range or directly on its elements with "for of". 60 61 ----------------------- 62 -- Basic operations -- 63 ----------------------- 64 65 -- Sequences are axiomatized using Length and Get, providing respectively 66 -- the length of a sequence and an accessor to its Nth element: 67 68 function Length (Container : Sequence) return Count_Type with 69 -- Length of a sequence 70 71 Global => null, 72 Post => 73 (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <= 74 Index_Type'Pos (Index_Type'Last); 75 76 function Get 77 (Container : Sequence; 78 Position : Extended_Index) return Element_Type 79 -- Access the Element at position Position in Container 80 81 with 82 Global => null, 83 Pre => Position in Index_Type'First .. Last (Container); 84 85 function Last (Container : Sequence) return Extended_Index with 86 -- Last index of a sequence 87 88 Global => null, 89 Post => 90 Last'Result = 91 Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) + 92 Length (Container)); 93 pragma Annotate (GNATprove, Inline_For_Proof, Last); 94 95 function First return Extended_Index is (Index_Type'First) with 96 Global => null; 97 -- First index of a sequence 98 99 ------------------------ 100 -- Property Functions -- 101 ------------------------ 102 103 function "=" (Left : Sequence; Right : Sequence) return Boolean with 104 -- Extensional equality over sequences 105 106 Global => null, 107 Post => 108 "="'Result = 109 (Length (Left) = Length (Right) 110 and then (for all N in Index_Type'First .. Last (Left) => 111 Get (Left, N) = Get (Right, N))); 112 pragma Annotate (GNATprove, Inline_For_Proof, "="); 113 114 function "<" (Left : Sequence; Right : Sequence) return Boolean with 115 -- Left is a strict subsequence of Right 116 117 Global => null, 118 Post => 119 "<"'Result = 120 (Length (Left) < Length (Right) 121 and then (for all N in Index_Type'First .. Last (Left) => 122 Get (Left, N) = Get (Right, N))); 123 pragma Annotate (GNATprove, Inline_For_Proof, "<"); 124 125 function "<=" (Left : Sequence; Right : Sequence) return Boolean with 126 -- Left is a subsequence of Right 127 128 Global => null, 129 Post => 130 "<="'Result = 131 (Length (Left) <= Length (Right) 132 and then (for all N in Index_Type'First .. Last (Left) => 133 Get (Left, N) = Get (Right, N))); 134 pragma Annotate (GNATprove, Inline_For_Proof, "<="); 135 136 function Contains 137 (Container : Sequence; 138 Fst : Index_Type; 139 Lst : Extended_Index; 140 Item : Element_Type) return Boolean 141 -- Returns True if Item occurs in the range from Fst to Lst of Container 142 143 with 144 Global => null, 145 Pre => Lst <= Last (Container), 146 Post => 147 Contains'Result = 148 (for some I in Fst .. Lst => Get (Container, I) = Item); 149 pragma Annotate (GNATprove, Inline_For_Proof, Contains); 150 151 function Constant_Range 152 (Container : Sequence; 153 Fst : Index_Type; 154 Lst : Extended_Index; 155 Item : Element_Type) return Boolean 156 -- Returns True if every element of the range from Fst to Lst of Container 157 -- is equal to Item. 158 159 with 160 Global => null, 161 Pre => Lst <= Last (Container), 162 Post => 163 Constant_Range'Result = 164 (for all I in Fst .. Lst => Get (Container, I) = Item); 165 pragma Annotate (GNATprove, Inline_For_Proof, Constant_Range); 166 167 function Equal_Except 168 (Left : Sequence; 169 Right : Sequence; 170 Position : Index_Type) return Boolean 171 -- Returns True is Left and Right are the same except at position Position 172 173 with 174 Global => null, 175 Pre => Position <= Last (Left), 176 Post => 177 Equal_Except'Result = 178 (Length (Left) = Length (Right) 179 and then (for all I in Index_Type'First .. Last (Left) => 180 (if I /= Position then Get (Left, I) = Get (Right, I)))); 181 pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except); 182 183 function Equal_Except 184 (Left : Sequence; 185 Right : Sequence; 186 X : Index_Type; 187 Y : Index_Type) return Boolean 188 -- Returns True is Left and Right are the same except at positions X and Y 189 190 with 191 Global => null, 192 Pre => X <= Last (Left) and Y <= Last (Left), 193 Post => 194 Equal_Except'Result = 195 (Length (Left) = Length (Right) 196 and then (for all I in Index_Type'First .. Last (Left) => 197 (if I /= X and I /= Y then 198 Get (Left, I) = Get (Right, I)))); 199 pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except); 200 201 function Range_Equal 202 (Left : Sequence; 203 Right : Sequence; 204 Fst : Index_Type; 205 Lst : Extended_Index) return Boolean 206 -- Returns True if the ranges from Fst to Lst contain the same elements in 207 -- Left and Right. 208 209 with 210 Global => null, 211 Pre => Lst <= Last (Left) and Lst <= Last (Right), 212 Post => 213 Range_Equal'Result = 214 (for all I in Fst .. Lst => Get (Left, I) = Get (Right, I)); 215 pragma Annotate (GNATprove, Inline_For_Proof, Range_Equal); 216 217 function Range_Shifted 218 (Left : Sequence; 219 Right : Sequence; 220 Fst : Index_Type; 221 Lst : Extended_Index; 222 Offset : Count_Type'Base) return Boolean 223 -- Returns True if the range from Fst to Lst in Left contains the same 224 -- elements as the range from Fst + Offset to Lst + Offset in Right. 225 226 with 227 Global => null, 228 Pre => 229 Lst <= Last (Left) 230 and then 231 (if Offset < 0 then 232 Index_Type'Pos (Index_Type'Base'First) - Offset <= 233 Index_Type'Pos (Index_Type'First)) 234 and then 235 (if Fst <= Lst then 236 Offset in 237 Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) .. 238 (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) - 239 Index_Type'Pos (Lst)), 240 Post => 241 Range_Shifted'Result = 242 ((for all I in Fst .. Lst => 243 Get (Left, I) = 244 Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset))) 245 and 246 (for all I in Index_Type'Val (Index_Type'Pos (Fst) + Offset) .. 247 Index_Type'Val (Index_Type'Pos (Lst) + Offset) 248 => 249 Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset)) = 250 Get (Right, I))); 251 pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted); 252 253 ---------------------------- 254 -- Construction Functions -- 255 ---------------------------- 256 257 -- For better efficiency of both proofs and execution, avoid using 258 -- construction functions in annotations and rather use property functions. 259 260 function Set 261 (Container : Sequence; 262 Position : Index_Type; 263 New_Item : Element_Type) return Sequence 264 -- Returns a new sequence which contains the same elements as Container 265 -- except for the one at position Position which is replaced by New_Item. 266 267 with 268 Global => null, 269 Pre => Position in Index_Type'First .. Last (Container), 270 Post => 271 Get (Set'Result, Position) = New_Item 272 and then Equal_Except (Container, Set'Result, Position); 273 274 function Add (Container : Sequence; New_Item : Element_Type) return Sequence 275 -- Returns a new sequence which contains the same elements as Container 276 -- plus New_Item at the end. 277 278 with 279 Global => null, 280 Pre => 281 Length (Container) < Count_Type'Last 282 and then Last (Container) < Index_Type'Last, 283 Post => 284 Length (Add'Result) = Length (Container) + 1 285 and then Get (Add'Result, Last (Add'Result)) = New_Item 286 and then Container <= Add'Result; 287 288 function Add 289 (Container : Sequence; 290 Position : Index_Type; 291 New_Item : Element_Type) return Sequence 292 with 293 -- Returns a new sequence which contains the same elements as Container 294 -- except that New_Item has been inserted at position Position. 295 296 Global => null, 297 Pre => 298 Length (Container) < Count_Type'Last 299 and then Last (Container) < Index_Type'Last 300 and then Position <= Extended_Index'Succ (Last (Container)), 301 Post => 302 Length (Add'Result) = Length (Container) + 1 303 and then Get (Add'Result, Position) = New_Item 304 and then Range_Equal 305 (Left => Container, 306 Right => Add'Result, 307 Fst => Index_Type'First, 308 Lst => Index_Type'Pred (Position)) 309 and then Range_Shifted 310 (Left => Container, 311 Right => Add'Result, 312 Fst => Position, 313 Lst => Last (Container), 314 Offset => 1); 315 316 function Remove 317 (Container : Sequence; 318 Position : Index_Type) return Sequence 319 -- Returns a new sequence which contains the same elements as Container 320 -- except that the element at position Position has been removed. 321 322 with 323 Global => null, 324 Pre => Position in Index_Type'First .. Last (Container), 325 Post => 326 Length (Remove'Result) = Length (Container) - 1 327 and then Range_Equal 328 (Left => Container, 329 Right => Remove'Result, 330 Fst => Index_Type'First, 331 Lst => Index_Type'Pred (Position)) 332 and then Range_Shifted 333 (Left => Remove'Result, 334 Right => Container, 335 Fst => Position, 336 Lst => Last (Remove'Result), 337 Offset => 1); 338 339 --------------------------- 340 -- Iteration Primitives -- 341 --------------------------- 342 343 function Iter_First (Container : Sequence) return Extended_Index with 344 Global => null; 345 346 function Iter_Has_Element 347 (Container : Sequence; 348 Position : Extended_Index) return Boolean 349 with 350 Global => null, 351 Post => 352 Iter_Has_Element'Result = 353 (Position in Index_Type'First .. Last (Container)); 354 pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element); 355 356 function Iter_Next 357 (Container : Sequence; 358 Position : Extended_Index) return Extended_Index 359 with 360 Global => null, 361 Pre => Iter_Has_Element (Container, Position); 362 363private 364 365 pragma SPARK_Mode (Off); 366 367 package Containers is new Ada.Containers.Functional_Base 368 (Index_Type => Index_Type, 369 Element_Type => Element_Type); 370 371 type Sequence is record 372 Content : Containers.Container; 373 end record; 374 375 function Iter_First (Container : Sequence) return Extended_Index is 376 (Index_Type'First); 377 378 function Iter_Next 379 (Container : Sequence; 380 Position : Extended_Index) return Extended_Index 381 is 382 (if Position = Extended_Index'Last then 383 Extended_Index'First 384 else 385 Extended_Index'Succ (Position)); 386 387 function Iter_Has_Element 388 (Container : Sequence; 389 Position : Extended_Index) return Boolean 390 is 391 (Position in Index_Type'First .. 392 (Index_Type'Val 393 ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container)))); 394 395end Ada.Containers.Functional_Vectors; 396