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