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

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

#ifndef AT_QUEUE_KERNEL
#define AT_QUEUE_KERNEL 1

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

abstract_template <
	concrete_instance class Item
    >
class Queue_Kernel
{
public:

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

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

    procedure Dequeue (
	    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_QUEUE_KERNEL