{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

如何？

Answer 1

我不确定

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

是一个有效的Hoare三重奏.

三元组应该如下:

      "无论启动状态如何,执行x:=yx等于y后."

它确实成立了.它为何成立的正式论据是

1. x := y给定后置条件的最弱前提{ x = y }是{ y = y },和
2. { 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不再满足后期条件.

Answer 2

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