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

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

#ifndef CT_PARTIAL_MAP_KERNEL_2
#define CT_PARTIAL_MAP_KERNEL_2 1

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

#include "AT/Partial_Map/Kernel.h"
/*!
    #include "AT/General/Is_Equal_To.h"
    #include "AT/General/Hash.h"
!*/
#include "CT/Queue/Kernel_1a.h"
#include "CT/Array/Kernel_1.h"

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

concrete_template <
	concrete_instance class D_Item,
	/*!
	    implements
		abstract_instance General_Is_Equal_To <D_Item, D_Item>
	!*/
	concrete_instance class R_Item,
	concrete_instance utility_class D_Item_Hash,
	/*!
	    implements
		abstract_instance General_Hash <D_Item>
	!*/	    
	Integer_constant hash_table_size,
	/*!
	    satisfies restriction
	        hash_table_size > 0
	!*/
        concrete_instance class D_R_Pair =
            Record <
		    D_Item, 
		    R_Item
		>,
        concrete_instance class Queue_Of_D_R_Pair =
    	    Queue_Kernel_1a <D_R_Pair>,
        concrete_instance class Array_Of_Queue =
	    Array_Kernel_1 <Queue_Of_D_R_Pair>,
	concrete_instance class Rep =
	    Representation <
		    Array_Of_Queue,
		    Integer
		>
    >
class Partial_Map_Kernel_2 :
    implements
	abstract_instance Partial_Map_Kernel <D_Item, R_Item>,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Array_Of_Queue, hash_table);
    rep_field_name (Rep, 1, Integer, total_pairs);

    field_name (D_R_Pair, 0, D_Item, d_item);
    field_name (D_R_Pair, 1, R_Item, r_item);
    
    /*!
	convention
	    self.hash_table.lb = 0  and
	    self.hash_table.ub = hash_table_size - 1  and
	    for all i: integer, q: string of (D_Item, R_Item)
		    where ((i,q) is in self.hash_table.table)
		(for all d1, d2: D_Item, r1, r2: R_Item,
		     a, b, c: string of (D_Item, R_Item)
			 where (q = a * <(d1,r1)> * b * <(d2,r2)> * c)
		     (d1 /= d2)  and
		 for all d: D_Item, r: R_Item
			where ((d,r) is in elements (q))
		    (HASH_FUNCTION (d) mod hash_table_size = i))  and
	    self.total_pairs =
		sum i: integer, q: string of (D_Item, R_Item)
			where ((i,q) is in self.hash_table.table)
		    (|q|)
		    
	correspondence
	    self =
		union i: integer, q: string of (D_Item, R_Item)
			where ((i,q) is in self.hash_table.table)
		    (elements (q))
    !*/

    local_procedure_body Initialize ()
    {
	//-------- for students to fill in --------    
    }
    
    local_procedure_body Move_To_Front (
	    alters Queue_Of_D_R_Pair& q,
	    preserves D_Item& d
	)
    /*!
	ensures
	    q is permutation of #q  and
	    (if IS_DEFINED_IN (elements (q), d)
	     then there exists r: R_Item (<(d,r)> is prefix of q)
    !*/
    {
	//-------- for students to fill in --------    
    }

public:

    standard_concrete_operations (Partial_Map_Kernel_2);

    procedure_body Define (
	    consumes D_Item& d,
            consumes R_Item& r
	)
    {
	//-------- for students to fill in --------    
    }

    procedure_body Undefine (
            preserves D_Item& d,
	    produces D_Item& d_copy,
            produces R_Item& r
	)
    {
	//-------- for students to fill in --------    
    }

    procedure_body Undefine_Any (
	    produces D_Item& d,
	    produces R_Item& r
	)
    {
	//-------- for students to fill in --------    
    }

    function_body Boolean Is_Defined (
	    preserves D_Item& d
	)
    {
	//-------- for students to fill in --------    
    }

    function_body R_Item& operator [] (
	    preserves D_Item& d
	)
    {
	//-------- for students to fill in --------    
    }

    function_body Integer Size ()
    {
	//-------- for students to fill in --------    
    }

};

#endif // CT_PARTIAL_MAP_KERNEL_2