Кажется, что автоматические c решатели не могут иметь дело со свойством, сгенерированным WP. Может быть, потому, что они не могут, или может быть из-за кодировки свойства.
Тем не менее, как вы сказали:
это всего лишь 16 случаев, их можно просто перечислить
И WP GUI предоставляет tacti c для создания такого доказательства. Если доказательство признано неудачным, дважды щелкните цель доказательства на панели «WP Goal» в нижней части окна. Затем выберите переменную для перечисления. Нажмите на тактич. c «Диапазон» и установите нижнее значение на 0, а верхнее на 15. Наконец, нажмите на зеленую стрелку рядом с названием тактильного обозначения c. WP сгенерирует 18 контрольных целей:
< 0
и > 15
: тривиально, поскольку условие: 0 <= i <= 15
0, 1, 2, 3 ..., 15
: автоматически сбрасывается WP Qed
Затем вы можете щелкнуть значок сохранения, чтобы можно было легко воспроизвести доказательство.
введите описание изображения здесь
Если вы затем захотите воспроизвести доказательство из GUI, вы можете использовать стрелку, которая появляется на панели «WP Goal», когда существует скрипт проверки. Или вы можете напрямую попросить использовать существующие сценарии в командной строке, добавив tip
в список проверяющих:
frama-c -wp -wp-prover alt-ergo,tip file.c
Обратите внимание, что сценарии WP сохраняются в сеансе WP, то есть по умолчанию в каталоге ./.frama-c/wp/scripts
. Каталог сеанса WP можно настроить с помощью опции wp-session <directory>
.