含舍入算子的表达式上界的证明
Certification of bounds on expressions involving rounded operators
摘要：
Gappa使用区间算术来验证涉及舍入和精确运算符的数学表达式的界限。Gappa生成了一个定理，并证明了每一个被处理的界限。证明可以使用更高阶逻辑自动证明检查器（Coq或HOL Light）进行检查，并且我们为Coq开发了一个大型的已验证事实配套库，用于处理固定和浮点运算中的加法、乘法、除法和平方根。点算术。Gappa使用多精度并元分数作为区间的端点，并在必要时对舍入运算符进行前向误差分析。当被询问时，Gappa报告它在给定上下文中能够达到给定表达式的最佳边界。此功能用于快速获得粗略的边界。它还可以用来确定Gappa中实现的事实集和自动技术在哪里变得不足。Gappa无缝地处理以区间属性表示的附加属性或重写规则，以建立更复杂的边界。最近的工作表明，Gappa非常适合证明小型软件的正确性。证明义务可以由设计者编写、由第三方工具生成或通过重载算术运算符获得。
英文摘要：
Gappa uses interval arithmetic to certify bounds on mathematical expressions that involve rounded as well as exact operators. Gappa generates a theorem with its proof for each bound treated. The proof can be checked with a higher order logic automatic proof checker, either Coq or HOL Light, and we have developed a large companion library of verified facts for Coq dealing with the addition, multiplication, division, and square root, in fixed- and floating-point arithmetics. Gappa uses multiple-precision dyadic fractions for the endpoints of intervals and performs forward error analysis on rounded operators when necessary. When asked, Gappa reports the best bounds it is able to reach for a given expression in a given context. This feature is used to quickly obtain coarse bounds. It can also be used to identify where the set of facts and automatic techniques implemented in Gappa becomes insufficient. Gappa handles seamlessly additional properties expressed as interval properties or rewriting rules in order to establish more intricate bounds. Recent work showed that Gappa is perfectly suited to the proof of correctness of small pieces of software. Proof obligations can be written by designers, produced by third-party tools or obtained by overloading arithmetic operators.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
