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

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

#ifndef AT_STATIC_ARRAY_KERNEL
#define AT_STATIC_ARRAY_KERNEL 1

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

abstract_template <
        concrete_instance class Item,
        Integer_constant lower,
        Integer_constant upper
        /*!
            satisfies restriction
                lower <= upper
	!*/
    >
class Static_Array_Kernel
{
public:

    /*!
	math subtype INDEXED_TABLE is finite set of (
		i: integer
		x: Item
	    )
	    exemplar t
	    constraint
		for all i1, i2: integer, x1, x2: Item
			where ((i1,x1) is in t and
			       (i2,x2) is in t)
		    (if i1 = i2 then x1 = x2)

        math subtype STATIC_ARRAY_MODEL is INDEXED_TABLE
            exemplar a
	    constraint
		for all i: integer
		    (there exists x: Item
			((i,x) is in a)  iff 
		     lower <= i <= upper)	
    !*/

    standard_abstract_operations (Static_Array_Kernel);
    /*!
	Static_Array_Kernel is modeled by STATIC_ARRAY_MODEL
	initialization ensures
		for all i: integer
		    (there exists x: Item
			((i,x) is in a)  iff 
		     (lower <= i <= upper  and
		      is_initial (x)))	
    !*/

    function Item& operator [] (
	    preserves Integer i
	) is_abstract;
    /*!
	requires
	    lower <= i <= upper
	ensures
	    (i, self[i]) is in self
    !*/

    function Integer Lower_Bound () is_abstract;
    /*!
	ensures
	    Lower_Bound = lower
    !*/

    function Integer Upper_Bound () is_abstract;
    /*!
	ensures
	    Upper_Bound = upper
    !*/
    
};

#endif // AT_STATIC_ARRAY_KERNEL