Eliminating Unstable Tests in Floating-Point Programs
Eliminating Unstable Tests in Floating-Point Programs
复制标题
消除浮点程序中的不稳定测试
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Mariano M. Moscato
中科院分区：
文献类型：
--
作者：
Laura Titolo;C. Muñoz;Marco A. Feliú;Mariano M. Moscato
由实数及其浮点数表示之间的差异引起的圆形误差导致条件浮点声明的控制流偏离了实数计算的理想流动。这个问题称为测试不稳定性，可能会导致浮点程序的计算与实际算术中的预期输出之间存在显着差异。在本文中，提出了一个正式验证的程序转换，以检测和纠正不稳定测试的影响。此转换的输出是一个浮点程序，当可以确保其真实和浮点流量同时同意其真实和浮点数时，可以保证返回原始浮点程序的结果。通过在NASA开发的多边形遏制算法的核心计算的转换来说明了所提出的方法，该算法用于无人飞机系统的地理申请系统中。
Round-off errors arising from the difference between real numbers and their floating-point representation cause the control flow of conditional floating-point statements to deviate from the ideal flow of the real-number computation. This problem, which is called test instability, may result in a significant difference between the computation of a floating-point program and the expected output in real arithmetic. In this paper, a formally proven program transformation is proposed to detect and correct the effects of unstable tests. The output of this transformation is a floating-point program that is guaranteed to return either the result of the original floating-point program when it can be assured that both its real and its floating-point flows agree or a warning when these flows may diverge. The proposed approach is illustrated with the transformation of the core computation of a polygon containment algorithm developed at NASA that is used in a geofencing system for unmanned aircraft systems.