gcc/testsuite/gnat.dg/predicate8_pkg.ads

   1 pragma Spark_Mode (On);
   2
   3 generic
   4   type Element_Type is private;
   5
   6 package 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
  65 private
  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
  81 end Predicate8_Pkg;