c - "assert in C"和 "assert in model checking like CBMC"有什么区别？

Question

在像 CBMC(Bounded Model Checker for C)这样的模型检查器中，用户定义的断言语句接受一个 bool 条件，模型检查器检查程序所有可能执行的条件是真还是假。

在C 编程中，我们使用头文件assert.h 定义assert() 宏。 assert() 宏如果其参数求值为 TRUE 则返回 TRUE，如果它求值为 FALSE 则采取某种操作。许多编译器会在 assert() 失败时中止程序。

有人可以澄清模型检查和编程世界中这两个断言之间的区别吗？

Answer 1

在模型检查中，断言(如您所说)针对所有可能的运行进行验证(这是模型检查器的主要目的)。因此，如果它为真，您就会知道无论发生什么情况，该条件都将始终成立。这是在形式验证领域。

而在 C 中，断言在运行时进行验证，即对于给定的运行实例，则不能保证它在另一次运行中为真。这是在测试领域。