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

//  /*-------------------------------------------------------------------*\
//  |   Concrete Template : Set_Kernel_C
//  \*-------------------------------------------------------------------*/

#ifndef CT_SET_KERNEL_C
#define CT_SET_KERNEL_C 1

///---------------------------------------------------------------------
/// Global Context -----------------------------------------------------
///---------------------------------------------------------------------

/*!
    #include "AT/Set/Kernel.h"
!*/

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

concrete_template <
	concrete_instance class Item,
	concrete_instance class Set_Base
	/*!
	    implements
		abstract_instance Set_Kernel <Item>
	!*/
    >
class Set_Kernel_C :
    checks
	concrete_instance Set_Base
{
public:
    
    procedure_body Add (
	    consumes Item& x
	)
    {
	assert (not self.Is_Member (x),
		"x is not in self");
	self.Set_Base::Add (x);
    }  

    procedure_body Remove (
            preserves Item& x,
            produces Item& x_copy
	)
    {
	assert (self.Is_Member (x),
		"x is in self");
	self.Set_Base::Remove (x, x_copy);
    }  

    procedure_body Remove_Any (
            produces Item& x
	)
    {
	assert (self.Size () > 0,
		"self /= empty_set");
	self.Set_Base::Remove_Any (x);
    }  

};

#endif // CT_SET_KERNEL_C