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

Question

我不确定

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

是一个有效的Hoare 三元组。

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

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

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

如何？

score 6 · Accepted Answer

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

三元组应如下解读：

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

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

但是，我完全理解你为什么对这个三重奏感到不安，你的担心是有道理的！

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

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

如何解决这个问题：

表达规范的“正确”方式是通过使用程序无法访问的一些元变量来确保规范是自包含x₀的（y₀在这种情况下）：

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

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

score 1 · Accepted Answer

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

x := y是一个赋值，因此，在前置条件中替换它。
前提是{y=y}，这意味着{true}。

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

score -2 · Accepted Answer

-2

*如果 x:=y，则 QQED _ *

于 2011-10-02T21:04:52.493 回答

3 回答 3