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

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

#ifndef AI_TIMER_KERNEL
#define AI_TIMER_KERNEL 1

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

abstract_instance
class Timer_Kernel
{
public:

    /*!
	math subtype ELAPSED_TIME is integer
	    exemplar t
	    constraint
	        t >= 0

	math definition SYSTEM_CLOCK: ELAPSED_TIME is
	    [the number of milliseconds spent by the system executing
	     this program so far, i.e., user time + system time]
    !*/

    standard_abstract_operations (Timer_Kernel);
    /*!
        Timer_Kernel is modeled by ELAPSED_TIME
	// NOTE: Initialization ensures nothing in particular, i.e.,
	// the initial value of self is arbitrary!
    !*/

    procedure Restart () is_abstract;
    /*!
	ensures
	    self = SYSTEM_CLOCK
    !*/

    function Integer Reading () is_abstract;
    /*!
	ensures
	    Reading = SYSTEM_CLOCK - self
    !*/

};

#endif // AI_TIMER_KERNEL