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

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

#ifndef AT_LIST_KERNEL
#define AT_LIST_KERNEL 1
    
///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

abstract_template <
	concrete_instance class Item
    >
class List_Kernel
{
public:

    standard_abstract_operations (List_Kernel);
    /*!
	List_Kernel is modeled by (
                left:  string of Item
                right: string of Item
            )
	initialization ensures
            self = (empty_string, empty_string)
    !*/

    procedure Add_Right (
	    consumes Item& x
	) is_abstract;
    /*!
	ensures
	    self.left = #self.left  and
	    self.right = <#x> * #self.right
    !*/

    procedure Remove_Right (
	    produces Item& x
	) is_abstract;
    /*!
	requires
	    self.right /= empty_string
	ensures
	    self.left = #self.left and
	    #self.right = <x> * self.right
    !*/

    function Item& operator [] (
	    preserves Accessor_Position& current
	) is_abstract;
    /*!
	requires
	    self.right /= empty_string
	ensures
	    self.left = #self.left  and
	    there exists a: string of Item
		(self.right = <self[current]> * a)
    !*/
    
    procedure Advance () is_abstract;
    /*!
	requires
	    self.right /= empty_string
	ensures
	    self.left * self.right = #self.left * #self.right and
	    |self.left| = |#self.left| + 1
    !*/

    procedure Move_To_Start () is_abstract;
    /*!
	ensures
	self.right = #self.left * #self.right and
	|self.left| = 0
    !*/

    procedure Move_To_Finish () is_abstract;
    /*!
	ensures
	    self.left = #self.left * #self.right and
	    |self.right| = 0
    !*/
    
    function Integer Left_Length () is_abstract;
    /*!
	ensures
	    Left_Length = |self.left|
    !*/
    
    function Integer Right_Length () is_abstract;
    /*!
	ensures
	    Right_Length = |self.right|
    !*/    
    
};

#endif // AT_LIST_KERNEL