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

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

#ifndef AT_LIST_RETREAT
#define AT_LIST_RETREAT 1

///------------------------------------------------------------------------
/// Global Context --------------------------------------------------------
///------------------------------------------------------------------------

#include "AT/List/Kernel.h"

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

abstract_template <
	concrete_instance class Item
    >
class List_Retreat :
    extends
	abstract_instance List_Kernel <Item>
{
public:

    procedure Retreat () is_abstract;
    /*!
	requires
	    self.left /= empty_string
	ensures
	    self.left * self.right = #self.left * #self.right and
	    |self.left| = |#self.left| - 1
    !*/

};

#endif // AT_LIST_RETREAT