Implementing a Rigorous ODE Solver Through Literate Programming
Implementing a Rigorous ODE Solver Through Literate Programming
复制标题
通过文字编程实现严格的 ODE 求解器
DOI：
10.1007/978-3-642-15956-5_1
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
N. Nedialkov
中科院分区：
文献类型：
--
作者：
N. Nedialkov
区间数值方法产生的结果可以具有数学证明的力量。虽然有大量的理论工作，这些方法，几乎没有做，以确保一个区间方法的实施可以很容易地验证。然而，当要求严格的数值结果时，确保计算中没有错误是至关重要的。此外，当在计算机辅助证明中使用这种方法时，期望以便于人类专家验证的形式公布其实现。我们已经应用Literate Programming（LP）生成了VNODE-LP，这是一个C++求解器，用于计算常微分方程（ODE）初值问题（IVP）解的严格边界。我们发现LP非常适合确保数值算法的实现是将其基础理论正确转换为编程语言：我们可以把理论分成若干小块，逐个翻译，并把数学表达式和相应的代码紧密地放在一个统一的文件中。然后，它可以由人类专家审查和检查其正确性，类似于科学工作在同行评审过程中的审查方式。
Interval numerical methods produce results that can have the power of a mathematical proof. Although there is a substantial amount of theoretical work on these methods, little has been done to ensure that an implementation of an interval method can be readily verified. However, when claiming rigorous numerical results, it is crucial to ensure that there are no errors in their computation. Furthermore, when such a method is used in a computer assisted proof, it would be desirable to have its implementation published in a form that is convenient for verification by human experts. We have applied Literate Programming (LP) to produce VNODE-LP, a C++ solver for computing rigorous bounds on the solution of an initial-value problem (IVP) for an ordinary differential equation (ODE).We have found LP well suited for ensuring that an implementation of a numerical algorithm is a correct translation of its underlying theory into a programming language: we can split the theory into small pieces, translate each of them, and keep mathematical expressions and the corresponding code close together in a unified document. Then it can be reviewed and checked for correctness by human experts, similarly to how a scientific work is examined in a peer-review process.