verification - 为什么在最强的后置条件中存在是必要的？

Question

我见过的最强后置谓词转换器的每个公式都呈现如下分配规则：

sp(X:=E, P) = ∃v. (X=E[v/X] ∧ P[v/X])

我想知道，为什么上述规则中需要存在（以及存在量化的变量“v”）？在我看来，最强的后置条件谓词转换器几乎与符号评估相同，因为您维护一个状态（从变量到值的映射）和一个路径条件（一个谓词，在程序中的特定点必须为真）。然而，符号评估并不依赖于存在量词。

所以，我想我一定在这里遗漏了一些东西。任何帮助表示赞赏！

Answer 1

我将给出一些直观的描述，因为您对符号评估有一些了解

如果你有一个任意的变量映射，在分析过程中查看它们之前，你不能说出程序中未来状态变化的任何内容。

符号评估会记住每个选择的路径[作为状态空间分离]，因此它不需要包含在评估公式中来解决。

然而，在这里你争论每一个可能的路径，因此需要一个任意的公式来描述行为。

假设您将变量保留在公式中，那么您只会争论可能运行的 1 条路径。如果您知道您的变量不会引发其他路径，那么您可以简化此行为。

不管有多么弱的自由先决条件，您都知道您从哪条可能的路径开始并将所有路径包装在一起以证明有关您的系统的属性。