Resolve/C++ Catalog
AI/Unique_Id_Generator/Kernel.h
Copyright © 2010, Reusable Software Research Group, The Ohio State University

//  /*-------------------------------------------------------------------*\
//  |   Abstract Instance : Unique_Id_Generator_Kernel
//  \*-------------------------------------------------------------------*/

#ifndef AI_UNIQUE_ID_GENERATOR_KERNEL
#define AI_UNIQUE_ID_GENERATOR_KERNEL 1

///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

abstract_instance
class Unique_Id_Generator_Kernel
{
public:

    /*!		
	math subtype UNIQUE_ID_GENERATOR_MODEL is finite set of integer
            exemplar m
            constraint
                for all id: integer where (id is in m) (id >= 0)
    !*/

    standard_abstract_operations (Unique_Id_Generator_Kernel);
    /*!
	Unique_Id_Generator_Kernel is modeled by UNIQUE_ID_GENERATOR_MODEL
	initialization ensures
	    self = empty_set
    !*/

    procedure Generate (
	    produces Integer& id
	) is_abstract;
    /*!
	ensures
	    id is not in #self and
	    self = #self union {id}
    !*/
    
    procedure Reclaim (
	    preserves Integer id
	) is_abstract;
    /*!
	requires
	    id is in self
	ensures
	    self = #self - {id}
    !*/
    
    function Boolean Is_In_Use (
	    preserves Integer id
	) is_abstract;
    /*!
	ensures
	    Is_In_Use = id is in self
    !*/

    function Integer Size () is_abstract;
    /*!
	ensures
	    Size = |self|
    !*/
    
};

#endif // AI_UNIQUE_ID_GENERATOR_KERNEL