//  /*-------------------------------------------------------------------*\
//  |   Concrete Template : Sequence_Kernel_1a_C (HOW NOT TO DO IT!)
//  \*-------------------------------------------------------------------*/

#ifndef CT_SEQUENCE_KERNEL_1A_C
#define CT_SEQUENCE_KERNEL_1A_C 1

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

#include "CT/Sequence/Kernel_1a.h"

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

concrete_template <
	concrete_instance class Item
    >
class Sequence_Kernel_1a_C :
    checks
	concrete_instance Sequence_Kernel_1a <Item>
{
public:
    
    procedure_body Add (
	    preserves Integer pos,
	    consumes Item& x
	)
    {
	assert (0 <= pos,
		"0 <= pos");
	assert (pos <= self.Length (),
		"pos <= |self|");
	self.Sequence_Kernel_1a<Item>::Add (pos, x);
    }  

    procedure_body Remove (
	    preserves Integer pos,
	    produces Item& x
	)
    {
	assert (0 <= pos,
		"0 <= pos");
	assert (pos < self.Length (),
		"pos < |self|");
	self.Sequence_Kernel_1a<Item>::Remove (pos, x);
    }  

    function_body Item& operator [] (
	    preserves Integer pos
	)
    {
	assert (0 <= pos,
		"0 <= pos");
	assert (pos < self.Length (),
		"pos < |self|");
	return self.Sequence_Kernel_1a<Item>::operator [] (pos);
    }

};

#endif // CT_SEQUENCE_KERNEL_1A_C