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

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

#ifndef AT_FIXED_LENGTH_BIT_STRING_KERNEL
#define AT_FIXED_LENGTH_BIT_STRING_KERNEL 1

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

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

    /*!
        math subtype BIT is integer
	    exemplar b
	    constraint
	        b is in {0,1}

	math subtype FIXED_LENGTH_BIT_STRING_MODEL is string of BIT
	    exemplar s
	    constraint
	        |s| = String_Length

	math subtype BIT_POSITION is integer
	    exemplar p
	    constraint
	        0 <= p < String_Length

	math definition BIT_VALUE_AT (
                s: FIXED_LENGTH_BIT_STRING_MODEL,
	        pos: BIT_POSITION
	    ): BIT satisfies
	    there exists left, right: string of BIT
		(s = left * <BIT_VALUE_AT (s, pos)> * right  and
		 |right| = pos)

        math definition BITS_FOR_INTEGER: integer satisfies
	    2^(BITS_FOR_INTEGER-1) < MAXIMUM_INTEGER <=
	        2^BITS_FOR_INTEGER

	math definition SIMPLE_BINARY_DECODING (
		s: string of BIT
	    ): integer satisfies
	    if s = empty_string
	    then SIMPLE_BINARY_DECODING (s) = 0
	    else there exists t: string of BIT, b: BIT
		     (s = t * <b> and
		      SIMPLE_BINARY_DECODING (s) =
		          2 * SIMPLE_BINARY_DECODING (t) + b)
    !*/

    standard_abstract_operations (Fixed_Length_Bit_String_Kernel);
    /*!
        Fixed_Length_Bit_String_Kernel is modeled by
	    FIXED_LENGTH_BIT_STRING_MODEL
	initialization ensures
	    elements (self) = {0}
    !*/

    procedure Set_Bit_At (
	    preserves Integer pos,
	    preserves Integer value
	) is_abstract;
    /*!
	requires
	    0 <= pos < String_Length  and
	    0 <= value < 2
	ensures
	    BIT_VALUE_AT (self, pos) = value  and
	    for all p: BIT_POSITION where (p /= pos)
	        (BIT_VALUE_AT (self, p) = BIT_VALUE_AT (#self, p))
    !*/

    function Integer Bit_Value_At (
	    preserves Integer pos
	) is_abstract;
    /*!
	requires
	    0 <= pos < String_Length
	ensures
	    Bit_Value_At = BIT_VALUE_AT (self, pos)
    !*/

    function Integer Length (
	) is_abstract;
    /*!
	ensures
	    Length = String_Length
    !*/

};

#endif // AT_FIXED_LENGTH_BIT_STRING_KERNEL