我正在尝试创建一个循环不变量来检查具有偶数索引的数组的所有元素是否都有数字 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.
我真的不明白这里发生了什么,但非常感谢任何帮助