Предупреждение Frama-C: отсутствует пункт assigns (вместо него назначается "все")

Question

Я тестирую эту маленькую программу с frama-c и продолжаю получать ту же ошибку. Я не уверен, что это значит. Я особенно запутался в том, что назначает все, что значит.

Вот этот код с аннотациями ACSL:

// assuming n is nonnegative and even, f returns n

/*@ requires n>=0;
*/

int f(int n) {
  int i=0;
  while (i<n) {
    i+=2;
  }
  //@ assert i==n;
  return i;
}

Вот что говорит терминал, когда я пытаюсь проверить код:

[wp] warning: Missing RTE guards
p3.c:9:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_f_assert : Unknown (Qed:8ms) (54ms)
[wp] Proved goals:    0 / 1
    Alt-Ergo:        0  (unknown: 1)

Answer 1

Прежде всего, ваша собственность не соответствует действительности, поскольку вы не требуете n быть даже в предварительном условии функции. Поэтому я покажу вам, как доказать вариант вашей программы с i += 1 в теле цикла.

assigns Предложение - это то, что WP требует, чтобы вы указали для каждого цикла и каждого вызова внешней функции. Он должен содержать список всех областей памяти (т. Е. Переменных), которые могут быть изменены циклом (или функцией). Это необходимо для того, чтобы знать, что все остальное не модифицируется циклом. В частности, в этой программе WP необходимо знать, что в то время как значение i может измениться в цикле, значение n не меняется. Но если вы не скажете ему, что это так, то предполагается, что цикл может назначить "все", включая n,

Чтобы указать это, вы можете вставить следующую аннотацию чуть выше цикла:

/*@ loop assigns i; */

Если вы попытаетесь доказать это (в графическом интерфейсе), вы увидите, что WP может проверить это назначение.

Тем не менее, ваше утверждение после цикла все еще не может быть доказано с этим. Это связано с тем, что в дополнение к предложению assigns каждый цикл должен также иметь инвариант цикла: то, что всегда верно до и после каждой итерации цикла. Выбор правильных и достаточно мощных инвариантов цикла является темным искусством, но в общем случае инвариант должен быть чем-то таким, что, если условие цикла ложно и цикл завершен, позволяет нам завершить утверждение после цикла.

То есть мы хотим в качестве инварианта формулы I имеет свойство, которое:

I && !(i < n)  ==>  i == n

Поэтому хорошим выбором является инвариант цикла i <= n так как если i <= n но мы знаем что i < n неверно (поскольку цикл перестал повторяться), тогда i должен быть равен n,

Собрав все воедино, вот аннотированный вариант вашей программы:

/*@ requires n>=0;
*/

int f(int n) {
  int i=0;
  /*@ loop assigns i;
    @ loop invariant i <= n;
   */
  while (i<n) {
    i += 1;
  }
  //@ assert i==n;
  return i;
}

И это проверяется автоматически:

[wp] warning: Missing RTE guards
[wp] 4 goals scheduled
[wp] Proved goals:    4 / 4
    Qed:             4