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

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

#ifndef AI_NATURAL_KERNEL
#define AI_NATURAL_KERNEL 1

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

abstract_instance
class Natural_Kernel
{
public:

    /*!
	math subtype NATURAL_MODEL is integer
	    exemplar n
	    constraint
	        n >= 0
		
	math definition RADIX: integer satisfies restriction
            RADIX >= 2
    !*/
    
    standard_abstract_operations (Natural_Kernel);
    /*!
	Natural_Kernel is modeled by NATURAL_MODEL
	initialization ensures
	    self = 0
    !*/
    
    procedure Multiply_By_Radix (
	    preserves Integer k
	) is_abstract;
    /*!
	requires
	    0 <= k < RADIX
	ensures
	    self = #self * RADIX + k
    !*/

    procedure Divide_By_Radix (
	    produces Integer& k
	) is_abstract;
    /*!
	ensures
	    #self = self * RADIX + k  and
	    0 <= k < RADIX
    !*/

    function Integer Discrete_Log () is_abstract;
    /*!
	ensures
	    if self = 0
	    then Discrete_Log = 0
	    else RADIX^(Discrete_Log - 1) <= self < RADIX^(Discrete_Log)
    !*/

    function Integer Radix () is_abstract;
    /*!
	ensures
            Radix = RADIX
    !*/
    
};

#endif // AI_NATURAL_KERNEL