debugging - 软件错误总是逻辑矛盾吗？

Question

在研究命题逻辑时，我提出了以下问题：

软件错误总是程序和规范之间的逻辑矛盾吗？

考虑以下示例：我们的规范告诉我们“如果前提 A 和 B 为真，我们会执行动作 C ”。

其实现如下：

main ()
  if A then C
  if B then C

很明显，可以看到规范不适合实现，因为（考虑上面的程序）“如果前提 A 或前提 B 为真，我们会做 C ”。

将我们的规范和程序表达为命题公式，我们得到以下等式：

我们将规范转换为 CNF 并应用解析演算，现在我们可以很容易地看到第一个子句与最后一个子句相矛盾。因此这个公式是不可满足的，因此我们的规范与我们的实现相矛盾。

我现在的问题是（因为上面只是一个例子）：

假设一个完整的文档，对于每个软件错误都是如此吗？

如果是这样：

如果我们将完整的规范转换为命题公式，我们是否可以自动化软件错误发现的过程？

score 0 · Accepted Answer

回答我自己的问题：这被称为“模型检查”，在英特尔等大公司的计算机科学中非常常见，用于检查硬件是否真的在做它应该做的事情。

最近，模型检查也开始越来越多地出现在软件开发中。例如，NASA 和 Microsoft 正在相当程度上使用这项技术。

在其基本形式中，它的工作方式如下：规范被转换为逻辑语句，编译器将给定的软件程序转换为称为“Kripke 结构”的树状结构。模型检查器将这些作为输入，并给出规范不完整的反例或发出真值。

1 回答 1