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
|
pragma Spark_Mode (On);
generic
type Element_Type is private;
package Predicate8_Pkg is
pragma Annotate (GNATprove, Terminating, Predicate8_Pkg);
subtype Small_Natural is Natural range 0 .. Natural'Last / 2;
subtype Small_Positive is Natural range 1 .. Natural'Last / 2;
type Element_Array_Type is array (Small_Positive range <>) of Element_Type;
type Ring_Buffer_Type (Max_Size : Small_Positive) is private
with Default_Initial_Condition => Empty (Ring_Buffer_Type);
function Empty
(Buffer : in Ring_Buffer_Type) return Boolean;
function Full
(Buffer : in Ring_Buffer_Type) return Boolean;
function Size
(Buffer : in Ring_Buffer_Type) return Natural;
function Free
(Buffer : in Ring_Buffer_Type) return Natural;
function First
(Buffer : in Ring_Buffer_Type) return Element_Type
with
Pre => not Empty (Buffer);
function Last
(Buffer : in Ring_Buffer_Type) return Element_Type
with
Pre => not Empty (Buffer);
procedure Get
(Buffer : in out Ring_Buffer_Type;
Element : out Element_Type)
with
Pre => not Empty (Buffer) and
Size (Buffer) >= 1,
Post => not Full (Buffer) and then
Element = First (Buffer'Old) and then
Size (Buffer) = Size (Buffer'Old) - 1;
procedure Put
(Buffer : in out Ring_Buffer_Type;
Element : in Element_Type)
with
Pre => not Full (Buffer),
Post => not Empty (Buffer) and then
Last (Buffer) = Element and then
Size (Buffer) = Size (Buffer'Old) + 1;
procedure Clear
(Buffer : in out Ring_Buffer_Type)
with
Post => Empty (Buffer) and then
not Full (Buffer) and then
Size (Buffer) = 0;
private
type Ring_Buffer_Type (Max_Size : Small_Positive) is record
Count : Small_Natural := 0;
Head : Small_Positive := 1;
Tail : Small_Positive := Max_Size;
Items : Element_Array_Type (1 .. Max_Size);
end record
with Dynamic_Predicate =>
(Max_Size <= Small_Positive'Last and
Count <= Max_Size and
Head <= Max_Size and
Tail <= Max_Size and
((Count = 0 and Tail = Max_Size and Head = 1) or
(Count = Max_Size + Tail - Head + 1) or
(Count = Tail - Head + 1)));
end Predicate8_Pkg;
|
