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

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

#ifndef AI_RANDOM_KERNEL
#define AI_RANDOM_KERNEL 1

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

abstract_instance
class Random_Kernel
{
public:

    /*!
	math definition LIMIT: integer satisfies restriction
	    0 < LIMIT <= MAXIMUM_INTEGER

	math subtype RANDOM_MODEL is integer
	    exemplar rn
	    constraint
		0 <= rn < LIMIT
		
	math definition NEXT (
		n: RANDOM_MODEL
	    ): RANDOM_MODEL satisfies restriction
	    [successive application of NEXT starting with n
	     (i.e., NEXT(n), NEXT(NEXT(n)), and so forth)
	     produces a sequence of pseudo-random numbers]
    !*/

    standard_abstract_operations (Random_Kernel);
    /*!
	Random_Kernel is modeled by RANDOM_MODEL
	initialization ensures
            self = 0
    !*/

    procedure Set_Value (
	    preserves Integer n
	) is_abstract;
    /*!
	ensures
	    self = n mod LIMIT
    !*/

    function Integer Value () is_abstract;
    /*!
	ensures
	    Value = self
    !*/

    procedure Generate_Next() is_abstract;
    /*!
	ensures
	    self = NEXT (#self)
    !*/

    function Integer Limit () is_abstract;
    /*!
	ensures
	    Limit = LIMIT
    !*/

};

#endif // AI_RANDOM_KERNEL