涉及舍入算子的表达式界的认证
数学软件
2007-06-13 v2
摘要
Gappa 使用区间算术来认证涉及舍入算子及精确算子的数学表达式的界。Gappa 为处理的每个界生成一个定理及其证明。该证明可以用高阶逻辑自动证明检查器（Coq 或 HOL Light）进行检查，并且我们为 Coq 开发了一个大型已验证事实的配套库，处理定点和浮点算术中的加法、乘法、除法和平方根。Gappa 对区间的端点使用多精度二进分数，并在必要时对舍入算子执行前向误差分析。当被要求时，Gappa 会报告其在给定上下文中能够为给定表达式达到的最佳界。此功能用于快速获取粗略的界。它也可用于识别 Gappa 中实现的事实集和自动技术何时变得不足。Gappa 无缝处理以区间属性或重写规则表达的附加属性，以建立更复杂的界。最近的工作表明，Gappa 非常适合用于证明小段软件的正确性。证明义务可以由设计者编写、由第三方工具产生或通过重载算术算子获得。
引用
@article{arxiv.cs/0701186,
title = {Certification of bounds on expressions involving rounded operators},
author = {Marc Daumas and Guillaume Melquiond},
journal= {arXiv preprint arXiv:cs/0701186},
year = {2007}
}