涉及舍入运算符的表达式界限的验证
摘要：Gappa使用区间算术来验证涉及舍入和精确操作符的数学表达式的边界。 Gappa为每个处理的边界生成带有其证明的定理。该证明可以使用高阶逻辑自动证明检查器（Coq或HOL Light）进行检查，我们还开发了一个大型伴随库，其中包含用于Coq的经过验证的附加事实，涉及加法，乘法，除法和平方根，以及固定点和浮点算术。 Gappa使用多精度二进制小数来表示区间的端点，并在必要时对舍入操作符进行前向误差分析。当要求时，Gappa报告对于给定上下文中给定表达式能够达到的最佳边界。这一特性用于快速获取粗略边界。它还可以用于确定Gappa中实施的事实和自动技术集合不足的地方。 Gappa可以无缝处理额外的属性，这些属性可以用区间属性或重写规则表示，以建立更复杂的边界。最近的工作表明，Gappa非常适合于证明小型软件的正确性。设计师可以编写证明义务，由第三方工具生成或通过重载算术运算符获得。
作者：Marc Daumas (LIRMM, LP2A), Guillaume Melquiond (LIP, INRIA Rh^one-Alpes)
论文ID：cs/0701186
分类：Mathematical Software
分类简称：cs.MS
提交时间：2007-06-13