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

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

#ifndef CT_SET_SUBTRACT_1
#define CT_SET_SUBTRACT_1 1

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

#include "AT/Set/Subtract.h"

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

concrete_template <
	concrete_instance class Item,
	concrete_instance class Set_Base
	/*!
	    implements
		abstract_instance Set_Kernel <Item>
	!*/
    >
class Set_Subtract_1 :
    implements
	abstract_instance Set_Subtract <Item>,
    extends
	concrete_instance Set_Base
{
public:
    
    procedure_body Subtract (
	    preserves Set_Subtract <Item>& s
	)
    {
	object catalyst Set_Subtract_1 temp;
	
	while (self.Size () > 0)
	/*!
	    alters self, temp
	    preserves s
	    maintains
		self union temp union s =
		    #self union #temp union s  and
		self intersection temp = {}  and
		temp intersection s = {}
	    decreases
		|self|
	!*/
	{
	    object Item x;

	    self.Remove_Any (x);
	    if (not s.Is_Member (x))
	    {
		temp.Add (x);
	    }
	}
	self &= temp;
    }

};

#endif // CT_SET_SUBTRACT_1