0

我正在用 frama-c 测试这个小程序，但我一直收到同样的错误。我不确定这意味着什么。我对分配一切意味着什么感到特别困惑。

这是带有 ACSL 注释的代码：

// assuming n is nonnegative and even, f returns n

/*@ requires n>=0;
*/

int f(int n) {
  int i=0;
  while (i<n) {
    i+=2;
  }
  //@ assert i==n;
  return i;
}

这是我尝试测试代码时终端所说的内容：

[wp] warning: Missing RTE guards
p3.c:9:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_assert : Unknown (Qed:8ms) (54ms)
[wp] Proved goals:    0 / 1
    Alt-Ergo:        0  (unknown: 1)
4

1 回答 1

4

首先，您的属性不正确，因为您甚至不需要n处于函数的先决条件。因此，我将向您展示如何i += 1在循环体中证明您的程序的变体。

该assigns子句是 WP 要求您为每个循环和每个外部函数调用指定的内容。它必须包含可以被循环（或函数）修改的所有内存位置（即变量）的列表。它需要这个才能知道循环不会修改其他所有内容。特别是，在这个程序中，WP 需要知道，虽然 的值i可能会在循环中改变，但 的值n不会改变。但是，如果您不告诉它是这种情况，它会假定循环可以分配“一切”，包括n.

要指定这一点，您可以在循环上方插入以下注释：

/*@ loop assigns i; */

如果您尝试证明这一点（在 GUI 中），您将看到 WP 可以验证此分配子句。

但是，您在循环之后的断言仍然不能用这个来证明。这是因为除了 assigns 子句之外，每个循环还必须有一个循环不变量：在循环的每次迭代之前和之后始终为真的东西。选择正确且足够强大的循环不变量是一门黑暗的艺术，但一般来说，不变量必须是这样的，一旦循环条件为假并且循环终止，我们就可以在循环之后得出断言。

也就是说，我们想要一个I具有以下属性的公式作为不变式：

I && !(i < n)  ==>  i == n

因此，一个不错的选择是循环不变量i <= n，因为如果i <= n但我们知道这i < n不是真的（因为循环已经停止迭代），那么i必须等于n。

将所有内容放在一起，这是您的程序的注释变体：

/*@ requires n>=0;
*/

int f(int n) {
  int i=0;
  /*@ loop assigns i;
    @ loop invariant i <= n;
   */
  while (i<n) {
    i += 1;
  }
  //@ assert i==n;
  return i;
}

这是自动验证的：

[wp] warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] Proved goals:    4 / 4
    Qed:             4
于 2018-04-12T19:54:30.370 回答