Re: getting started with Spark; generic queue package

[Stephen Leake <stephen_leake@stephe-leake.org>]

Just for completeness, posting the final version of the package that allows Spark to prove all the contract conditions.

--  Abstract:
--
--  A generic queue, allowing definite non-limited item types.
--
--  Copyright (C) 2004, 2008, 2009, 2011, 2017, 2019 Stephen Leake.  All Rights Reserved.
--
--  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 Item_Type is private;
   Max_Size : in Integer := 100;
package SAL.Gen_Bounded_Definite_Queues
  with Spark_Mode
is
   pragma Pure;

   subtype Size_Type is Integer range 1 .. Max_Size with
     Dynamic_Predicate => Max_Size in 1 .. Integer'Last / 2 - 1;
   --  We need to be able to say Head + N in expressions.

   type Queue_Type (Size : Size_Type) is tagged private;
   --  Size is maximum number of items in the queue.
   --  Tagged to allow Object.Method syntax.

   procedure Clear (Queue : in out Queue_Type)
   with Post => Queue.Count = 0;
   --  Empty Queue of all items.

   function Count (Queue : in Queue_Type) return Natural;
   --  Returns count of items in the Queue

   function Is_Empty (Queue : in Queue_Type) return Boolean
   with Post => (if Is_Empty'Result then Queue.Count = 0);
   --  Returns true if no items are in Queue.

   function Is_Full (Queue : in Queue_Type) return Boolean
   with Post => (if Is_Full'Result then Queue.Count = Queue.Size);
   --  Returns true if Queue is full.

   procedure Remove (Queue : in out Queue_Type; Item : out Item_Type) with
     Pre'Class => Queue.Count > 0,
     Post      => Queue.Count = Queue'Old.Count - 1;
   --  Remove head item from Queue, return it.
   --
   --  Raises Container_Empty if Is_Empty.

   function Remove (Queue : in out Queue_Type) return Item_Type with
     Spark_Mode => Off;

   procedure Drop (Queue : in out Queue_Type) with
     Pre'Class => Queue.Count > 0,
     Post      => Queue.Count = Queue'Old.Count - 1;
   --  Remove head item from Queue, discard it.
   --
   --  Raises Container_Empty if Is_Empty.

   function Peek (Queue : in Queue_Type; N : Integer := 0) return Item_Type with
     Pre'Class => Queue.Count > 0 and
                  N in 0 .. Queue.Count - 1;
   --  Return a copy of a queue item, without removing it. N = 0 is
   --  the queue head.

   procedure Add (Queue : in out Queue_Type; Item : in Item_Type) with
     Pre'Class => Queue.Count < Queue.Size;
   --  Add Item to the tail of Queue.

   procedure Add_To_Head (Queue : in out Queue_Type; Item : in Item_Type) with
     Pre'Class => Queue.Count < Queue.Size;
   --  Add Item to the head of Queue.

private

   type Item_Array_Type is array (Positive range <>) of Item_Type;

   type Queue_Type (Size : Size_Type) is tagged
   record
      Head       : Integer := 1;
      Tail       : Integer := 1;
      Item_Count : Integer := 0; -- not 'Count' to distinguish from the function
      Data       : Item_Array_Type (1 .. Size);
      --  Add at Tail + 1, remove at Head. Item_Count is current count;
      --  easier to keep track of that than to compute Is_Empty for
      --  each Add and Remove.
      --
      --  Empty is indicated by Item_Count = 0; head and tail are arbitrary
      --  in that case.
   end record with
     Dynamic_Predicate =>
       Head in 1 .. Size and
       Tail in 1 .. Size and
       Item_Count in 0 .. Size;

   function Count (Queue : in Queue_Type) return Natural is (Queue.Item_Count);

end SAL.Gen_Bounded_Definite_Queues;

--  Abstract:
--
--  See spec.
--
--  Copyright (C) 2004, 2008, 2009, 2011, 2017, 2019 Stephen Leake.  All Rights Reserved.
--
--  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);

package body SAL.Gen_Bounded_Definite_Queues
  with Spark_Mode
is

   --  Local subprograms

   function Wrap (Queue : in Queue_Type; I : in Integer) return Integer with
     Pre  => I in 0 .. (Queue.Size - 1) + Queue.Size,
     Post => Wrap'Result in 1 .. Queue.Size
   is begin
      if I > Queue.Size then
         return I - Queue.Size;
      elsif I < 1 then
         return Queue.Size + I;
      else
         return I;
      end if;
   end Wrap;

   ----------
   --  Public subprograms

   procedure Clear (Queue : in out Queue_Type) is
   begin
      Queue.Item_Count := 0;
   end Clear;

   function Is_Empty (Queue : in Queue_Type) return Boolean is
   begin
      return Queue.Item_Count = 0;
   end Is_Empty;

   function Is_Full (Queue : in Queue_Type) return Boolean is
   begin
      return Queue.Item_Count = Queue.Size;
   end Is_Full;

   procedure Remove (Queue : in out Queue_Type; Item : out Item_Type)
   is begin
      Item := Queue.Data (Queue.Head);

      Queue.Item_Count := Queue.Item_Count - 1;

      if Queue.Item_Count > 0 then
         Queue.Head := Wrap (Queue, Queue.Head + 1);
      end if;
   end Remove;

   function Remove (Queue : in out Queue_Type) return Item_Type with
     Spark_Mode => Off
   is begin
      return Item : Item_Type  do
         Remove (Queue, Item);
      end return;
   end Remove;

   procedure Drop (Queue : in out Queue_Type)
   is begin
      Queue.Item_Count := Queue.Item_Count - 1;

      if Queue.Item_Count > 0 then
         Queue.Head := Wrap (Queue, Queue.Head + 1);
      end if;
   end Drop;

   function Peek (Queue : in Queue_Type; N : Integer := 0) return Item_Type
   is begin
      return Queue.Data (Wrap (Queue, Queue.Head + N));
   end Peek;

   procedure Add (Queue : in out Queue_Type; Item : in Item_Type) is
   begin
      if Queue.Item_Count = 0 then
         Queue.Tail       := 1;
         Queue.Head       := 1;
         Queue.Item_Count := 1;
         Queue.Data (1)   := Item;
      else
         Queue.Tail              := Wrap (Queue, Queue.Tail + 1);
         Queue.Data (Queue.Tail) := Item;
         Queue.Item_Count        := Queue.Item_Count + 1;
      end if;
   end Add;

   procedure Add_To_Head (Queue : in out Queue_Type; Item : in Item_Type) is
   begin
      if Queue.Item_Count = 0 then
         Queue.Tail       := 1;
         Queue.Head       := 1;
         Queue.Item_Count := 1;
         Queue.Data (1)   := Item;
      else
         Queue.Head              := Wrap (Queue, Queue.Head - 1);
         Queue.Data (Queue.Head) := Item;
         Queue.Item_Count        := Queue.Item_Count + 1;
      end if;
   end Add_To_Head;

end SAL.Gen_Bounded_Definite_Queues;