В чем разница между утверждением в C и утверждением в проверке модели, например CBMC?

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

В программировании на C мы определяем макрос assert() с заголовочным файлом assert.h. Макрос assert() возвращает значение TRUE, если его параметр оценивается как TRUE, и предпринимает какие-либо действия, если он оценивает FALSE. Многие компиляторы прервут программу при неудачном вызове assert().

Может ли кто-нибудь прояснить разницу между этими двумя утверждениями в мире проверки моделей и программирования?


c testing assert model-checking
person sepideha    schedule 27.08.2016    source источник
comment
assert возвращает void, хотя было бы полезно возвращать значение выражения.   -  person Jonathon Reinhart    schedule 27.08.2016
comment
@JonathonReinhart Это невозможно сделать в сборках NDEBUG, потому что тогда условие никогда не оценивается.   -  person melpomene    schedule 27.08.2016
comment
@melpomene Я знаю - я думаю, вам придется реализовать это самостоятельно. Довольно часто обнаруживают ошибку, обрабатывая ее одним способом в релизных сборках, но с шумом прерывая ее в отладке.   -  person Jonathon Reinhart    schedule 27.08.2016

Ответы (3)


arrow_upward
3
arrow_downward

При проверке модели утверждение (как вы сказали) проверяется для всех возможных прогонов (это основная цель средства проверки модели). Итак, если это правда, вы будете знать, что условие всегда будет выполняться, что бы ни случилось. Это относится к области официальной проверки.

В то время как в C утверждение проверяется во время выполнения, то есть для данного экземпляра запуска, нет гарантии, что оно будет верным в другом запуске. Это относится к области тестирования.

person Jean-Baptiste Yunès    schedule 27.08.2016

arrow_upward
1
arrow_downward

Для C это зависит от того, определяется ли NDEBUG при включении assert.h.

Если NDEBUG не определено, assert, приводящее к false, напечатает сообщение о стандартной ошибке и прервет программу.

Если NDEBUG определено, assert не будет генерировать никакого кода, т. е. проверка будет пропущена.

См. также http://man7.org/linux/man-pages/man3/assert.3.html

person 4386427    schedule 27.08.2016

arrow_upward
1
arrow_downward

Утверждение в C (см. https://en.wikipedia.org/wiki/Assert.h) отличается от assert при проверке модели. Например,

    assert(x > 0);

В C программа выполняется, и когда оператор assert оценивается как ложный, выполнение прерывается. На самом деле assert() выводит сообщение об ошибке в стандартную ошибку и завершает программу, вызывая abort().

Наоборот, фактически, в средстве проверки моделей оператор assert принимает логическое условие и проверяет, что это условие истинно для всех запусков программы. В алгоритме проверки модели (в случае CBMC/HiFrog,...) нет выполнения программы (поскольку это часть статического анализа). Алгоритм проверки модели на высоком уровне выглядит следующим образом:

Сначала средство проверки модели превращает всю программу вместе с отрицанием утверждения в логическую формулу (логическую, LRA, ...), а затем передает всю формулу процедуре принятия решения, такой как решатель SAT/SMT. Если формула невыполнима (нет решения), это означает, что в программе выполняется утверждение, x > 0 для всех возможных входов программы. В противном случае есть по крайней мере один вход, который делает x меньше нуля в утверждении.

Как объяснялось выше, при проверке модели утверждение проверяется для всех возможных прогонов (основная цель средства проверки модели). Таким образом, если средство проверки модели подтвердит истинность утверждения, мы будем знать, что утверждение утверждения всегда будет выполняться для любого произвольного ввода/запуска программы.

person sepideha    schedule 09.07.2019