The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - May (1989 vol.15)
pp: 611-621
ABSTRACT
<p>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.</p>
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
7 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool