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

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

#ifndef AT_FIXED_LENGTH_BIT_STRING_SET_SUBSTRING_FROM_INTEGER
#define AT_FIXED_LENGTH_BIT_STRING_SET_SUBSTRING_FROM_INTEGER 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_Set_Substring_From_Integer :
    extends
	abstract_instance Fixed_Length_Bit_String_Kernel <String_Length>
{
public:

    procedure Set_Substring_From_Integer (
	    preserves Integer pos,
	    preserves Integer len,
	    preserves Integer source
	) is_abstract;
    /*!
	requires
	    0 <= pos < String_Length  and
	    0 < len <= String_Length - pos  and
	    there exists s: string of BIT
		(|s| = len  and
		 SIMPLE_BINARY_DECODING (s) = source)
	ensures
	    there exists w, x, y, z: string of BIT
		(#self = x * y * z  and
		 self = x * w * z  and
		 |z| = pos and
		 |y| = |w| = len  and
		 SIMPLE_BINARY_DECODING (w) = source)
    !*/

};

#endif // AT_FIXED_LENGTH_BIT_STRING_SET_SUBSTRING_FROM_INTEGER