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

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

#ifndef AT_STATIC_ARRAY_ARE_IN_ORDER_AT
#define AT_STATIC_ARRAY_ARE_IN_ORDER_AT 1

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

#include "AT/Static_Array/Kernel.h"
/*!
    #include "AT/General/Are_In_Order.h"
!*/

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

abstract_template <
        concrete_instance class Item,
	Integer_constant lower,
        Integer_constant upper,
	/*!
	    satisfies restriction
	        lower <= upper
	!*/
        concrete_instance utility_class Item_Are_In_Order
        /*!
            implements
                abstract_instance General_Are_In_Order <Item>
        !*/
    >
class Static_Array_Are_In_Order_At :
    extends
	abstract_instance Static_Array_Kernel <Item,lower,upper>
{
public:
    
    /*!
        math definition ARE_IN_ORDER_AT (
	        t: INDEXED_TABLE
                i: integer
		j: integer
            ): boolean is
	   there exists x, y: Item
	       ({(i, x), (j, y)} is subset of t and
		 ARE_IN_ORDER (x, y))
    !*/

    function Boolean Are_In_Order_At (
	    preserves Integer i,
	    preserves Integer j
	) is_abstract;
    /*!
	requires
	    lower <= i and i <= upper and
	    lower <= j and j <= upper
	ensures
	    Are_In_Order_At = ARE_IN_ORDER_AT (self, i, j))
    !*/

};

#endif // AT_STATIC_ARRAY_ARE_IN_ORDER_AT