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

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

#ifndef AT_BIJECTIVE_PARTIAL_MAP_KERNEL
#define AT_BIJECTIVE_PARTIAL_MAP_KERNEL 1

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

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

    /*!
	math subtype BIJECTIVE_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)
		    (d1 = d2 iff r1 = r2)

	math definition D_ITEM_IS_DEFINED_IN (
		b: BIJECTIVE_PARTIAL_FUNCTION,
		d: D_Item
	    ): boolean is
	    there exists r: R_Item
		((d,r) is in m)

        math definition R_ITEM_IS_DEFINED_IN (
		b: BIJECTIVE_PARTIAL_FUNCTION,
		r: R_Item
	    ): boolean is
	    there exists d: D_Item
		((d,r) is in m)
    !*/

    standard_abstract_operations (Bijective_Partial_Map_Kernel);
    /*!
        Bijective_Partial_Map_Kernel is modeled by BIJECTIVE_PARTIAL_FUNCTION
        initialization
            ensures self = empty_set
    !*/

    procedure Define (
	    consumes D_Item& d,
            consumes R_Item& r
	) is_abstract;
    /*!
	requires
	    not D_ITEM_IS_DEFINED_IN (self, d) and
	    not R_ITEM_IS_DEFINED_IN (self, r)
	ensures
	    self = #self union {(#d, #r)}
    !*/

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

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

    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 Boolean D_Is_Defined (
	    preserves D_Item& d
	) is_abstract;
    /*!
	ensures
	    D_Is_Defined = D_ITEM_IS_DEFINED_IN (self, d)
    !*/

    function Boolean R_Is_Defined (
	    preserves R_Item& r
	) is_abstract;
    /*!
	ensures
	    R_Is_Defined = R_ITEM_IS_DEFINED_IN (self, r)
    !*/
    
    function Integer Size () is_abstract;
    /*!
	ensures
	    Size = |self|
    !*/    

};

#endif // AT_BIJECTIVE_PARTIAL_MAP_KERNEL