Как мне отладить ACSL в frama-c?

Я пытаюсь выучить ACSL, но пытаюсь написать полную спецификацию. Мой код

#include <stdint.h>
#include <stddef.h>

#define NUM_ELEMS (8)

/*@ requires expected != test;
  @ requires \let n = NUM_ELEMS;
  @          \valid_read(expected + (0.. n-1)) && \valid_read(test + (0.. n-1));
  @ assigns \nothing;
  @ behavior matches:
  @   assumes \let n = NUM_ELEMS;
  @           \forall integer i; 0 <= i < n ==> expected[i] == test[i];
  @   ensures \result == 1;
  @ behavior not_matches:
  @   assumes \let n = NUM_ELEMS;
  @           \exists integer i; 0 <= i < n && expected[i] != test[i];
  @   ensures \result == 0;
  @ complete behaviors;
  @ disjoint behaviors;
  @*/
int array_equals(const uint32_t expected[static NUM_ELEMS], const uint32_t test[static NUM_ELEMS]) {
  for (size_t i = 0; i < NUM_ELEMS; i++) {
    if (expected[i] != test[i]) {
      return 0;
    }
  }
  return 1;
}

Я запускаю это с

frama-c -wp -wp-rte test.c

и я вижу следующий журнал

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no preprocessing)
[kernel] Parsing test.c (with preprocessing)
[rte] annotating function array_equals
test.c:22:[wp] warning: Missing assigns clause (assigns 'everything' instead)
[wp] 9 goals scheduled
[wp] [Alt-Ergo] Goal typed_array_equals_assign_part1 : Unknown (Qed:2ms) (67ms)
[wp] [Alt-Ergo] Goal typed_array_equals_assert_rte_mem_access_2 : Unknown (Qed:2ms) (128ms)
[wp] [Alt-Ergo] Goal typed_array_equals_assert_rte_mem_access : Unknown (Qed:2ms) (125ms)
[wp] [Alt-Ergo] Goal typed_array_equals_matches_post : Unknown (Qed:10ms) (175ms)
[wp] [Alt-Ergo] Goal typed_array_equals_not_matches_post : Unknown (Qed:7ms) (109ms)
[wp] Proved goals:    4 / 9
     Qed:             4  (0.56ms-4ms)
     Alt-Ergo:        0  (unknown: 5)

Таким образом, кажется, что мои два поведения и "присваивает \ ничего" не могут быть доказаны. Так, как я продолжу отсюда?

РЕДАКТИРОВАТЬ: Таким образом, я понял непосредственную проблему. У меня нет аннотации к моей петле:

  /*@ loop invariant \let n = NUM_ELEMS; 0 <= i <= n;
    @ loop invariant \forall integer k; 0 <= k < i ==> expected[k] == test[k];
    @ loop assigns i;
    @ loop variant \let n = NUM_ELEMS; n-i;
    @*/

Мой большой вопрос все еще остается в силе: что является хорошим способом устранения проблем? Я решил эту проблему, просто изменив и удалив код и увидев, что доказано / не доказано.

Источник

1 ответ

Решение

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

Выявление отдельных пунктов

Спецификации ACSL быстро состоят из множества пунктов (requires, ensures, loop invariant, assert...) Важно уметь легко различать их. Для этого у вас есть два основных ингредиента:

  1. Используйте графический интерфейс. Намного легче увидеть, какие аннотации доказаны (зеленая маркировка), доказаны, но при условии, что другие недоказанные предложения являются истинными (зеленый / желтый) или недоказанными (желтый).
  2. Назовите ваши предложения: любой предикат ACSL может быть связан с именем с синтаксисом name: pred, Когда предложение снабжено именем, WP будет использовать его для ссылки на предложение.

Обычные подозреваемые

Очень легко пропустить какую-то очень важную часть спецификации. Вот краткий контрольный список:

  1. Все петли должны быть оснащены loop invariant а также loop assigns
  2. Все функции, вызываемые анализируемой, должны иметь контракт (по крайней мере, с assigns оговорка)
  3. Если ячейка памяти упоминается в loop assigns не подлежит соответствующему loop invariant Вы ничего не знаете о значении, хранящемся в этом месте за пределами цикла. Это может быть проблемой.

Отладка отдельных предложений

Если вы уверены, что не пропустили ничего очевидного, настало время начать изучение конкретных предложений.

  1. Как правило, гораздо проще проверить, что loop invariant устанавливается (т. е. истина при достижении цикла в первый раз), а не сохраняется (остается верным на протяжении шага цикла). Если вы не можете установить loop invariant, это либо неправильно, либо вы забыли requires ограничить ввод функции (типичный случай для алгоритма над массивами loop invariant 0<=i<=n; это не может быть доказано, если вы этого не сделаете requires n>=0;)
  2. так же assigns а также loop assigns должно быть легче проверить, чем реальные функциональные свойства. Пока они не все доказаны, вы должны сосредоточиться на них (распространенная ошибка - забыть поместить индекс цикла в loop assigns или упомянуть, что он назначает a[i] и не a[0..i]). Не забывай это assigns должен включать все возможные задания, в том числе выполненные в вызываемых пользователях.
  3. Не стесняйтесь использовать assert проверить, может ли WP доказать, что свойство имеет место в данной точке. Это поможет вам понять, где возникают проблемы. [ редактировать в соответствии с комментарием @DavidMENTRÉ ниже ] Обратите внимание, что в этом случае вы должны позаботиться о том, чтобы первоначальное обязательство по доказательству могло бы быть выполнено в предположении, что assert держит в то время как assert Сам не подтвержден. В графическом интерфейсе это отражается зеленой / желтой пулей и, конечно, желтой пулей перед assert, В этом случае доказательство еще не закончено, и вы должны понять, почему утверждение не доказано, возможно, используя ту же стратегию, что и выше, пока вы точно не поймете, в чем проблема.
Источник
Другие вопросы по тегам