Realization Sort_Realiz(
      operation Are_Ordered(restores x,y: Entry): Boolean;
         ensures Are_Ordered = (LEQV(x,y));
      )for Sort_Capability of Queue_Template;
    uses Std_Boolean_Fac, Std_Integer_Fac;


   Operation Remove_Min(updates Q: Queue; replaces min: Entry);
      requires |Q| /= 0;
      ensures IsPermutation(Q o <min>, #Q) and IsPreceding(<min>, Q);
    Procedure 
	Var NewQ:Queue;
	Var E:Entry;

	Dequeue(min, Q);
	While (Length(Q) /= 0)
		changing Q, min, NewQ, E;
		maintaining IsPermutation(NewQ o Q o <min>,  #Q) and IsPreceding(<min>, NewQ);
		decreasing |Q|;
	do
		Dequeue(E, Q);
		If Are_Ordered(E, min) then
			min :=: E;
		end;
		Enqueue(E, NewQ);
	end;
	Q :=: NewQ;
    end Remove_Min;

    Procedure Sort_Q(updates Q: Queue);
	Var sorted:Queue;
	Var min:Entry;
 	While (Length(Q) /= 0)
		changing Q, sorted, min;
		maintaining IsPermutation(Q o sorted, #Q) and IsNonDecreasing(sorted) and IsPreceding(sorted, Q);
		decreasing |Q|;
	do
		Remove_Min(Q, min);
		Enqueue(min, sorted);
	end;	
	Q :=: sorted;

    end Sort_Q;
end Sort_Realiz;