re: round to 0 or 5 at the 3 decimal place

[J Naman]

*Step-by-step:*
x=0.128765
r=100*x; ## r=12.8765
i=int(r) ## i=12.000
i+=.5*(i<int(r+.5)) # # i+=.5 in this case: 12<13.3765
x=i/100; ## x=0.125
printf("%.3d", x ...)

You can write your own awk function roundto05(x);

I used to give this problem as a homework assignment to my students.