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

//  /*-------------------------------------------------------------------*\
//  |   Abstract Template : Natural_Arithmetic
//  \*-------------------------------------------------------------------*/

#ifndef AT_NATURAL_ARITHMETIC
#define AT_NATURAL_ARITHMETIC 1

///------------------------------------------------------------------------
/// Global Context --------------------------------------------------------
///------------------------------------------------------------------------

#include "AI/Natural/Kernel.h"

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

abstract_template <
        concrete_instance class T
	/*!
	    implements
		abstract_instance Natural_Kernel
	!*/
    >
class Natural_Arithmetic :
    extends
        abstract_instance Natural_Kernel
{
public:
    
    procedure Convert_From_Integer (
	    preserves Integer i
	) is_abstract;
    /*!
	produces self
	requires
	    i >= 0
	ensures
	    self = i
    !*/

    procedure Increment () is_abstract;
    /*!
	ensures
	    self = #self + 1
    !*/

    procedure Decrement () is_abstract;
    /*!
        requires
	    self > 0
	ensures
	    self = #self - 1
    !*/

    function Integer Compare (
	    preserves T& n
	) is_abstract;
    /*!
        ensures
	    if self < n
	    then Compare = -1
	    else if self = n
	         then Compare = 0
		 else Compare = 1
    !*/
    
    procedure Add (
	    preserves T& n
	) is_abstract;
    /*!
	ensures
	    self = #self + n
    !*/

    procedure Subtract (
	    preserves T& n
	) is_abstract;
    /*!
	requires
	    self >= n
	ensures
	    self = #self - n
    !*/

    procedure Multiply (
	    preserves T& n
	) is_abstract;
    /*!
	ensures
	    self = #self * n
    !*/

    procedure Divide (
	    preserves T& n,
	    produces T& rem
	) is_abstract;
    /*!
	requires
	    n > 0
	ensures
	    #self = self * n + rem  and
	    0 <= rem < n
    !*/

};

#endif // AT_NATURAL_ARITHMETIC