1pragma Spark_Mode (On);
2
3generic
4  type Element_Type is private;
5
6package Predicate8_Pkg is
7   pragma Annotate (GNATprove, Terminating, Predicate8_Pkg);
8
9   subtype Small_Natural  is Natural range 0 .. Natural'Last / 2;
10   subtype Small_Positive is Natural range 1 .. Natural'Last / 2;
11
12   type Element_Array_Type is array (Small_Positive range <>) of Element_Type;
13
14   type Ring_Buffer_Type (Max_Size : Small_Positive) is private
15     with Default_Initial_Condition => Empty (Ring_Buffer_Type);
16
17   function Empty
18     (Buffer : in Ring_Buffer_Type) return Boolean;
19
20   function Full
21     (Buffer : in Ring_Buffer_Type) return Boolean;
22
23   function Size
24     (Buffer : in Ring_Buffer_Type) return Natural;
25
26   function Free
27     (Buffer : in Ring_Buffer_Type) return Natural;
28
29   function First
30     (Buffer : in Ring_Buffer_Type) return Element_Type
31   with
32     Pre => not Empty (Buffer);
33
34   function Last
35     (Buffer : in Ring_Buffer_Type) return Element_Type
36   with
37     Pre => not Empty (Buffer);
38
39   procedure Get
40     (Buffer   : in out Ring_Buffer_Type;
41      Element  :    out Element_Type)
42   with
43     Pre   => not Empty (Buffer) and
44              Size (Buffer) >= 1,
45     Post  => not Full (Buffer) and then
46              Element = First (Buffer'Old) and then
47              Size (Buffer) = Size (Buffer'Old) - 1;
48
49   procedure Put
50     (Buffer   : in out Ring_Buffer_Type;
51      Element  : in     Element_Type)
52   with
53     Pre   => not Full (Buffer),
54     Post  => not Empty (Buffer) and then
55              Last (Buffer) = Element and then
56              Size (Buffer) = Size (Buffer'Old) + 1;
57
58   procedure Clear
59     (Buffer : in out Ring_Buffer_Type)
60   with
61     Post => Empty (Buffer) and then
62             not Full (Buffer) and then
63             Size (Buffer) = 0;
64
65private
66   type Ring_Buffer_Type (Max_Size : Small_Positive) is record
67      Count : Small_Natural  := 0;
68      Head  : Small_Positive := 1;
69      Tail  : Small_Positive := Max_Size;
70      Items : Element_Array_Type (1 .. Max_Size);
71   end record
72     with Dynamic_Predicate =>
73       (Max_Size <= Small_Positive'Last and
74        Count    <= Max_Size and
75        Head     <= Max_Size and
76        Tail     <= Max_Size and
77        ((Count = 0 and Tail = Max_Size and Head = 1) or
78         (Count = Max_Size + Tail - Head + 1) or
79         (Count = Tail - Head + 1)));
80
81end Predicate8_Pkg;
82