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

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

#ifndef CT_ARRAY_PUT_TO_1
#define CT_ARRAY_PUT_TO_1 1

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

#include "AT/General/Put_To.h"

/*!
    #include "AT/Array/Kernel.h"
!*/

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

concrete_template <
	concrete_instance class Item,
	/*!
	    implements
		abstract_instance General_Put_To <Item>
	!*/
	concrete_instance class Array_Base
	/*!
	    implements
		abstract_instance Array_Kernel <Item>
	!*/
    >
class Array_Put_To_1 :
    extends
	concrete_instance Array_Base,
    implements
	abstract_instance General_Put_To <Array_Base>
{
public:
    
    procedure_body Put_To (
	    alters Character_OStream& outs
	)
    {
	object Integer i;
    
	// Open scope of tuple

	outs.Open_Scope ("(");

	// Put lower bound and upper bound

	outs.New_Line ();
	outs << self.Lower_Bound () << ", " << self.Upper_Bound () << ",";
    
	// Open scope of set
    
	outs.Open_Scope ("{");

	// Put contents of self

	i = self.Lower_Bound ();
	while (i <= self.Upper_Bound ())
	/*!
	    alters self, i
	    maintains
		self.lb <= i <= self.ub + 1  and
		for all k: integer, x: Item
			where (self.lb <= k < i  and  (k,x) is in self.table)
		    ([pair (k,x) has been output])
	    decreases
	        self.ub + 1 - i
	!*/
	{
	    outs.New_Line ();
	    outs << i << " --> " << self[i];
	    i++;
	}

	// Close scope of set
    
	outs.Close_Scope ("}");
    
	// Close scope of tuple
    
	outs.Close_Scope (")");
    }

};

#endif // CT_ARRAY_PUT_TO_1