Formal methods applied to a floating-point number system

Author

Barrett, Geoff

Author_Institution

Programming Res. Group, Oxford Univ., UK

Volume

15

Issue

5

fYear

1989

fDate

5/1/1989 12:00:00 AM

Firstpage

611

Lastpage

621

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;

fLanguage

English

Journal_Title

Software Engineering, IEEE Transactions on

Publisher

ieee

ISSN

0098-5589

Type

jour

DOI

10.1109/32.24710

Filename

24710