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

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

#ifndef AT_FIXED_LENGTH_BIT_STRING_EXCLUSIVE_OR
#define AT_FIXED_LENGTH_BIT_STRING_EXCLUSIVE_OR 1

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

#include "AT/Fixed_Length_Bit_String/Kernel.h"

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

abstract_template <
        Integer_constant String_Length,
        /*!
	    satisfies restriction
	        String_Length > 0
	!*/
        concrete_instance class T
        /*!
	    implements
	        abstract_instance Fixed_Length_Bit_String_Kernel <
		                          String_Length
		                      >
	!*/
    >
class Fixed_Length_Bit_String_Exclusive_Or :
    extends
	abstract_instance Fixed_Length_Bit_String_Kernel <String_Length>
{
public:

    /*!
        math definition EXCLUSIVE_OR (
		bit1: BIT,
		bit2: BIT
	    ): BIT satisfies
	    EXCLUSIVE_OR (0, 0) = 0  and
	    EXCLUSIVE_OR (0, 1) = 1  and
	    EXCLUSIVE_OR (1, 0) = 1  and
	    EXCLUSIVE_OR (1, 1) = 0
    !*/
    
    procedure Exclusive_Or (
	    preserves T& rhs
	) is_abstract;
    /*!
	ensures
	    for all p: BIT_POSITION
	        (BIT_VALUE_AT (self, p) =
		     EXCLUSIVE_OR (BIT_VALUE_AT (#self, p),
		                   BIT_VALUE_AT (rhs, p))
    !*/

};

#endif // AT_FIXED_LENGTH_BIT_STRING_EXCLUSIVE_OR