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

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

#ifndef AT_SET_KERNEL
#define AT_SET_KERNEL 1

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

abstract_template <
        concrete_instance class Item
    >
class Set_Kernel
{
public:

    standard_abstract_operations (Set_Kernel);
    /*!
        Set_Kernel is modeled by set of Item
        initialization ensures
            self = empty_set
    !*/
    
    procedure Add (
	    consumes Item& x
	) is_abstract;
    /*!
	requires
	    x is not in self
	ensures
	    self = #self union {#x}
    !*/

    procedure Remove (
            preserves Item& x,
            produces Item& x_copy
	) is_abstract;
    /*!
	requires
	    x is in self
	ensures
	    self = #self - {x}  and
	    x_copy = x
    !*/

    procedure Remove_Any (
            produces Item& x
	) is_abstract;
    /*!
	requires
	    self /= empty_set
	ensures
	    x is in #self  and
	    self = #self - {x}
    !*/

    function Boolean Is_Member (
	    preserves Item& x
	) is_abstract;
    /*!
	ensures
	    Is_Member = (x is in self)
    !*/

    function Integer Size () is_abstract;
    /*!
	ensures
	    Size = |self|
    !*/

};

#endif // AT_SET_KERNEL