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

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

#ifndef AT_SEQUENCE_KERNEL
#define AT_SEQUENCE_KERNEL 1

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

abstract_template <
	concrete_instance class Item
    >
class Sequence_Kernel
{
public:
    
    standard_abstract_operations (Sequence_Kernel);
    /*!
	Sequence_Kernel is modeled by string of Item
	initialization ensures
            self = empty_string
    !*/

    procedure Add (
	    preserves Integer pos,
	    consumes Item& x
	) is_abstract;
    /*!
	requires
	    0 <= pos <= |self|
	ensures
	    there exists a, b: string of Item
		(|a| = pos  and
		 #self = a * b  and
		 self = a * <#x> * b)
    !*/

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

    function Item& operator [] (
	    preserves Integer pos
	) is_abstract;
    /*!
	requires
	    0 <= pos < |self|
	ensures
	    there exists a, b: string of Item
		(|a| = pos  and
		 #self = a * <self[pos]> * b)
    !*/

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

};

#endif // AT_SEQUENCE_KERNEL