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

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

#ifndef AT_STACK_KERNEL
#define AT_STACK_KERNEL 1

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

abstract_template <
	concrete_instance class Item
    >
class Stack_Kernel
{
public:

    standard_abstract_operations (Stack_Kernel);
    /*!
	Stack_Kernel is modeled by string of Item
	initialization ensures
            self = empty_string
    !*/

    procedure Push (
	    consumes Item& x
	) is_abstract;
    /*!
	ensures
	    self = <#x> * #self 
    !*/

    procedure Pop (
	    produces Item& x
	) is_abstract;
    /*!
	requires
	    self /= empty_string
	ensures
	    #self = <x> * self
    !*/

    function Item& operator [] (
	    preserves Accessor_Position& current
	) is_abstract;
    /*!
	requires
	    self /= empty_string
	ensures
	    there exists a: string of Item
		(self = <self[current]> * a)
    !*/

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

};

#endif // AT_STACK_KERNEL