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

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

#ifndef AT_ARRAY_ARE_IN_ORDER_AT
#define AT_ARRAY_ARE_IN_ORDER_AT 1

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

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

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

abstract_template <
        concrete_instance class Item,
        concrete_instance utility_class Item_Are_In_Order
        /*!
            implements
                abstract_instance General_Are_In_Order <Item>
        !*/
    >
class Array_Are_In_Order_At :
    extends
	abstract_instance Array_Kernel <Item>
{
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
	    self.lb <= i and i <= self.ub and
	    self.lb <= j and j <= self.ub
	ensures
	    Are_In_Order_At = ARE_IN_ORDER_AT (self.table, i, j))
    !*/

};

#endif // AT_ARRAY_ARE_IN_ORDER_AT