1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164 | -- Abstract :
--
-- A simple bounded vector of definite items, in Spark.
--
-- Copyright (C) 2017 - 2020 Free Software Foundation, Inc.
--
-- This library is free software; you can redistribute it and/or modify it
-- under terms of the GNU General Public License as published by the Free
-- Software Foundation; either version 3, or (at your option) any later
-- version. This library is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHAN-
-- TABILITY 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.
pragma License (Modified_GPL);
generic
type Index_Type is range <>;
type Element_Type is private;
Default_Element : in Element_Type;
-- Only used in Empty_Vector
Capacity : in Ada.Containers.Count_Type;
package SAL.Gen_Bounded_Definite_Vectors
with Spark_Mode
is
use all type Ada.Containers.Count_Type;
subtype Extended_Index is Index_Type'Base
range Index_Type'First - 1 ..
Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
pragma Assert (Capacity <= Ada.Containers.Count_Type (Index_Type'Last - Index_Type'First + 1));
No_Index : constant Extended_Index := Extended_Index'First;
type Vector is private with
Default_Initial_Condition => Length (Vector) = 0;
-- Not 'tagged' because SPARK in Gnat Community 2019 does not support
-- type invariant on tagged type.
Empty_Vector : constant Vector;
function Length (Container : in Vector) return Ada.Containers.Count_Type with
Post => Length'Result in 0 .. Capacity;
function Is_Full (Container : in Vector) return Boolean with
Post => Is_Full'Result = (Length (Container) = Capacity);
function Has_Space (Container : in Vector; Item_Count : in Ada.Containers.Count_Type) return Boolean
is (Length (Container) + Item_Count <= Capacity)
with Pre => Item_Count <= Ada.Containers.Count_Type'Last - Length (Container);
procedure Clear (Container : in out Vector) with
Post => Length (Container) = 0;
function First_Index (Container : in Vector) return Index_Type is (Index_Type'First) with
Depends => (First_Index'Result => null, null => Container);
function Last_Index (Container : in Vector) return Extended_Index;
-- No_Index when Container is empty.
function Element (Container : in Vector; Index : in Index_Type) return Element_Type
with Pre => Index <= Last_Index (Container);
-- Index of first element in Vector is Index_Type'First.
procedure Replace_Element
(Container : in out Vector;
Index : in Index_Type;
New_Item : in Element_Type)
with
Pre => Index <= Last_Index (Container),
Post => Element (Container, Index) = New_Item;
-- Index of first element in Vector is Index_Type'First.
function To_Vector (Element : in Element_Type) return Vector with
Post => Length (To_Vector'Result) = 1;
procedure Append (Container : in out Vector; New_Item : in Element_Type) with
Pre => Length (Container) < Capacity,
Post => Length (Container) = Length (Container'Old) + 1 and
Element (Container, Last_Index (Container)) = New_Item and
(for all I in Index_Type'First .. Last_Index (Container) - 1 =>
Element (Container'Old, I) = Element (Container, I));
procedure Prepend (Container : in out Vector; New_Item : in Element_Type) with
Pre => Length (Container) < Capacity,
Post => Length (Container) = Length (Container'Old) + 1 and then
(Element (Container, Index_Type'First) = New_Item and
(for all I in Index_Type'First .. Last_Index (Container'Old) =>
Element (Container'Old, I) = Element (Container, I + 1)));
-- Insert New_Item at beginning of Container; current elements slide right.
procedure Insert
(Container : in out Vector;
New_Item : in Element_Type;
Before : in Extended_Index) with
Pre => Length (Container) < Capacity and Before <= Last_Index (Container),
Contract_Cases =>
(Before = No_Index =>
Length (Container) = Length (Container'Old) + 1 and
Element (Container, Last_Index (Container)) = New_Item and
(for all I in Index_Type'First .. Last_Index (Container) - 1 =>
Element (Container'Old, I) = Element (Container, I)),
Before /= No_Index =>
Length (Container) = Length (Container'Old) + 1 and
Element (Container, Before) = New_Item and
(for all I in Index_Type'First .. Before - 1 =>
Element (Container'Old, I) = Element (Container, I)) and
(for all I in Before + 1 .. Last_Index (Container) =>
Element (Container'Old, I - 1) = Element (Container, I)));
-- Insert New_Item before Before, or after Last_Index if Before is
-- No_Index. Current elements at Before and after slide right.
-- New_Item then has index Before.
function "+" (Item : in Element_Type) return Vector with
Post => Length ("+"'Result) = 1 and
Element ("+"'Result, Index_Type'First) = Item;
function "&" (Left : in Vector; Right : in Element_Type) return Vector with
Pre => Length (Left) < Capacity,
Post => Length ("&"'Result) = Length (Left) + 1 and
(for all I in Index_Type'First .. Last_Index (Left) => Element (Left, I) = Element ("&"'Result, I)) and
Element ("&"'Result, Last_Index ("&"'Result)) = Right;
procedure Delete_First (Container : in out Vector; Count : in Ada.Containers.Count_Type := 1) with
Pre => Length (Container) >= Count,
Post => Length (Container) = Length (Container)'Old - Count and then
(for all I in Index_Type'First .. Last_Index (Container) =>
Element (Container'Old, Index_Type (Integer (I) + Integer (Count))) = Element (Container, I));
-- Remaining elements slide down.
procedure Delete_Last (Container : in out Vector; Count : in Ada.Containers.Count_Type := 1) with
Pre => Length (Container) >= Count,
Post => Length (Container) = Length (Container)'Old - Count and then
(for all I in Index_Type'First .. Last_Index (Container) =>
Element (Container'Old, I) = Element (Container, I));
private
type Array_Type is array (Peek_Type range 1 .. Peek_Type (Capacity)) of aliased Element_Type;
function To_Peek_Index (Index : in Extended_Index) return Base_Peek_Type is
(Base_Peek_Type (Index - Index_Type'First + 1));
type Vector is
record
Elements : Array_Type;
Last : Extended_Index := No_Index;
end record with
Type_Invariant => To_Peek_Index (Last) <= Elements'Last;
pragma Annotate (GNATprove, Intentional, "type ""Vector"" is not fully initialized",
"Only items in Elements with index < Last are accessed");
-- We require Default_Element for this because SPARK in GNAT Community 2019 doesn't
-- support <> here.
Empty_Vector : constant Vector :=
(Last => No_Index,
Elements => (others => Default_Element));
end SAL.Gen_Bounded_Definite_Vectors;
|