Numerical programs may require a high level of guarantee. This can be achieved by applying formal methods, such as machine-checked proofs. But these tools handle mathematical theorems while we are interested in C code, in which numerical computations are performed using floating-point arithmetic, whereas proof tools typically handle exact real arithmetic. To achieve this high level of confidence on C programs, we use a chain of tools: Frama-C, its Jessie plugin, Why and provers among Coq, Gappa, Alt-Ergo, CVC3 and Z3. This approach requires the C program to be annotated: each function must be precisely specified, and we prove the correctness of the program by proving both that it meets its specifications and that no runtime error may occur. The purpose of this paper is to illustrate, on various examples, the features of this approach.
展开▼
机译：数值程序可能需要高水平的保证。这可以通过应用正式方法（例如机器检查的证明）来实现。但是当我们对C代码感兴趣时，这些工具处理数学定理，在C代码中，使用浮点算术执行数值计算，而证明工具通常处理精确的实数算术。为了获得对C程序的高度信任，我们使用了一系列工具：Frama-C，其Jessie插件，Cohy，Gappa，Alt-Ergo，CVC3和Z3的Why and provers。这种方法要求对C程序进行批注：必须精确指定每个函数，并且我们通过证明该程序符合其规范并且不会发生运行时错误来证明该程序的正确性。本文的目的是在各种示例上说明此方法的功能。
展开▼
