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

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

#ifndef AT_PARTIAL_MAP_KERNEL
#define AT_PARTIAL_MAP_KERNEL 1
   
///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

abstract_template <
        concrete_instance class D_Item,
        concrete_instance class R_Item
    >
class Partial_Map_Kernel
{
public:

    /*!
	math subtype PARTIAL_FUNCTION is finite set of (
		d: D_Item
		r: R_Item
	    )
	    exemplar m
	    constraint
		for all d1, d2: D_Item, r1, r2: R_Item
			where ((d1,r1) is in m  and
			       (d2,r2) is in m)
		    (if d1 = d2 then r1 = r2)

	math definition IS_DEFINED_IN (
		m: PARTIAL_FUNCTION,
		d: D_Item
	    ): boolean is
	    there exists r: R_Item
		((d,r) is in m)
    !*/

    standard_abstract_operations (Partial_Map_Kernel);
    /*!
        Partial_Map_Kernel is modeled by PARTIAL_FUNCTION
        initialization
            ensures  self = empty_set
    !*/
    
    procedure Define (
	    consumes D_Item& d,
            consumes R_Item& r
	) is_abstract;
    /*!
	requires
	    not IS_DEFINED_IN (self, d)
	ensures
	    self = #self union {(#d, #r)}
    !*/

    procedure Undefine (
            preserves D_Item& d,
            produces D_Item& d_copy,
	    produces R_Item& r
	) is_abstract;
    /*!
	requires
	    IS_DEFINED_IN (self, d)
	ensures
	    d_copy = d  and
	    (d_copy, r) is in #self and
	    self = #self - {(d_copy, r)}
    !*/

    procedure Undefine_Any (
            produces D_Item& d,
	    produces R_Item& r
	) is_abstract;
    /*!
	requires
	    self /= empty_set
	ensures
	    (d, r) is in #self and
	    self = #self - {(d, r)}
    !*/

    function R_Item& operator [] (
	    preserves D_Item& d
	) is_abstract;
    /*!
	requires
	    IS_DEFINED_IN (self, d)
	ensures
	    (d, self[d]) is in self
    !*/

    function Boolean Is_Defined (
	    preserves D_Item& d
	) is_abstract;
    /*!
	ensures
	    Is_Defined = IS_DEFINED_IN (self, d)
    !*/
    
    function Integer Size () is_abstract;
    /*!
	ensures
	    Size = |self|
    !*/

};

#endif // AT_PARTIAL_MAP_KERNEL