Formal methods applied to a floating-point number system
The work
| Authors | Geoff Barrett |
|---|---|
| Editors | |
| Type | article |
| Year | 1989 |
| Citekey | barrett1989formal |
Where it appeared
| Published in | IEEE Transactions on Software Engineering |
|---|---|
| Publisher | IEEE Computer Society |
| Volume | 15 |
| Issue | 5 |
| Pages | 611--621 |
Identifiers
| DOI | 10.1109/32.24710 |
|---|---|
| OpenAlex | W2157279226 |
Access
| Landing page | https://doi.org/10.1109/32.24710 |
|---|
Empty on purpose
| copy |
Related
| Distinct from | barrett1987formal |
|---|---|
| Distinct from | gibbons1993formal |
| Distinct from | jacobi2002formal |
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
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.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-09-15 18:22 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Cite it as
@article{barrett1989formal,
title = {Formal methods applied to a floating-point number system},
author = {Geoff Barrett},
year = {1989},
journal = {IEEE Transactions on Software Engineering},
publisher = {IEEE Computer Society},
volume = {15},
number = {5},
pages = {611--621},
doi = {10.1109/32.24710},
}
This record lives at https://refs.drheap.org/barrett1989formal/ and will keep doing so.