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

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

#ifndef CT_QUEUE_SORT_3
#define CT_QUEUE_SORT_3 1

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

#include "AT/Queue/Sort.h"
/*!
    #include "AT/General/Are_In_Order.h"
    #include "AT/Queue/Kernel.h"
!*/

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

concrete_template <
	concrete_instance class Item,
	concrete_instance utility_class Item_Are_In_Order,
	/*!
	    implements
		abstract_instance General_Are_In_Order <Item>
	!*/
	concrete_instance class Queue_Base
	/*!
	    implements
		abstract_instance Queue_Kernel <Item>
	!*/
    >
class Queue_Sort_3 :
    implements
	abstract_instance Queue_Sort <Item>,
    extends
	concrete_instance Queue_Base
{
private:

    local_procedure_body Partition (
            consumes Queue_Sort_3& q,
            preserves Item& p,
            alters Queue_Sort_3& q1,
            alters Queue_Sort_3& q2
        )
    /*!
	requires
	    q1 = empty_string  and
	    q2 = empty_string
	ensures
	    (q1 * q2) is permutation of #q  and
	    for all x: Item
		    where (x is in elements (q1))
		(ARE_IN_ORDER (x, p))  and
	    for all x: Item
		    where (x is in elements (q2))
		(not ARE_IN_ORDER (x, p))
    !*/
    {
       //-------- for students to fill in --------
    }

    local_procedure_body Combine (
            alters Queue_Sort_3& q,
	    consumes Item& p,
	    consumes Queue_Sort_3& q1,
	    consumes Queue_Sort_3& q2
	)
    /*!
	requires
	    q = empty_string
	ensures
	    q = #q1 * <#p> * #q2
    !*/
    {
       //-------- for students to fill in --------
    }

public:
    
    procedure_body Sort ()
    {
       //-------- for students to fill in --------
    }

};

#endif // CT_QUEUE_SORT_3