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

//  /*-------------------------------------------------------------------*\
//  |   Concrete Template : List_Retreat_1
//  \*-------------------------------------------------------------------*/

#ifndef CT_LIST_RETREAT_1
#define CT_LIST_RETREAT_1 1

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

#include "AT/List/Retreat.h"
/*!
    #include "AT/List/Kernel.h"
!*/
   
///------------------------------------------------------------------------
/// Interface -------------------------------------------------------------
///------------------------------------------------------------------------

concrete_template <
	concrete_instance class Item,
	concrete_instance class List_Base
	/*!
	    implements
		abstract_instance List_Kernel <Item>
	!*/
    >
class List_Retreat_1 :
    extends
	concrete_instance List_Base,
    implements
	abstract_instance List_Retreat <Item>
{
public:
    
    procedure_body Retreat ()
    {
	object Integer desired_left_length = self.Left_Length () - 1;

	self.Move_To_Start ();
	while (self.Left_Length () < desired_left_length)
	/*!
	    alters self
	    preserves desired_left_length
	    maintains
	        self.left * self.right = #self.left * #self.right  and
	        |self.left| <= desired_left_length
	    decreases
	        |self.right|
	!*/
	{
	    self.Advance ();
	}
    }

};

#endif // CT_LIST_RETREAT_1