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

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

#ifndef CT_SEQUENCE_KERNEL_2
#define CT_SEQUENCE_KERNEL_2 1

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

#include "AT/Sequence/Kernel.h"
#include "CT/Queue/Kernel_1a.h"

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

concrete_template <
	concrete_instance class Item,
	concrete_instance class Queue_Of_Item =
            Queue_Kernel_1a <Item>,
	concrete_instance class Rep =
            Representation <
		    Queue_Of_Item,
		    Integer
		>
    >
class Sequence_Kernel_2 :
    implements
	abstract_instance Sequence_Kernel <Item>,
    encapsulates
	concrete_instance Rep
{
private:

    rep_field_name (Rep, 0, Queue_Of_Item, items);
    rep_field_name (Rep, 1, Integer, pos_at_front);

    /*!
	convention
	    if |self.items| > 0
		then 0 <= self.pos_at_front < |self.items|
		else self.pos_at_front = 0
		
	correspondence
	    there exists a, b: string of Item
		(self.items = b * a  and
		 |a| = self.pos_at_front  and
		 self = a * b)
    !*/
    
    local_procedure_body Rotate_Pos_To_Front (
	    alters Queue_Of_Item& s_items,
	    alters Integer& s_pos_at_front,
	    preserves Integer pos
	)
    /*!
	requires
	    |s_items| > 0  and
	    0 <= s_pos_at_front < |s_items|  and
	    0 <= pos < |s_items|
	ensures
	    s_pos_at_front = pos  and
	    there exists a, b, c, d: string of Item
		(|a| = #s_pos_at_front  and
		 #s_items = b * a  and
		 |c| = s_pos_at_front  and
		 s_items = d * c  and
		 a * b = c * d)
    !*/
    {
	while (s_pos_at_front != pos)
	/*!
	    alters s_items, s_pos_at_front
	    preserves pos
	    maintains
		there exists a, b, c, d: string of Item
		    (|a| = #s_pos_at_front  and
		     #s_items = b * a  and
		     |c| = s_pos_at_front  and
		     s_items = d * c  and
		     a * b = c * d)
	    decreases
	        (pos - s_pos_at_front) mod |s_items|
	!*/
	{
	    object catalyst Item x;

	    s_items.Dequeue (x);
	    s_items.Enqueue (x);
	    s_pos_at_front = (s_pos_at_front + 1) mod s_items.Length ();
	}
    }

public:

    standard_concrete_operations (Sequence_Kernel_2);

    procedure_body Add (
	    preserves Integer pos,
	    consumes Item& x
	)
    {
	if (self[items].Length () > 0)
	{
	    self.Rotate_Pos_To_Front (self[items], self[pos_at_front],
				      pos mod self[items].Length ());
	}
	self[items].Enqueue (x);
	self[pos_at_front] = (pos + 1) mod self[items].Length ();
    }  

    procedure_body Remove (
	    preserves Integer pos,
	    produces Item& x
	)
    {
	//-------- for students to fill in --------
    }

    function_body Item& operator [] (
	    preserves Integer pos
	)
    {
	//-------- for students to fill in --------
    }

    function_body Integer Length ()
    {
	//-------- for students to fill in --------
    }

};

#endif // CT_SEQUENCE_KERNEL_2