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

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

#ifndef CT_SET_KERNEL_2
#define CT_SET_KERNEL_2 1

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

#include "AT/Set/Kernel.h"
/*!
    #include "AT/General/Is_Equal_To.h"
    #include "AT/General/Hash.h"
!*/
#include "CT/Set/Kernel_1.h"
#include "CT/Static_Array/Kernel_1.h"

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

concrete_template <
	concrete_instance class Item,
        /*!
            implements
                abstract_instance General_Is_Equal_To <Item>
        !*/
	concrete_instance utility_class Item_Hash,
	/*!
	    implements
		abstract_instance General_Hash <Item>
	!*/
	Integer_constant hash_table_size,
	/*!
	    satisfies restriction
	        hash_table_size > 0
	!*/
	concrete_instance class Set_Of_Item =
            Set_Kernel_1 <Item>,
        concrete_instance class Static_Array_Of_Set_Of_Item =
            Static_Array_Kernel_1 <
                    Set_Of_Item,
                    0,
                    hash_table_size - 1
                >,
	concrete_instance class Rep =
            Representation <
		    Static_Array_Of_Set_Of_Item,
		    Integer
		>
    >
class Set_Kernel_2 :
    implements
	abstract_instance Set_Kernel <Item>,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Static_Array_Of_Set_Of_Item, hash_table);
    rep_field_name (Rep, 1, Integer, size);

    /*!
	convention
	    for all i: integer, s: finite set of Item
		    where ((i,s) is in self.hash_table)
		(|s| = |elements (s)|  and
		 for all x: Item
			where (x is in elements (s))
		    (HASH_FUNCTION (x) mod hash_table_size = i))  and
	    self.size =
		sum i: integer, s: finite set of Item
			where ((i,s) is in self.hash_table)
		    (|s|)
		    
	correspondence
	    self =
		union i: integer, s: finite set of Item
			where ((i,s) is in self.hash_table)
		    (elements (s))
    !*/

public:

    standard_concrete_operations (Set_Kernel_2);

    procedure_body Add (
	    consumes Item& x
	)
    {
	object Integer k = Item_Hash::Hash (x) mod hash_table_size;
	self[hash_table][k].Add (x);
	self[size]++;
    }

    procedure_body Remove (
	    preserves Item& x,
	    produces Item& x_copy
	)
    {
	object Integer k = Item_Hash::Hash (x) mod hash_table_size;
	self[hash_table][k].Remove (x, x_copy);
	self[size]--;
    }

    procedure_body Remove_Any (
	    produces Item& x
	)
    {
	object Integer k;

	while (self[hash_table][k].Size () == 0)
	/*!
	    alters k
	    maintains
	        for all i: integer where (0 <= i < k)
		    ((i, {}) is in self.hash_table.table)
	    decreases
	        hash_table_size - k
	!*/
	{
	    k++;
	}
	self[hash_table][k].Remove_Any (x);
	self[size]--;
    }

    function_body Boolean Is_Member (
	    preserves Item& x
	)
    {
	object Integer k = Item_Hash::Hash (x) mod hash_table_size;
	return self[hash_table][k].Is_Member (x);
    }

    function_body Integer Size ()
    {
	return self[size];
    }

};

#endif // CT_SET_KERNEL_2