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

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

#ifndef AT_FIXED_LENGTH_BIT_STRING_SHIFT_RIGHT
#define AT_FIXED_LENGTH_BIT_STRING_SHIFT_RIGHT 1

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

#include "AT/Fixed_Length_Bit_String/Kernel.h"

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

abstract_template <
	Integer_constant String_Length
        /*!
	    satisfies restriction
	        String_Length > 0
        !*/
    >
class Fixed_Length_Bit_String_Shift_Right :
    extends
	abstract_instance Fixed_Length_Bit_String_Kernel <String_Length>
{
public:

    procedure Shift_Right (
	    preserves Integer bits_to_shift,
	    preserves Integer fill_value
	) is_abstract;
    /*!
	requires
	    0 < bits_to_shift <= |self|  and
	    0 <= fill_value < 2
	ensures
	    there exists a, b, c: string of Integer
		(#self = b * a  and
		 self = c * b  and
		 |a| = |c| = bits_to_shift  and
		 for all z: BIT where (<z> is substring of c)
		     (z = fill_value)
    !*/

};

#endif // AT_FIXED_LENGTH_BIT_STRING_SHIFT_RIGHT