Title :
Formal methods applied to a floating-point number system
Author_Institution :
Programming Res. Group, Oxford Univ., UK
fDate :
5/1/1989 12:00:00 AM
Abstract :
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
Keywords :
digital arithmetic; specification languages; ANSI/IEEE Std. 754-1985; IEEE standard; Inmos IMS T800 transputer; Z; binary floating-point arithmetic; floating-point number system; floating-point unit; formal methods; formal specification; formalization; internal representations; mathematically rigorous method; operands; pack; program development; proven rules; round; sequential components; set-theoretic specification language; unpack; Algorithm design and analysis; Costs; Floating-point arithmetic; Formal specifications; Formal verification; Helium; Natural languages; Packaging; Specification languages; Testing;
Journal_Title :
Software Engineering, IEEE Transactions on
