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

//  /*-------------------------------------------------------------------*\
//  |   Abstract Template : Queue_Sort
//  \*-------------------------------------------------------------------*/

#ifndef AT_QUEUE_SORT
#define AT_QUEUE_SORT 1

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

#include "AT/Queue/Kernel.h"

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

abstract_template <
	concrete_instance class Item
    >
class Queue_Sort :
    extends
	abstract_instance Queue_Kernel <Item>
{
public:
    
    /*!
	math definition ARE_IN_ORDER (
		x: Item,
		y: Item
	    ): boolean satisfies restriction
	    for all x, y, z: Item
		((ARE_IN_ORDER (x, y)  or  ARE_IN_ORDER (y, x))  and
		 (if (ARE_IN_ORDER (x, y)  and  ARE_IN_ORDER (y, z))
		  then ARE_IN_ORDER (x, z)))

        math definition IS_ORDERED (
		s: string of Item
	    ): boolean is
	    for all u, v: Item where (<u> * <v> is substring of s)
		(ARE_IN_ORDER (u, v))
    !*/

    procedure Sort () is_abstract;
    /*!
	ensures
	    self is permutation of #self  and
	    IS_ORDERED (self)
    !*/

};

#endif // AT_QUEUE_SORT