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

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

#ifndef AT_BAG_KERNEL
#define AT_BAG_KERNEL 1

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

abstract_template <
        concrete_instance class Item
    >
class Bag_Kernel
{
public:

    standard_abstract_operations (Bag_Kernel);
    /*!
        Bag_Kernel is modeled by finite multiset of Item
        initialization ensures
            self = empty_multiset
    !*/

    procedure Add (
	    consumes Item& x
	) is_abstract;
    /*!
	ensures
	    self = #self union {#x}
    !*/

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

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

#endif // AT_BAG_KERNEL