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

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

#ifndef AT_ARRAY_KERNEL
#define AT_ARRAY_KERNEL 1

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

abstract_template <
	concrete_instance class Item
    >
class 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 ARRAY_MODEL is (
		lb: integer
		ub: integer
		table: INDEXED_TABLE
	    )
            exemplar a
	    constraint
		for all i: integer
		    (there exists x: Item
			((i,x) is in a.table)  iff 
			a.lb <= i <= a.ub)		
    !*/

    standard_abstract_operations (Array_Kernel);
    /*!
	Array_Kernel is modeled by ARRAY_MODEL
	initialization ensures
	    self = (1, 0, empty_set)
    !*/

    procedure Set_Bounds (
            preserves Integer lower,
            preserves Integer upper
        ) is_abstract;
    /*!
	ensures
	    self.lb = lower  and
	    self.ub = upper  and
	    for all i: integer
		(there exists x: Item
		    ((i,x) is in self.table  iff
			self.lb <= i <= self.ub)  and
			is_initial (x))
    !*/

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

    function Integer Lower_Bound () is_abstract;
    /*!
	ensures
	    Lower_Bound = self.lb
    !*/
    function Integer Upper_Bound () is_abstract;
    /*!
	ensures
	    Upper_Bound = self.ub
    !*/



};

#endif // AT_ARRAY_KERNEL