{true} x := y { x = y } 是有效的 Hoare 三元组吗？答案

【问题标题】：Is {true} x := y { x = y } a valid Hoare triple?{true} x := y { x = y } 是有效的 Hoare 三元组吗？
【发布时间】：2011-10-02 20:14:13
【问题描述】：

我不确定

{ true } x := y { x = y }

是一个有效的Hoare triple。

我不确定是否允许引用一个变量（在本例中为y），而无需先在三重程序主体或前置条件中明确定义它。

{ y=1 } x := y { x = y } //valid

{true} y := 1; x := y { x = y } //valid

怎么样？

【问题讨论】：

【解决方案1】：

我不确定
{ true } x := y { x = y }
是一个有效的 Hoare 三元组。

三元组应该读成如下：

“无论开始状态如何，执行x:=y后x等于y。”

它确实成立。为什么它成立的正式论据是

不过，我完全理解你为什么对这个三元组感到不安，你的担心是有充分理由的！

三元组的表述很糟糕，因为前后条件没有提供有用的规范。为什么？因为（正如您所发现的）x := 0; y := 0 也满足规范，因为x = y 在执行后仍然成立。

显然，x := 0; y := 0 不是一个非常有用的实现，它仍然满足规范的原因是（根据我）是由于 规范错误。

如何解决这个问题：

表达规范的“正确”方式是通过使用程序无法访问的一些元变量（x₀ 和 y₀ in本例）：

{ x=x₀ ∧ y=y₀ } x := y { x=y₀ ∧ y=y₀ }

这里x := 0; y := 0不再满足post条件。

【讨论】：

【解决方案2】：

{ true } x := y { x = y } 是一个有效的 Hoare 三元组。原因如下：

x := y 是一个赋值，因此，在前置条件中替换它。
前置条件为{y=y}，表示{true}。

换句话说，{y=y} => {true}。

【讨论】：

【解决方案3】：

* 如果 x:=y，那么 Q.Q.E.D. _*

【讨论】：

当然。一个苹果就是一个苹果。梨就是梨。绿海龟是绿海龟。如果 (x:=y) 则 x=y。所以，如果你有两只绿海龟，那么它们都是绿海龟。与两只大绿海龟等一样。
换一种说法：A=A if A:=A.
也许您需要为您的问题添加解释。您是在特定语言实现的上下文中还是在特定的具体实现上下文中询问？ IMO，这将使问题变得不同于所陈述的内容。一般来说，一个陈述会导致自己作为一个结论。
这被标记为 Hoare Logic。这不是某种“特定实现”或任何编程语言。
它没有以任何方式回答 OP 中的问题。