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

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

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

#include "AT/Binary_Tree/Kernel.h"

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

concrete_template <
	concrete_instance class Item,
	concrete_instance class Subtree_Type,
	/*!
	    implements
		abstract_instance Binary_Tree_Kernel <
		        Item,
			Subtree_Type
		    >
	!*/
	concrete_instance class Rep =
            Representation <
		    Item,
		    Pointer_C <Subtree_Type>,
		    Pointer_C <Subtree_Type>,
		    Integer,
		    Integer
		>
    >
class Binary_Tree_Kernel_1 :
    implements
	abstract_instance Binary_Tree_Kernel <
                Item,
                Subtree_Type
            >,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Item, data);
    rep_field_name (Rep, 1, Pointer_C <Subtree_Type>, left_subtree_ptr);
    rep_field_name (Rep, 2, Pointer_C <Subtree_Type>, right_subtree_ptr);
    rep_field_name (Rep, 3, Integer, height);
    rep_field_name (Rep, 4, Integer, size);
    
    /*!
	math definition IS_LEGAL_REP (
		rep_data: Item,
		rep_left_ptr: [Pointer_C <binary tree of Item>],
		rep_right_ptr: [Pointer_C <binary tree of Item>],
		rep_height: integer,
		rep_size: integer
	    ): boolean is
	    0 <= rep_height <= rep_size <= (2^rep_height - 1)  and
	    (if (rep_height + rep_size = 0)
	     then rep_left_ptr = rep_right_ptr = NULL
	     else rep_left_ptr /= NULL  and
		  rep_right_ptr /= NULL  and
		  rep_left_ptr /= rep_right_ptr  and
		  rep_size = 1 + (*rep_left_ptr).size +
				 (*rep_right_ptr).size and
		  rep_height = 1 + MAX((*rep_left_ptr).height,
				       (*rep_right_ptr).height))

	math subtype TREE_REP is Rep
	    exemplar tr
	    constraint
		IS_LEGAL_REP (tr.data, tr.left_subtree_ptr,
		              tr.right_subtree_ptr, tr.height, tr.size)

	math definition ABSTRACT_TREE (
		t_rep: TREE_REP
	    ): binary tree of Item satisfies
	    if t_rep.size = 0
	    then ABSTRACT_TREE (t_rep) = empty_tree
	    else ABSTRACT_TREE (t_rep) =
		    compose (t_rep.data,
			     *(t_rep.left_subtree_ptr),
			     *(t_rep.right_subtree_ptr))
				 
	convention
	    IS_LEGAL_REP (self.data, self.left_subtree_ptr,
			  self.right_subtree_ptr, self.height, self.size)
	correspondence
	    self = ABSTRACT_TREE ((self.data, self.left_subtree_ptr,
				   self.right_subtree_ptr,
				   self.height, self.size))
	!*/
    
    procedure_body Initialize ()
    {
	self[left_subtree_ptr] = NULL;
	self[right_subtree_ptr] = NULL;
    }
    
    procedure_body Finalize ()
    {
	// This works without checking whether a subtree pointer is
	// NULL because, in that case, Delete does nothing.

	Delete (self[left_subtree_ptr]);
	Delete (self[right_subtree_ptr]);
    }

public:

    standard_concrete_operations (Binary_Tree_Kernel_1);

    procedure_body Compose (
	    consumes Item& x,
	    consumes Subtree_Type& left_subtree,
	    consumes Subtree_Type& right_subtree
	)
    {
	self.Clear ();

	self[data] &= x;
	New (self[left_subtree_ptr]);
	New (self[right_subtree_ptr]);
	self[size] = 1 + left_subtree.Size () + right_subtree.Size ();

	if (left_subtree.Height() > right_subtree.Height())
	{
	    self[height] = left_subtree.Height() + 1;
	}
	else
	{
	    self[height] = right_subtree.Height() + 1;
	}

	(*(self[left_subtree_ptr])) &= left_subtree;
	(*(self[right_subtree_ptr])) &= right_subtree;
    }

    procedure_body Decompose (
	    produces Item& x,
	    produces Subtree_Type& left_subtree,
	    produces Subtree_Type& right_subtree
	)
    {
	self[data] &= x;
	(*(self[left_subtree_ptr])) &= left_subtree;
	(*(self[right_subtree_ptr])) &= right_subtree;

	self.Clear ();
    }

    function_body Item& operator [] (
	    preserves Accessor_Position& current
	)
    {
	return self[data];
    }

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

};

//-------------------------------------------------------------------------

#endif // CT_BINARY_TREE_KERNEL_1