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

//  /*-------------------------------------------------------------------*\
//  |   Abstract Template : Binary_Tree_Kernel
//  \*-------------------------------------------------------------------*/

#ifndef AT_BINARY_TREE_KERNEL
#define AT_BINARY_TREE_KERNEL 1
    
///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

abstract_template <
	concrete_instance class Item,
        concrete_instance class Subtree_Type
	/*!
	    implements
		abstract_instance Binary_Tree_Kernel <
			Item,
			Subtree_Type
                    >
	!*/
    >
class Binary_Tree_Kernel
{
public:

    /*!
        math definition HEIGHT (
	        tree: binary tree of Item
	    ): integer satisfies
	    if tree = empty_tree
	    then HEIGHT(tree) = 0
	    else there exists root: Item, left, right: binary tree of Item
		     (tree = compose (root, left, right) and
		      HEIGHT(tree) = 1 + max (HEIGHT(left), HEIGHT(right)))
    !*/

    standard_abstract_operations (Binary_Tree_Kernel);
    /*!
	Binary_Tree_Kernel is modeled by binary tree of Item
	initialization ensures
            self = empty_tree
    !*/

    procedure Compose (
	    consumes Item& x,
	    consumes Subtree_Type& left_subtree,
	    consumes Subtree_Type& right_subtree
	) is_abstract;
    /*!
	produces self
	ensures
	    self = compose (#x, #left_subtree, #right_subtree)
    !*/

    procedure Decompose (
	    produces Item& x,
	    produces Subtree_Type& left_subtree,
	    produces Subtree_Type& right_subtree
	) is_abstract;
    /*!
	consumes self
	requires
	    self /= empty_tree
	ensures
	    #self = compose (x, left_subtree, right_subtree)
    !*/

    function Item& operator [] (
	    preserves Accessor_Position& current
	) is_abstract;
    /*!
	requires
	    self /= empty_tree
	ensures
	    there exists left, right: binary tree of Item
		(self = compose (self[current], left, right))
    !*/

    function Integer Height () is_abstract;
    /*!
	ensures
	    Height = HEIGHT(self)
    !*/
    
    function Integer Size () is_abstract;
    /*!
	ensures
	    Size = |self|
    !*/

};

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

#endif // AT_BINARY_TREE_KERNEL