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

Question

我所见过的最强后置条件谓词转换器的每个公式都给出了如下赋值规则：

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

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

所以，我想我一定是漏掉了什么。如有任何帮助，我们不胜感激！

Answer 1

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

如果您有一个到变量的任意映射，那么在分析过程中查看它们之前，您不能对程序中未来的状态更改说任何话。

符号求值记住了每条选定的路径状态空间的分离，因此不需要包含在求值公式中求解。

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

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

然而，在最弱的自由前提下，您知道从哪条可能的路径开始，并将所有路径包装在一起，以证明您的系统的属性。