Tempelate

template <class T, class TCompare>
class SortingMachine1
    //! SortingMachine1 is modeled by tuple of
    //!             contents:  FiniteMultiSet(T)
    //!             inserting: boolean
    //! exemplar self

    //! math operation IS_FIRST (
    //!          s: FiniteMultiSet(T),
    //!          x: T
    //!      ): boolean
    //!      definition
    //!          x is in s  and
    //!          for all y: Item where (y is in s)
    //!              (areOrdered (x, y))

    //! TCompare required to have an areOrdered operation:
    //!
    //! Boolean areOrdered (T& lhs, T& rhs)
    //! preserves lhs, rhs
    //!   areOrdered returns true iff the two items compared
    //!      are in order relative to each other.
    //!   lhs stands for left hand side
    //!   rhs stands for right hand side

{
public: // standard Operations
    SortingMachine1 ();
        //! alters self
        //! ensures: self.contents = { }  and  self.inserting = true
    ~SortingMachine1 ();
    void clear (void);
        //! alters self
        //! ensures: self.contents = { }  and  self.inserting = true
    void transferFrom(SortingMachine1& source);
        //! alters self, source
        //! ensures self = #source  and  source = self.contents = { }  and  self.inserting = true
    SortingMachine1& operator = (SortingMachine1& rhs);
        //! alters self
        //! preserves rhs
        //! ensures: self = rhs

    // SortingMachine1 Specific Operations
    void add (T& x);
        //! alters    self
        //! consumes x
        //! requires:  self.inserting
        //!  ensures: self.contents = #self.contents  union  {#x}  and
        //!       self.inserting = true
    void changeToExtractionMode (void);
        //! alters self
        //! requires:  self.inserting
        //!  ensures: self.inserting = false  and  self.contents = #self.contents
    void removeFirst (T& x);
        //! alters self
        //! produces x
        //! requires:  not self.inserting  and  self.contents != {}
        //!  ensures: IS_FIRST (#self.contents, x)  and
        //!       self.contents = #self.contents / {x}  and
        //!       self.inserting = false
    Integer size (void);
        //! preserves  self
        //! ensures: size = |self.contents|
    Boolean isInInsertionMode (void);
        //! preserves  self
        //!  ensures: isInInsertionMode = self.inserting

private: // Representation
};