local_procedure_body Initialize ()
    {
        self[inserting_rep] = true;
    }

    local_procedure_body Partition (
	    consumes Queue_Of_Item& q,
            preserves Item& p,
            produces Queue_Of_Item& q1,
            produces Queue_Of_Item& q2
        )
    /*!
	ensures
	    q1 * q2 is permutation of #q and
		    for all x: integer where (x is in elements (q1))
		(ARE_IN_ORDER(x, p))  and
	    for all x: integer where (x is in elements (q2))
		(not ARE_IN_ORDER(x, p))
    !*/
    {
	q1.Clear();
	q2.Clear();
        while (q.Length > 0)
	{
	  object Item temp;
	  q.Dequeue (temp);
	  if (Item_Are_In_Order::Are_In_Order (p, temp))
    	  {
      	    q2.Enqueue(temp);
    	  }
    	  else
    	  {
      	    q1.Enqueue(temp);
    	  }
  	}
    }

    local_procedure_body Combine (
            produces Queue_Of_Item& q,
            consumes Item& p,
            consumes Queue_Of_Item& q1,
            consumes Queue_Of_Item& q2
        )
    /*!
	ensures
	    q = #q1 * <#p> * #q2
    !*/
    {
        object Integer temp;  // used in the loop
  	q &= q1;
	q1.Clear();
 	q.Enqueue(p);
 	while (q2.Length() > 0)
  	{
   	  q2.Dequeue(temp);
   	  q.Enqueue(temp);
  	}
    }

    local_procedure_body Sort (
            alters Queue_Of_Item& q
        )
    /*!
	ensures
	    q is permutation of #q  and
	    IS_ORDERED (q)
	decreases
	    |q|
    !*/
    {
        if (q.Length() > 1)
	{
	  object Item p;
	  q.Dequeue (p);
	  object Queue_Of_Item q1, q2;
	  Partition (q, p, q1, q2);
	  Sort (q1);
	  Sort (q2);
	  Combine (q, p, q1, q2);
	}
    }



public:

    standard_concrete_operations (Sorting_Machine_Kernel_3);

    procedure_body Insert (
	    consumes Item& x
	)
    {
        self[contents_rep].Enqueue (x);
    }

    procedure_body Remove_First (
	    produces Item& x
	)
    {
        self[contents_rep].Dequeue (x);
    }

    procedure_body Remove_Any (
	    produces Item& x
	)
    {
        self[contents_rep].Dequeue (x);
    }

    procedure_body Change_To_Extraction_Phase ()
    {
        self[inserting_rep] = false;
	Sort(self[contents_rep]);
    }

    function_body Boolean Is_In_Extraction_Phase ()
    {
        return not (self[inserting_rep]);
    }

    function_body Integer Size ()
    {
        return self[contents_rep].Length();
    }

};