Add leading zeros in floating point variable

Shell Programming and Scripting
1

I need to add leading zeros in a floating point numbers.
The length of the number should be 13 including decimal.
The input number is changing so number of leading zeros is not fix.

For example
input output
216.000 000000216.000
1345.000 000001345.000
22345.500 000022345.500

How can i do this in bash shell scripting.
kindly suggest.

Thanks in advance.

2 
awk '{printf "%013.3f\n" ,$1}' infile

000000216.000
000001345.000
000022345.500
3

Thanks for the quick reply.
But i am passing these values to a function and there i used the awk command mentioned by you(pay_amount=`awk '{printf "%013.3f\n" ,$1}'$4 `) ,its showing
awk: syntax error near line 1
awk: bailing out near line 1

Kindly suggest

4

Use nawk or /usr/xpg4/bin/awk on Solaris.

5

Another way would be..

cat inputfile | xargs printf "%013.3f\n"