This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Methods Applied to a Floating-Point Number System
May 1989 (vol. 15 no. 5)
pp. 611-621

A formalization of the IEEE standard for binary floating-point arithmetic (ANSI/IEEE Std. 754-1985) is presented in the set-theoretic specification language Z. The formal specification is refined into four sequential components, which unpack the operands, perform the arithmetic, and pack and round the result. This refinement follows proven rules and so demonstrates a mathematically rigorous method of program development. In the course of the proofs, useful internal representations of floating-point numbers are specified. The procedures presented form the basis for the floating-point unit of the Inmos IMS T800 transputer.

[1] G. Barrett,Formal Methods Applied to Floating-Point Number System, Comput. Lab., Oxford Univ., Tech. Monograph PRG-58, 1987.
[2] W. S. Brown, "A simple but realistic model of floating-point computation,"ACM Trans. Math. Software, vol. 7, pp. 445-480, 1981.
[3] J. DuCroz and M. Pont, "The development of a floating-point validation package,"NAG Newslett., no. 3, pp. 3-9, 1984.
[4] I. Hayes, Ed.,Specification Case Studies (Series in Computer Science). Englewood Cliffs, NJ: Prentice-Hall International, 1987.
[5] M. B. Josephs, "Formal methods for stepwise refinement in the Z specification language," Comput. Lab., Oxford Univ., Internal Rep.
[6] A. Pentland, T. Darrell, M. Turk, and W. Huang," A simple, real-time range camera," inIEEE Comput. Soc. Conf. Comput. Vision Patt Recogn., 1989, pp. 256-261.
[7] N. L. Schryer, "A test of a computer's floating-point arithmetic unit," Bell Lab., Comput. Sci. Tech. Rep. No. 89, Feb. 1981.
[8] D. Shepherd, "Specification and development of a correct division algorithm," inmos Limited, Internal Rep., 1987.
[9] J.M. Spivey,Introducing Z: A Specification Language and its Formal Semantics, Cambridge Univ. Press, 1988.
[10] B. A. Wichmann, "Floating-point interval arithmetic for validation," NPL Rep. DITC 76/86, Oct. 1986.
[11] IEEE Standard for Binary Floating-Point Arithmetic. New York: ANSI/IEEE, Std. 754-1985, Aug. 1985.

Index Terms:
formal methods; floating-point number system; formalization; IEEE standard; binary floating-point arithmetic; ANSI/IEEE Std. 754-1985; set-theoretic specification language; Z; formal specification; sequential components; unpack; operands; pack; round; proven rules; mathematically rigorous method; program development; internal representations; floating-point unit; Inmos IMS T800 transputer; digital arithmetic; specification languages
Citation:
G. Barrett, "Formal Methods Applied to a Floating-Point Number System," IEEE Transactions on Software Engineering, vol. 15, no. 5, pp. 611-621, May 1989, doi:10.1109/32.24710
Usage of this product signifies your acceptance of the Terms of Use.