Issue No. 05 - May (1989 vol. 15)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.24710
<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>
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
G. Barrett, "Formal Methods Applied to a Floating-Point Number System," in IEEE Transactions on Software Engineering, vol. 15, no. , pp. 611-621, 1989.