{true} x := y { x = y } 是有效的霍尔三元组吗?

发布于 12-07 16:30 字数 322 浏览 0 评论 0原文

我不确定这

{ 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 技术交流群。

扫码二维码加入Web技术交流群

发布评论

需要 登录 才能够评论, 你可以免费 注册 一个本站的账号。

评论(3

半仙2024-12-14 16:30:11

我不确定

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

是一个有效的 Hoare 三元组。

该三元组应解读如下:

      “无论如何执行x:=y后,x等于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 不再满足后置条件。

I am not sure that

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

is a valid Hoare triple.

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

  1. the weakest precondition of x := y given postcondition { x = y } is { y = y }, and
  2. { 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, since x = 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₀ and y₀ in this case):

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

Here x := 0; y := 0 no longer satisfies the post condition.

茶底世界2024-12-14 16:30:11

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

x := y是赋值,因此将前置条件中的替换掉。
前提条件为 {y=y},这意味着 {true}

换句话说,{y=y} => {true}

{ true } x := y { x = y } is a valid Hoare triple. The reason is as follows:

x := y is an assignment, therefore, replace that in the precondition.
The precondition stands as {y=y}, which implies {true}.

In other words, {y=y} => {true}.

以酷2024-12-14 16:30:11

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

* If x:=y, then Q. Q.E.D. _*

~没有更多了~
我们使用 Cookies 和其他技术来定制您的体验包括您的登录状态等。通过阅读我们的 隐私政策 了解更多相关信息。 单击 接受 或继续使用网站,即表示您同意使用 Cookies 和您的相关数据。
原文