"assert in C“和"assert in model checking like CBMC”有什么区别？

Question

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

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

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

Answer 1

在模型检查中，assert (如您所说)针对所有可能的运行进行了验证(这是模型检查器的主要意图)。因此，如果这是真的，你就会知道，无论发生什么，条件总是成立的。这属于形式化验证领域。

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

Answer 2

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

如果未定义NDEBUG，则生成false的assert将在出现标准错误时打印一条消息，并终止程序。

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

另请参阅http://man7.org/linux/man-pages/man3/assert.3.html

Answer 3

C中的Assert (参见https://en.wikipedia.org/wiki/Assert.h)不同于模型检查中的assert。例如，

    assert(x > 0);

在C中，程序被执行，当assert语句被计算为false时，执行中止。实际上，assert()会向标准错误输出一条错误消息，并通过调用abort()来终止程序。

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

首先，模型检查器将整个程序连同断言的否定转换为逻辑公式(Boolean，LRA，...)，然后将整个公式传递给诸如SAT/SMT求解器之类的决策过程。如果公式不可满足(无解)，则表示程序中的断言保持，对于程序的所有可能输入，x>0。否则，至少有一个输入会使断言中的x变得小于零。

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