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

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

#ifndef AT_ARRAY_EXCHANGE_AT
#define AT_ARRAY_EXCHANGE_AT 1

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

#include "AT/Array/Kernel.h"

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

abstract_template <
        concrete_instance class Item
    >
class Array_Exchange_At :
    extends
	abstract_instance Array_Kernel <Item>
{
public:
    
    procedure Exchange_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
	    there exists x, y: Item
		({(i, x), (j, y)} is subset of #self.table and
		 self.table = (#self.table - {(i, x), (j, y)})
				   union {(i, y), (j, x)}) and
	    self.lb = #self.lb and
	    self.ub = #self.ub
    !*/

};

#endif // AT_ARRAY_EXCHANGE_AT