Why is the guard invalid in this loop invariant

Question

I'm trying to create a loop invariant to check if all the elements of an array with an even index have the number 2on them (program to find prime numbers, in this step it's generating the SPF).

However, when I try this:

/*@ 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;
  }

I get the following error:

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.

I really can't understand what's happening here, but any help is much appreciated

Answer 1

The issue here is that E-ACSL does not instrument arbitrary quantified formulas, but only the ones it knows how to translate as a for loop. Basically, this means that it syntactically search for explicit bounds for the quantified variable (j in this case). For that, it will look whether the formula has the form \forall integer j; lower_bound <= j <= higher_bound ==> some_formula. Because your hypothesis on j adds the modulo constraint, it does not follow this pattern, hence its rejection by E-ACSL. To avoid this problem, you can rewrite it as:

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

this is logically equivalent (in both cases, j must lie between 4 and i and be even for primes[j] to be equal to 2), but now fits in the pattern E-ACSL is looking for.