介绍ACSL/Frama-C的数学函数规范

Question

是否可以在ACSL中为通常在-lm编译时调用的函数实现规范，如sqrt？我把它用于Frama的插件WP。

这里有一个小例子来说明我想做什么。

/*@ requires sqrt_spec: \forall float x; 
             \model(sqrt(x)) * \model(sqrt(x)) == \model(x);  
    ensures [...] */  

void f (...) {
double y = sqrt x;
[...]
}

显然，如果我这样做，WP会哭，因为当我在注释中使用sqrt时，sqrt并不存在。

内核用户错误:注释中的未绑定函数sqrt

所以我想定义一个抽象的sqrt，但是我的测试都没有用：

#define sqrt(x) (...)

对于这件事，我看不出我能做什么(.)因为我想要一个抽象的定义，而不是重新实现整个浮动sqrt。

/*@  axiomatic SqrtSpec {
logic real sqrt (real x);
} */

而这次解决不了我的问题：

函数sqrt既没有代码也没有规范，从原型生成默认赋值。

Answer 1

Frama有一个内置逻辑函数\sqrt，它对real号进行操作(请注意，内置函数和谓词通常以反斜杠\作为前缀，以避免与现有C标识符发生冲突)。尽管如此，为sqrt提供一个公理定义并不难。

axiomatic Sqrt {
  logic real sqrt(real);
  axiom real_def: \forall real x; x >= 0 ==> x == sqrt(x) * sqrt(x);
}

另外，请注意，Gappa (http://gappa.gforge.inria.fr/)是唯一知道浮点(相对于实数)的自动验证程序，但是即使您已经安装了它，完成处理浮点计算的验证义务也是非常困难的。

更新

如果您想将double sqrt(double) (和/或float sqrt(float))公理化，其思想将是描述相对于在reals上操作的\sqrt结果的错误，即类似于

axiomatic Sqrt {
  logic float sqrt(float sqrt);
  axiom sqrt_def: \forall float x; \is_finite(x) && x>= 0.0 ==> sqrt(x) ==  (float)\sqrt(x);
}

当然，这种描述可能有点限制性。你可能想要像\abs(sqrt(x) - \sqrt(x)) <= err_bound * \sqrt(x)这样的东西，但我必须承认，我在浮点计算方面不够流利，无法从头顶上给出适当的err_bound值。

更新2

假设您有一个具有您想要的属性的逻辑 sqrt，那么说C sqrt具有相同的行为只是给它一个契约的问题：

/*@ requires \is_finite(x); //unless you want to play with NaN or infinities 
    assigns \nothing;
    ensures \result == sqrt(x);
 */
extern float sqrt(float x);

函数的规范在链接阶段被合并，所以这个契约是用math.h编写的(注意:在标准的标头sqrt中接受(并返回)一个double，是sqrtf在float上操作)还是在您自己的文件中。