Formal methods applied to a floating-point number system

Abstract-This paper presents a formalization of the IEEE standard for binary floating-point arithmetic 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 devel-opment. In the course of the proofs, useful internal representations of floating-point numbers are specified. The procedures which are pre-sented here form the basis for the floating-point unit of the inmos IMS T800 transputer. Index Terms-Floating-point arithmetic, formal specification, pro-gram derivation, refinement, transputer, Z. I