为什么赋值规则是Hoare逻辑中的方式？

Question

为什么赋值规则是Hoare逻辑/公理语义中的方式？我无法思考为什么分配规则与我预期的相反。

我明白Hoare逻辑是用来证明程序状态的正式命题，因为命令被执行。因此，如果我们执行命令 $ $x:=e$ $ 我会料到 下一个 态具有这样的取代。..但似乎替代发生了 以前 我们执行任务，我发现bizzare。我会料到的:

$ $\{P\}x:=e\{p[e/x]\}$ $

鉴于此 $P$ 是关于程序状态的语句。

我敢肯定有一个很好的解释，对不起，如果这是一个基本的问题，我知道它必须是。但有人能给我解释一下吗？

---

奖金问题:

我们为什么不把赋值规则写成:

$ $\{Q\}x:=e\{q[x/e]\}$ $

请注意，它与我最初的建议不一样，因为我们有 $x$ 和 $e$ 到处交换。即在岗位条件下，只要我们有一个 $e$ 我们放置一个 $x$ （这很好，因为我们刚刚执行的语句是 $x$ 持有的价值 $e$, ，所以我们应该能够更换 $e$ 为 $x$ 如果前置条件有帮助，则在后置条件中。

---

我读过的相关帖子没有帮助:

• Hoare triple for assignment p{x/E}x:=E{P}
• 维基百科Hoare逻辑
• https://www.quora.com/unanswered/Why-is-the-assignment-rule-the-way-it-is-in-Hoare-Logic
• https://www.reddit.com/r/ProgrammingLanguages/comments/e8suhh/why_is_the_assignment_rule_the_way_it_is_in_hoare/

---

附录:

对于我们阅读障碍者来说，在这个问题中，这就是替换符号的含义:

$ $P[e/x]=p[e o x]$ $

即替换每个自由出现的 $x$ 用表达式/术语/事物 $e$.

Answer 1

所以在阅读和思考它后，这是我的解释（谢谢软件基础）：

我的关键混淆似乎是 $ p [e / x] $ 的含义（用e替换x的每个自由实例））。无论您看到符号 $ x $ 字面上都会删除它并放置 $ e $ 。例如 $ p [e / x]=（x + y + 1）[e / x] \到p [e / x]=（e + y + 1）$ 所以请注意<跨越类=“math-container”> $ x $ 从 $ p $ 。所以我们想要的是，一旦我们进行了作业：

$$ x：= e $$

如果我们有 $ x $ 而不是 $ e $ ，则该声明是正确的。所以，如果规则是：

$$ \ {p [e / x] \} x：= e \ {p \} $$

然后我们想要的是，当我们插入 $ x $ for $ e $ 我们想要的考虑到陈述是真实的。所以在我们开始代码之前，我们有 $ p [e / x] $ 。然后我们运行分配和 $ e $ 消失的所有实例，我们得到 $ x $ 替换它们。如果ran被赋值的代码（因为 $ x $ 现在按住Value > $ e $ ，因此您可以删除 $ e $ s并放置 $ x $ ）。

这是抽象概念的解释。让（无耻地）使用软件基础（SF）示例：

{{y= 1}} x ::= y {{x= 1}}英文：如果我们在y值为1的状态下启动，我们将y分配给x，那么我们会在x为1的状态下完成。即，等于1的属性从y转移到x。

来自SF的另一个有用段落：

同样，在 {{y + z= 1}} x ::= y + z {{x= 1}} 相同的属性（等于一个）从分配右侧的表达式y + z传输到x。 更一般地，如果a是任何算术表达式，那么 {{a= 1}} x ::= a {{x= 1}} 是一个有效的Hoare三倍。

---

附录来自评论的伟大观察：

认识到规则是很重要的 { P. [ E. / X ] } X ：= E. { P. } 允许表达式 E. 和变量 X 发生在后期。换句话说，推理规则允许您推断出一个出现的任何子集的后期位置 E. 在前提下已被替换 X ，包括它们都不。此外，它允许您同时推断所有这些不同的后兴。

---

回复奖金为什么

1） $ \ {p [e / x] \} x：= e \ {p \} $

比

更好

2） $ \ {q \} x：= e \ {q [x / e] \} $ ：

除了用可能是不可见的表达式替换x的微妙点（例如，e= 0，如果我们用无限数量的 $ 0 $ “Math-Container”> $ x $ 's吗？如果零点不存在......规则应该是句法，但我认为最好避免这种混淆），我认为这是原因：< / p>

捕获的分配规则是我们将表达式e分配给变量x。因此，只有x应该被e“替换”。直观地，在代码中（或者更准确地是程序 $ \ sigma $ ），当x开始持有值e时，它不会随机意味着到处都是执行分配 $ x：= e $ 后，可能存在x。事实上它所做的是，现在在帖子条件下我们有x的。现在，那些X如果我们没有赋值，则应具有 $ e $ 等值的值。我们只“撤消”替换/分配赋值命令。不是每隔一个随机表达式e。简而言之，知道在哪里放置正确的E的方法是通过在完成作业后开始在后期条件下，然后从那里开始放置e。如果我们倒退，我们可能会更换我们不想替换的e（即使他们可能是真的，我猜他们应该在分配e to x之后保持x的值x。

Answer 2

假设我们正在运行程序 x := e, ，并让 $\sigma$ 为初始状态，并且 sigma\西格玛'$ 为最终状态。

这里的关键直觉是:的价值 $x$ 在 决赛 国家 sigma\西格玛'$ 与表达式的值相同 $e$ 在 初始 国家 $\sigma$.事实上，后者是我们分配给的值 $x$ 用命令 x := e.

因此，如果 $P(-)$ 是值的属性，公式 $P(\mbox{x x$-in-the-final-state})$ 相当于 $P(\mbox{e e$-in-the-initial-state})$.换句话说 ＜P(x)＞ 在 邮递服务 （在状态 sigma\西格玛'$）真的相当于 ＜P(e)＜ 在 先决条件 （在状态 $\sigma$).

使用替换只是将后置条件视为"依赖于 $x$"，即作为 ＜P(x)＞, ，然后要求 ＜P(e)＜ 作为先决条件。