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

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

#ifndef AT_STATIC_ARRAY_EXCHANGE_AT
#define AT_STATIC_ARRAY_EXCHANGE_AT 1

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

#include "AT/Static_Array/Kernel.h"

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

abstract_template <
        concrete_instance class Item,
	Integer_constant lower,
        Integer_constant upper
        /*!
            satisfies restriction
                lower <= upper
	!*/
    >
class Static_Array_Exchange_At :
    extends
	abstract_instance Static_Array_Kernel <Item, lower, upper>
{
public:
    
    procedure Exchange_At (
	    preserves Integer i,
	    preserves Integer j
	) is_abstract;
    /*!
	requires
	    lower <= i and i <= upper and
	    lower <= j and j <= upper
	ensures
	    there exists x, y: Item
		({(i, x), (j, y)} is subset of #self and
		 self = (#self - {(i, x), (j, y)})
				   union {(i, y), (j, x)})
    !*/

};

#endif // AT_STATIC_ARRAY_EXCHANGE_AT