Блог

Я пытаюсь создать инвариант цикла, чтобы проверить, имеют ли все элементы массива с четным индексом число 2 на них (программа для поиска простых чисел, на этом шаге она генерирует SPF).

Однако, когда я попробую это:

 /*@ loop invariant (forall integer j; (4<=j<i amp;amp; 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.

 

Я действительно не могу понять, что здесь происходит, но я очень ценю любую помощь

Проблема здесь в том, что 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.