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

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

#ifndef AT_SORTING_MACHINE_KERNEL
#define AT_SORTING_MACHINE_KERNEL 1
    
///------------------------------------------------------------------------
/// Global Context --------------------------------------------------------
///------------------------------------------------------------------------

/*!
    #include "AT/General/Are_In_Order.h"
!*/

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

abstract_template <
        concrete_instance class Item,
        concrete_instance utility_class Item_Are_In_Order
        /*!
            implements
                abstract_instance General_Are_In_Order <Item>
	!*/
    >
class Sorting_Machine_Kernel
{
public:

    /*!
	math subtype SORTING_MACHINE_MODEL is (
		inserting: boolean
		contents: finite multiset of Item
	    )

	math definition IS_FIRST (
		s: finite multiset of Item,
		x: Item
	    ): boolean is
	    x is in s  and
	    for all y: Item where (y is in s)
		(ARE_IN_ORDER (x, y))
    !*/
	
    standard_abstract_operations (Sorting_Machine_Kernel);
    /*!
	Sorting_Machine_Kernel is modeled by SORTING_MACHINE_MODEL
	initialization ensures
            self = (true, empty_multiset)
    !*/

    procedure Insert (
	    consumes Item& x
	) is_abstract;
    /*!
	requires
	    self.inserting = true
	ensures
	    self = (true, #self.contents union {#x})
    !*/
    
    procedure Change_To_Extraction_Phase () is_abstract;
    /*!
	requires
	    self.inserting = true
	ensures
	    self = (false, #self.contents)
    !*/
    
    procedure Remove_First (
	    produces Item& x
	) is_abstract;
    /*!
	requires
	    self.inserting = false  and
	    self.contents /= empty_multiset
	ensures
	    IS_FIRST (self.contents, x)  and
	    self = (false, #self.contents - {x})
    !*/
    
    procedure Remove_Any (
	    produces Item& x
	) is_abstract;
    /*!
	requires
	    self.contents /= empty_multiset
	ensures
	    x is in #self.contents  and
	    self = (#self.inserting, #self.contents - {x})
    !*/
    
    function Boolean Is_In_Extraction_Phase () is_abstract;
    /*!
	ensures
	    Is_In_Extraction_Phase = not self.inserting
    !*/
    
    function Integer Size () is_abstract;
    /*!
	ensures
	    Size = |self.contents|
    !*/

};

#endif // AT_SORTING_MACHINE_KERNEL