可在www.sciencedirect.com在线获取理论计算机科学电子笔记317（2015）101-107www.elsevier.com/locate/entcsHOL光的参数化浮点形式化Charles Jacobsena，1，2 Alexey Solovyeva，3，5 Ganesh Gopalakrishnana，4，5a犹他大学计算学院美国摘要我们提出了一个新的，开源的形式化的固定和浮点数的任意基数和精度，现在是HOL光分布的一部分[10]。我们证明了四种不同舍入模式的正确性和误差界，并通过将一个集合粘合在一起来形式化IEEE 754 [1]标准的子集固定点和浮动点的数字来表示次法线和法线。在我们的定点证明中，我们将定点数的相位视为不同精度的定点数的副本，以便我们可以重用定点舍入定理。保留字：IEEE-754-2008，迭代点，不动点，形式化1引言程序员需要计算错误界限的工具，并自动化繁琐和容易出错的推理，这些推理涉及到他们的浮点算法的正确性证明。它们遵循IEEE 754标准，因为大多数硬件和软件库都支持该标准，并提供具有多级精度的快速实现。作为采用该标准的示例，IntelCPU [13]上有四个精度级别，Nvidia GPU [2]上有三个精度级别，并且十进制浮点数在Cornea等人开发的软件包[7]的文件。但是，很难对浮点算法进行推理，因为浮点数和运算是实数的近似模型，1部分由NSF本科生研究经验（REU）支持，奖励CCF 1430497。2电子邮件：charlesj@cs.utah.edu3电子邮件：monad@cs.utah.edu4电子邮件：ganesh@cs.utah.edu5NSF Awards CCF 1421726和7298529的部分支持。http://dx.doi.org/10.1016/j.entcs.2015.10.0101571-0661/© 2015作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。102C. Jacobsen et al./理论计算机科学电子笔记317（2015）101共享理想的属性，如结合性，它们的实值对应物具有。程序员可能会错过产生大错误的边缘情况，错过通过重新排序操作来提高精度的方法，或者使用过于保守的精度。例如，Goualard [9]表明Intlab V5.5 [14]将μ报告为区间[−μ，μ]的中点而不是0，其中μ是最小的次正态数。虽然Intlab V5.5的设计者可能已经意识到了这种边缘情况，但它显示了浮点算法中的错误是多么我们提出了一个新的形式化的固定和浮点数，可用于推理程序，使用IEEE浮点数。[6]我们的工作是受John Harrison在HOL Light中对二进制浮点数的形式化的启发据我们所知，这种形式化不是公开的，也不像我们的那样使用固定点理论作为浮动点理论的基础。Daumas，Rideau，andTh'ery[8]andBoldoandMelquiond[4]已经在Coq中对任意基数和精度的固定点和旋转点的改进进行了改进。我们选择不使用Coq形式化，也不将它们转换为HOL Light，因为这些形式化既庞大又复杂，而我们的迫切需要只是形式化固定点和非固定点理论的一个子集。HOL Light还提供了非构造性的希尔伯特选择算子，这使得形式化更容易编写，因为我们二进制浮点的其他形式化已经在Z，PVS，HOL 4，Isabelle/HOL和ACL 2中完成[3，6，5，12，16，15]。据我们所知，Z形式化并不是公开的。其次，Isabelle/HOL形式化中的定理仅适用于单精度，不易推广。最后，我们的形式化不依赖于更高级别的操作和相应的理论，如ACL2中的实值地板2形式化概述我们将IEEE浮点数建模为R的子集。次正规数和零使用一组相隔固定距离的实数（定点数）表示正规数是用实数无限集合的一个子集来表示的，这些实数之间的距离是变化的（浮点数）。最后，我们把任何一个其大小超过一个精心选择的阈值的实数看作是浮点无穷大。我们不对符号零或NaN建模。以下各节将对每组进行更详细我们已经定义了四种舍入模式（舍入到最接近的偶数，舍入到零，舍入到正无穷大，舍入到负无穷大）中的定点数和定点数的舍入，并证明了舍入的基本性质，如（1 +δ）误差规则。C. Jacobsen et al./理论计算机科学电子笔记317（2015）101103图1.一、次正态数和零作为R的不动点数的子集的模型2.1次正规数与零在IEEE标准中，次正规数和零之间的距离是固定的re−p+1，其中r是基数，e是最小指数，p是精度，由格式决定。例如，对于二进制单精度，r为2，e为−126，p为24，固定距离为2 −149。 我们可以用一组实数来表示它们，它们的大小是f·re−p+1的形式，其中f∈N，0 ≤f0，所以零不包括在这组浮点数中。定义2.4Float（r，p）={x∈R：|X|=f·re−p+1， f∈N， e∈Z，0< f1，甚至p>1，并且emax≥emin，但没有其他IEEE限制（例如，Emin= −Emax+1）。我们将IEEE数的舍入形式化如下：对于任何实数x，如 果 is inf （ x ） 为 真 ， 则 舍 入 结果 就 是 x 。否 则 ， 我 们 使 用roundfixed 或roundfloat，这取决于x我们还没有证明IEEE舍入的正确性，但我们已经3总结发言在这项工作中，我们提出了一种新的固定和浮动点的形式化，这是当前HOL光分布的一部分。 我们认为，公开释放一个HOL光理论的浮动点将使HOL光社区工作在他们熟悉的框架，而不必诉诸交叉定理证明分析，目前不是很好地支持或发展。我们还计划在一个单独的项目中，研究定点计算中的舍入误差，以获得舍入误差的严格上限。我们计划将我们在该项目中的工作用于检查所报告错误的证明证书引用[1] IEEE标准的浮点运算。 IEEE标准754 -2008、2008年。[2] CUDA C编程指南 NVIDIA公司，2012年[3] 乔治·巴雷特。应用于浮点数系统的形式化方法。 软件工程，IEEE Transactions on，15（5）：611[4] 西尔维·博尔多和纪尧姆·梅尔奎昂。 Flocq：一个用于证明浮点算法的统一库在Coq。在计算机算术（ARITH）中，2011年第20届IEEE研讨会，第243-252页。IEEE，2011年。[5] 西尔维·博尔多和塞萨尔·穆尼奥斯。PVS中的一个高级形式化的迭代节点。美国宇航局/CR-2006-214298，美国宇航局，兰利研究中心，汉普顿弗吉尼亚州23681-2199，美国，2006年10月。[6] 维克多·A·卡瑞·恩卡洛和保罗·S·米纳。在HOL和PVS中的IEEE-854认证点标准的规范。高阶逻辑定理证明及其应用，1995。[7] Marius Cornea，John Harrison，Cristina Anderson，Peter Tang，Eric Schneider，and Evgeny Gvozdev.IEEE 754R十进制浮点运算的软件实现，使用二进制编码格式。计算机，IEEE Transactions on，58（2）：148[8] 我是道玛斯，劳伦斯·里多，还有劳伦·泰赫里。一个通用的插值函数库及其在精确计算中的应用。在高阶逻辑中的定理证明，第169-184页。施普林格，2001年。[9] 我是埃 里克·古拉尔。如 何 计 算 中间值的中点？ACMTransactionsonMathematical Software（TOMS），40（2）：11，2014.[10] 约翰·哈里森。HOL光：一个教程介绍. 计算机辅助设计中的形式方法，第265-269页。Springer，1996年。[11] 约翰·哈里森。浮点运算的机检理论。在高阶逻辑的定理证明，第113Springer，1999年。[12] HOL4中的浮点形式化。https://github.com/HOL-Theorem-Prover/HOL/tree/master/src/floating-point.[13] 在电话里。 英特尔®AVR®64和IA-32Archit ectu resSoftwa re Per's Manual. 2014年9月。C. Jacobsen et al./理论计算机科学电子笔记317（2015）101107[14] 齐格弗里德·M·朗普INTLAB-INTerval实验室Springer，1999年。[15] David M. Russino用ACL2对寄存器转移逻辑进行形式验证的一个实例研究AMD Athlon处理器的点加法器计算机辅助设计中的形式方法，第22-55页施普林格，2000年。[16] 雷雨。IEEE浮点运算的形式化模型Archive of Formal Proofs，2013年7月http://afp.sf.net/entries/IEEE_Floating_Point.shtml网站，正式证明发展。
我的内容管理
展开
