Someone

global_procedure Swap_Substring (
	alters Text& t1,
	preserves Integer pos,
	preserves Integer len,
	alters Text& t2
    );
    /*!
	requires
	    0 <= pos <= pos + len <= |t1|
	ensures
            there exists a, b: string of character
                (#t1 = a * t2 * b  and
                 |a| = pos  and
                 |t2| = len  and
                 t1 = a * #t2 * b)
    !*/