4

是否可以在 ACSL 中为通常在使用 -lm 编译时调用的函数实现规范，如 sqrt ？我将它用于 Frama-C 的插件 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，但我的测试都没有工作：

#define sqrt(x) (...)

对于这个，我看不到我可以放入什么（...），因为我想要一个抽象定义而不是重新实现整个 float sqrt。

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

而这个并不能解决我的问题：

函数 sqrt 的代码和规范都没有，从原型生成默认分配。

4

1 回答 1

4

Frama-C 有一个内置的逻辑函数\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)），这个想法将是描述相对于对实数进行\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中接受（并返回） a double，它是sqrtf在 上操作float）还是在您自己的文件中都没有关系。

于 2014-06-24T19:02:50.893 回答