Realization Isabelle_Selection_Sort_Realiz(
      operation Are_Ordered(restores x,y: Entry): Boolean;
         ensures Are_Ordered = (LEQV(x,y));
      )for Isabelle_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 IsASmallest(#Q, min);
    Procedure 
	Var temp:Queue;
	Var x:Entry;

	Dequeue(min, Q);
	While (Length(Q) /= 0)
		changing Q, min, temp, x;
		maintaining IsPermutation(temp o Q o <min>,  #Q) and IsASmallest(temp o <min>, min);
		decreasing |Q|;
	do
		Dequeue(x, Q);
		If Are_Ordered(x, min) then
			min :=: x;
		end;
		Enqueue(x, temp);
	end;
	Q :=: temp;
    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 (for all y: Entry, if IsSubstring (<y>, Q) then IsNondecreasing(sorted o <y>));
		decreasing |Q|;
	do
		Remove_Min(Q, min);
		Enqueue(min, sorted);
	end;	
	Q :=: sorted;

    end Sort_Q;
end Isabelle_Selection_Sort_Realiz;