{true} x := y { x = y } 是有效的霍尔三元组吗?
我不确定这
{ true } x := y { x = y }
是一个有效的霍尔三元组。
我不确定是否允许引用变量(在本例中为 y),而无需首先在三重程序主体或前置条件中明确定义它。
{ y=1 } x := y { x = y } //valid
{true} y := 1; x := y { x = y } //valid
如何?
I am not sure that
{ true } x := y { x = y }
is a valid Hoare triple.
I am not sure one is allowed to reference a variable (in this case, y
), without explicitly defining it first either in the triple program body or in the pre-condition.
{ y=1 } x := y { x = y } //valid
{true} y := 1; x := y { x = y } //valid
How is it?
如果你对这篇内容有疑问,欢迎到本站社区发帖提问 参与讨论,获取更多帮助,或者扫码二维码加入 Web 技术交流群。
发布评论
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱,如果其他用户或者作者回复了您的评论,将不能在第一时间通知您!
该三元组应解读如下:
“无论如何执行
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 := 0; y := 0
不再满足后置条件。The triple should be read as follows:
"Regardless of starting state, after executing
x:=y
x equals y."and it does hold. The formal argument for why it holds is that
x := y
given postcondition{ x = y }
is{ y = y }
, and{ true }
implies{ y = y }
.However, I completely understand why you feel uneasy about this triple, and you're worried for a good reason!
The triple is badly formulated because the pre- and post condition do not provide a useful specification. Why? Because (as you've discovered)
x := 0; y := 0
also satisfies the spec, sincex = y
holds after execution.Clearly,
x := 0; y := 0
is not a very useful implementation and the reason why it still satisfies the specification, is (according to me) due to a specification bug.How to fix this:
The "correct" way of expressing the specification is to make sure the specification is self contained by using some meta variables that the program can't possible access (
x₀
andy₀
in this case):Here
x := 0; y := 0
no longer satisfies the post condition.