1

我正在尝试创建一个循环不变量来检查具有偶数索引的数组的所有元素是否都有数字 2（查找素数的程序，在此步骤中它正在生成 SPF）。

但是，当我尝试这个时：

/*@ loop invariant (\forall integer j; (4<=j<i && j%2==0 ==> prime[j]==2));
  */
  for (int i = 4; i <= n; i += 2) {
    prime[i] = 2;
  }

我收到以下错误：

Warning: 
  invalid E-ACSL construct
  `invalid guard 4 ≤ j < i_0 ∧ j % 2 ≡ 0 in quantification
  ∀ ℤ j; 4 ≤ j < i_0 ∧ j % 2 ≡ 0 ⇒ *(prime + j) ≡ 2'.
  Ignoring annotation.

我真的不明白这里发生了什么，但非常感谢任何帮助

4

1 回答 1

1

这里的问题是 E-ACSL 不检测任意量化的公式，而只检测它知道如何转换为for循环的那些。基本上，这意味着它在语法上搜索量化变量的显式边界（j在这种情况下）。为此，它将查看公式是否具有形式\forall integer j; lower_bound <= j <= higher_bound ==> some_formula。因为您的假设j添加了模约束，所以它不遵循这种模式，因此被 E-ACSL 拒绝。为避免此问题，您可以将其重写为：

\forall integer j; (4<=j<i ==> j%2==0 ==> primes[j]==2)

这在逻辑上是等价的（在这两种情况下，j必须介于4andi和 be even forprimes[j]等于2），但现在符合 E-ACSL 正在寻找的模式。

于 2021-10-25T06:43:46.283 回答