---------------------------------------------------------------------------
-- FILE    : serial_generator.ads
-- SUBJECT : Specification of a package to abstract the serial number generator.
-- AUTHOR  : (C) Copyright 2015 by Peter Chapin
--
-- Serial numbers are required to be unique over the lifetime of the system's deployment.
--
-- Please send comments or bug reports to
--
--      Peter Chapin <PChapin@vtc.vsc.edu>
---------------------------------------------------------------------------
pragma SPARK_Mode(On);
with Ada.Calendar;
pragma Elaborate_All (Ada.Calendar);

package Serial_Generator
  with
     Abstract_State => State,
     Initializes => (State => Ada.Calendar.Clock_Time)
is
   type Serial_Number_Type is mod 2**64;

   -- Computes the next serial number and updates the internal state to prepare for a following
   -- call to Next. This procedure can't fail. However, the numbers it generates cycle with a
   -- period of 2**64.
   --
   procedure Next(Number : out Serial_Number_Type)
     with
        Global => (In_Out => State),
        Depends => ((State, Number) => State);

end Serial_Generator;