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

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

#ifndef AT_TREE_KERNEL
#define AT_TREE_KERNEL 1
  
///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

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

    standard_abstract_operations (Tree_Kernel);    
    /*!
        Tree_Kernel is modeled by tree of Item
        initialization ensures
	    there exists x: Item
	        (is_initial (x) and
		 self = compose (x, empty_string))
    !*/
    
    procedure Add (
	    preserves Integer pos,
	    consumes Subtree_Type& t
	) is_abstract;
    /*!
	requires
	    0 <= pos <= |children (self)|
	ensures
	    there exists a, b: string of NON_EMPTY_TREE
		(|a| = pos and
		 children (#self) = a * b and
		 self = compose (root (#self), a * <#t> * b))
    !*/

    procedure Remove (
            preserves Integer pos,
	    produces Subtree_Type& t
	) is_abstract;
    /*!
	requires
	    0 <= pos < |children (self)|
	ensures
	    there exists a, b: string of NON_EMPTY_TREE
		(|a| = pos and
		 children (#self) = a * <t> * b and
		 self = compose (root (#self), a * b))
    !*/

    function Item& operator [] (
	    preserves Accessor_Position& current
	) is_abstract;
    /*!
	ensures
	    self = compose (self[current], children (self))
    !*/

    function Integer Number_Of_Children () is_abstract;
    /*!
	ensures
	    Number_Of_Children = |children (self)|
    !*/

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

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

#endif // AT_TREE_KERNEL