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

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

#ifndef AT_GENERAL_ARE_IN_ORDER
#define AT_GENERAL_ARE_IN_ORDER 1

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

abstract_template <
	concrete_instance class T
    >
utility_class General_Are_In_Order
{
public:

    /*!
	math definition ARE_IN_ORDER (
		x: T,
		y: T
	    ): boolean satisfies restriction
	    for all x, y, z: T
		((ARE_IN_ORDER (x, y)  or  ARE_IN_ORDER (y, x))  and
		 (if (ARE_IN_ORDER (x, y)  and  ARE_IN_ORDER (y, z))
		  then ARE_IN_ORDER (x, z)))
    !*/

    utility_function Boolean Are_In_Order (
	    preserves T& x,
	    preserves T& y
	);
    /*!
	ensures
	    Are_In_Order = ARE_IN_ORDER (x, y)		
    !*/

};

#endif // AT_GENERAL_ARE_IN_ORDER