Вы должны использовать класс FORMAT_DOUBLE
local
fd: FORMAT_DOUBLE
do
create fd.make (5, 3)
print (fd.formatted ({REAL_64} 12345.6789)) --> "12345.679"
print (fd.formatted ({REAL_64} 12345.6)) --> "12345.600"
print (fd.formatted ({REAL_64} 0.6)) --> "0.600"
create fd.make (10, 2)
fd.right_justify
print (fd.formatted ({REAL_64} 1.678)) --> " 1.68"
create fd.make (20, 3)
fd.right_justify
print ("[" + fd.formatted ({REAL_64} 12345.6789) + "]%N") --> [ 12345.679]
fd.left_justify
print ("[" + fd.formatted ({REAL_64} 12345.6789) + "]%N") --> [12345.679 ]
fd.center_justify
print ("[" + fd.formatted ({REAL_64} 12345.6789) + "]%N") --> [ 12345.679 ]
И так далее ...
Существует также набор классов для имитации "printf", вы можете найти их в http://www.amalasoft.com/downloads.htm Я не использовал их сам, но это могло бы удовлетворить ваши потребности.
Это использует ECMA Eiffel (я не уверен, откуда взялся предыдущий ответ, но DOUBLE не имеет такой функции `to_string_format '. И DOUBLE - это старое имя для REAL_64