c - “在 C 中断言”和“在模型检查中断言如 CBMC”有什么区别？

Question

在像 CBMC（C 的有界模型检查器）这样的模型检查器中，用户定义的断言语句采用布尔条件，模型检查器检查程序所有可能执行的条件是真还是假。

在 C 编程中，我们使用头文件 assert.h 定义 assert() 宏。如果它的参数评估为 TRUE，则 assert() 宏返回 TRUE，如果评估为 FALSE，则执行某种操作。许多编译器会在失败的 assert() 上中止程序。

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

Answer 1

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

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

Answer 2

对于 C，它取决于是否NDEBUG定义了 whenassert.h被包含。

如果NDEBUG未定义，则assert结果为 false 将在标准错误上打印一条消息并终止程序。

如果NDEBUG已定义assert将不会生成任何代码，即跳过检查。

另见http://man7.org/linux/man-pages/man3/assert.3.html

Answer 3

C 中的断言（参见 https://en.wikipedia.org/wiki/Assert.h）与模型检查中的断言不同。例如，

    assert(x > 0);

在 C 中，程序被执行，当断言语句被评估为 false 时，执行中止。事实上，assert() 将错误消息打印到标准错误并通过调用 abort() 终止程序。

相反，事实上，在模型检查器中，assert 语句接受一个布尔条件，并检查该条件对于程序的所有运行是否为真。在模型检查算法中（在 CBMC/HiFrog 的情况下，...）没有程序的执行（因为它是静态分析的一部分）。高层的模型检查算法如下：

首先，模型检查器将整个程序与断言的否定一起转换为逻辑公式（布尔，LRA，...），然后将整个公式传递给决策程序，例如 SAT/SMT 求解器。如果公式不可满足（无解），则表示程序中的断言保持，对于程序的所有可能输入，x > 0。否则，至少有一个输入使 x 在断言中变得小于零。

如上所述，在模型检查中，针对所有可能的运行验证断言（模型检查器的主要目标）。因此，如果模型检查器验证断言为真，我们将知道断言语句将始终适用于程序的任意输入/运行。