logic - 是 {true} x := y { x = y } a valid Hoare triple?

Question

我不确定

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

是有效的 Hoare triple .

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

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

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

如何？

Answer 1

I am not sure that

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

is a valid Hoare triple.

三元组应阅读如下:

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

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

x := y的最弱前提给定后置条件 { x = y }是 { y = y } , 和

{ true }暗示 { y = 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不再满足后置条件。