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

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

#ifndef CT_SET_KERNEL_1
#define CT_SET_KERNEL_1 1
 
///---------------------------------------------------------------------
/// Global Context -----------------------------------------------------
///---------------------------------------------------------------------

#include "AT/Set/Kernel.h"
/*!
    #include "AT/General/Is_Equal_To.h"
!*/
#include "CT/Queue/Kernel_1a.h"

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

concrete_template <
	concrete_instance class Item,
        /*!
            implements
                abstract_instance General_Is_Equal_To <Item>
        !*/
        concrete_instance class Queue_Of_Item =
            Queue_Kernel_1a <Item>,
	concrete_instance class Rep =
            Representation <Queue_Of_Item>
    >
class Set_Kernel_1 :
    implements
	abstract_instance Set_Kernel <Item>,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Queue_Of_Item, items);

    /*!
	convention
	    |self.items| = |elements (self.items)|
	    
	correspondence
	    self = elements (self.items)
    !*/

public:

    standard_concrete_operations (Set_Kernel_1);

    procedure_body Add (
	    consumes Item& x
	)
    {
	self[items].Enqueue (x);
    }

    procedure_body Remove (
	    preserves Item& x,
	    produces Item& x_copy
	)
    {
	/*! auxiliary object Integer remaining = self[items].Length (); !*/
	while (true)
	/*!
	    alters self.items, remaining
	    preserves x
	    produces x_copy
	    maintains
		self.items /= empty_string  and
		there exists examined, unexamined: string of Item
		    (x is in elements (unexamined)  and
		     |unexamined| = remaining  and
		     #self.items = examined * unexamined  and
		     self.items = unexamined * examined)
	    decreases
		remaining
	!*/
	{
	    /*! auxiliary remaining--; !*/
	    self[items].Dequeue (x_copy);
	    if (x.Is_Equal_To (x_copy))
	    {
		return;
	    }
	    self[items].Enqueue (x_copy);
	}
    }


    procedure_body Remove_Any (
	    produces Item& x
	)
    {
	//-------- for students to fill in --------
    }

    function_body Boolean Is_Member (
	    preserves Item& x
	)
    {
	//-------- for students to fill in --------
    }

    function_body Integer Size ()
    {
	return self[items].Length ();
    }

};

#endif // CT_SET_KERNEL_1