为什么这个循环中的保护无效

Question

我正在尝试创建一个循环不变量，以检查具有偶数索引的数组的所有元素上是否都有数字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.

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

Answer 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必须位于4和i之间，并且对于primes[j]等于2是偶数)，但现在符合E-ACSL所寻找的模式。