repeat_string(a_string: STRING; times: INTEGER): STRING
require
times_positive: times > 0
do
Result := a_string.multiply(times)
end