Defining the IEEE-854 Floating-Point Standard in PVS
Defining the IEEE-854 Floating-Point Standard in PVS
复制标题
在 PVS 中定义 IEEE-854 浮点标准
DOI：
--
复制
发表时间：
1995
期刊：
影响因子：
--
通讯作者：
Miner
中科院分区：
文献类型：
--
作者：
Paul;S.;Miner
ANSI/IEEE-854标准的一个重要部分是在PVS（原型验证系统）中定义的。由于IEEE-854是ANSI/IEEE-754二进制浮点运算标准的推广，因此PVS中IEEE-854的定义也正式定义了IEEE-754的大部分内容。这些PVS理论为浮点系统的机器检查验证提供了基础。这个形式化定义说明了形式化规范技术已经足够先进，在未来的标准开发中考虑使用它们是合理的。
A significant portion of the ANSI/IEEE-854 Standard for Radix-Independent Floating-Point Arithmetic is defined in PVS (Prototype Verification System). Since IEEE-854 is a generalization of the ANSI/IEEE-754 Standard for Binary Floating-Point Arithmetic, the definition of IEEE-854 in PVS also formally defines much of IEEE-754. This collection of PVS theories provides a basis for machine checked verification of floating-point systems. This formal definition illustrates that formal specification techniques are sufficiently advanced that it is reasonable to consider their use in the development of future standards.